CryptoVerif is an automatic protocol prover sound in the computational model. It can prove
- 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: 11 Jul 2023
Analysing the HPKE Standard – Supplementary Material
The material in this directory is supplementary material accompanying the paper:
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer. Long version: https://eprint.iacr.org/2020/1499
The “RFC” we are referring to in this README, is the draft 8 of the RFC “Hybrid Public Key Encryption”.
Files in this Directory
The files with filenames starting by
lib.* contain macro definitions for CryptoVerif:
lib.authkem.ocvl: assumptions on authenticated KEMs as defined in the paper
lib.gdh.ocvl: the GDH assumption as used by the paper. This is a simplified version of the GDH assumption available in the standard CryptoVerif library, with just the oracles needed for our proofs.
lib.aead.ocvl: defines an AEAD scheme, with multikey security notions.
lib.prf.ocvl: defines a PRF, with a multikey security notion.
lib.choice.ocvl: defines convenience functions to choose between plaintexts m0 and m1 based on a bit b.
lib.option.ocvl: defines a macro for option types, which we heavily use as return types of functions
lib.truncate.ocvl: defines an equivalence for transforming a uniformly distributed random value of one type into a uniformly distributed random value of another, shorter, type.
The files with filenames starting by
common.* contain definitions used in multiple models:
common.dhkem.dh.ocvl: definition of the Diffie-Hellman group for all DHKEM security notions
common.dhkem.ocvl: definition of DHKEM as defined in the RFC
common.hpke.ocvl: definition of HPKE (only everything after the KEM) as defined in the RFC
These files are included by the
*.m4.ocv files that generate the model files.
The ”model files” are the files on which we run CryptoVerif. Each model contains the definition of a security notion, the definition of the game, and the proof.
We prove three security notions for DHKEM, and three security notions for HPKE. These three files share a lot of code, which is why we generate the files from templates. These templates are the
*.m4.ocv files; m4 makes reference to the preprocessor m4 which we use.
To generate the model files from the templates, run the script
prepare in this directory.
Which files to read
If you don't mind jumping around in one big file, you can read the
*.ocv files listed below.
If you prefer smaller files, you can read the
*.m4.ocv files for an overview, and look at the included files separately.
dhkem.auth.outsider-cca-lr.ocv: Prove that DHKEM as defined in the RFC is Outsider-CCA-secure.
dhkem.auth.outsider-auth-lr.ocv: Prove that DHKEM as defined in the RFC is Outsider-Auth-secure.
dhkem.auth.insider-cca-lr.ocv: Prove that DHKEM as defined in the RFC is Insider-CCA-secure.
We do not use a template for this proof, because it is the only one of its kind.
keyschedule.auth.prf.ocv: Prove that the key schedule
KS_auth()as used by HPKE's mode Auth, is a PRF with
HPKE Composition Proofs
These models treat HPKE as defined in the RFC, assuming
KeySchedule (without the VerifyPSKInputs call) is a PRF with
the KEM used is an authenticated KEM satisfying the appropriate above-mentioned security notions
There is one model for each security notion:
hpke.auth.outsider-cca.ocv: Prove that HPKE is Outsider-CCA-secure.
hpke.auth.outsider-auth.ocv: Prove that HPKE is Outsider-Auth-secure.
hpke.auth.insider-cca.ocv: Prove that HPKE is Insider-CCA-secure.