CryptoVerif: Cryptographic protocol verifier in the computational model

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, Zagreb, Croatia, October 2021. Springer. To appear.
Long version:


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 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.

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 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.

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 shared_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 key

  • 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.

Reverse Dependencies