package cryptoverif
Install
Dune Dependency
Authors
Maintainers
Sources
md5=b05495bf9320cf5647ae2054a3517c58
sha512=9605625a4c69950cb5407da236228d6a110c313c0db3f12b43527afc1c1d6ca8fc16582a8091d85a42229da0ea4ecb85433c3b28ff57dfd416c41f9180945c6d
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: 11 Jul 2023
README
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
Preliminaries
The “RFC” we are referring to in this README, is the draft 8 of the RFC “Hybrid Public Key Encryption”.
Files in this Directory
Library Files
The files with filenames starting by lib.*
contain macro definitions for CryptoVerif:
lib.authkem.ocvl
: assumptions on authenticated KEMs as defined in the paperlib.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 functionslib.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.
Common Definitions
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 notionscommon.dhkem.ocvl
: definition of DHKEM as defined in the RFCcommon.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.
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
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.
KeySchedule
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 scheduleKS_auth()
as used by HPKE's mode Auth, is a PRF withshared_secret
as key.
HPKE Composition Proofs
These models treat HPKE as defined in the RFC, assuming
KeySchedule (without the VerifyPSKInputs call) is a PRF with
shared_secret
as keythe 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.