package cryptoverif

  1. Overview
  2. Docs
CryptoVerif: Cryptographic protocol verifier in the computational model

Install

Dune Dependency

Authors

Maintainers

Sources

cryptoverif2.02.tar.gz
md5=d8fc3009b4de37f09ab769a323198c0c
sha512=1fcc9a991211d13b0fa2b4ebe864a4595cd90a85bb71bed3e82a8fbf5f9304567b42875adebae9b78f2df9fcee56c7659f02fe83f15bca57ab854b607cba2058

README.md.html

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
OCaml

Innovation. Community. Security.