package cryptoverif
Install
Dune Dependency
Authors
Maintainers
Sources
md5=d0f0525bbdd4a2820214cdfa51f2f4a7
sha512=c8a1ea460b28be1c06db24826d6bcbe307f142d9248042d9a75ffe5a4c48a1c9f12157d2b83c8176aad7c03de031b62a37d8f6b3230d78195871908d2c7de6d5
Description
CryptoVerif is an automatic protocol prover sound in the computational model. It can prove
- secrecy;
- correspondences, which include in particular authentication;
- indistinguishability between two games.
It provides a generic mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular symmetric encryption, message authentication codes, public-key encryption, signatures, hash functions.
The generated proofs are proofs by sequences of games, as used by cryptographers. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. CryptoVerif can also evaluate the probability of success of an attack against the protocol as a function of the probability of breaking each cryptographic primitive and of the number of sessions (exact security).
This software is under development; please use it at your own risk. Comments and bug reports welcome.
Published: 16 Oct 2020
README
TLS 1.3: Computational Verification with CryptoVerif
Lemmas on the key schedule (Section 6.3)
KeySchedule1.cv
KeySchedule2.cv
KeySchedule3.cv
HKDFexpand.cv
The protocol
Initial handshake (Section 6.4)
tls13-core-InitialHandshake.cv
tls13-core-InitialHandshake-1RTT-only.cv
The first file deals with 0.5-RTT and 1-RTT messages. The second one supports only 1-RTT (but proves stronger properties from server to client messages).
Handshake with pre-shared key (Section 6.5)
tls13-core-PSKandPSKDHE-NoCorruption.cv
Record Protocol (Section 6.6)
tls13-core-RecordProtocol.cv
tls13-core-RecordProtocol-0RTT.cv
tls13-core-RecordProtocol-0RTT-badkey.cv
The first file is the normal record protocol. The last two are variants for 0-RTT messages: one with a replicated receiver, and one with no sender.
Summary of obtained results:
HKDFexpand
All queries proved.
0.024s (user 0.020s + system 0.004s), max rss 29424K
KeySchedule1
All queries proved.
0.036s (user 0.028s + system 0.008s), max rss 36752K
KeySchedule2
All queries proved.
0.028s (user 0.024s + system 0.004s), max rss 33808K
KeySchedule3
All queries proved.
0.480s (user 0.472s + system 0.008s), max rss 53424K
tls13-core-InitialHandshake
All queries proved.
115.935s (user 115.751s + system 0.184s), max rss 2171776K
tls13-core-InitialHandshake-1RTTonly
All queries proved.
121.572s (user 121.412s + system 0.160s), max rss 2199040K
tls13-core-PSKandPSKDHE-NoCorruption
All queries proved.
482.898s (user 482.646s + system 0.252s), max rss 1711360K
tls13-core-RecordProtocol
All queries proved.
0.044s (user 0.044s + system 0.000s), max rss 31312K
tls13-core-RecordProtocol-0RTT
All queries proved.
0.044s (user 0.044s + system 0.000s), max rss 31408K
tls13-core-RecordProtocol-0RTT-badkey
All queries proved.
0.036s (user 0.028s + system 0.008s), max rss 30032K