package cryptoverif

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

Install

Dune Dependency

Authors

Maintainers

Sources

cryptoverif2.04.tar.gz
md5=f08d6ff61416ad6caa068ebecf1694d5
sha512=eecbc4c2ce8bfe603cc16a85ee2ac0f53a8b7b15c07712e2cd9f4428a6cd18f5904d2fd3043fc273fce7bbc3b188f8c50db9040b164f7e2f85c1911475755a5c

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: 02 Dec 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

Dependencies (4)

  1. conf-m4 post
  2. cryptokit post
  3. ocamlfind post
  4. ocaml >= "4.03"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.