Dealing with Dynamic Key Compromise in CryptoVerif

archive of all files

These examples run with CryptoVerif version 2.07. Most of these files are also included in the CryptoVerif distribution, and the files in the distribution will be updated if needed as CryptoVerif evolves.

To use the scripts run mentioned below, the cryptoverif executable should be in the PATH or the variable CVDIR should be set to the directory that contains the cryptoverif executable.

• Examples 2 and 3
• Additional application of the new proof of secrecy to a signed Diffie-Hellman protocol (file examples/basic/signedDH-forward-secrecy.cv in the CryptoVerif distribution)
• Examples 4 to 6 (file examples/basic/forward-secrecy-focus-success-simplify.cv in the CryptoVerif distribution)
• Example 7 (file examples/obasic/intctxt-corrupt.ocv in the CryptoVerif distribution)
• Examples 8 and 9 (file examples/basic/pkauth-guess.cv in the CryptoVerif distribution)
• Section VI.A Compromise of the Pre-shared Key in TLS 1.3 and WireGuard
  • TLS (file examples/tls13/tls13-core-PSKDHE-CorruptPSK.cv in the CryptoVerif distribution)
  • WireGuard This file generates several CryptoVerif files using m4. You should run it by downloading the whole archive and running the script run inside the directory WireGuard. (File examples/wireguard/WG.25519.psk_dyn.m4.cv in the CryptoVerif distribution. The CryptoVerif files are generated by examples/wireguard/prepare.)
• Section VI.B PRFODH
  • model of Noise NK that relies on the PRFODH assumption
    model of Noise NK that relies on GDH + the random oracle model
    These two files use a specific library of cryptographic primitives. You should run them by downloading the whole archive and running the script run inside the directory PRFODH/NoiseNK. (directory examples/noiseNK/ in the CryptoVerif distribution)
  • model of TLS 1.3 Draft 18 that relies on the PRFODH assumption (directory examples/tls13/PRFODH/ in the CryptoVerif distribution)
  • model of the Diffie-Hellman authenticated KEM of HPKE that relies on the PRFODH assumption. The files in this directory use a specific library of cryptographic primitives. You should run them by downloading the whole archive and running the script run inside the directory PRFODH/HPKE. (directory examples/hpke/PRFODH/ in the CryptoVerif distribution)
• Section VI.C OEKE (file examples/obasic/OEKE-forward-secrecy.ocv in the CryptoVerif distribution)
• Section VI.D Grouping compromise scenarios. This file uses a specific library of cryptographic primitives. You should run it by downloading the whole archive running the script run inside the directory WireGuard_group. (file examples/wireguard/WG.25519.AB-BA.replay_prot.cv in the CryptoVerif distribution)