# package cryptoverif

## Install

## Dune Dependency

## Authors

## Maintainers

## Sources

`sha256=e8de9daa77cb5ba3907c84e1ed4540219f9bc80fa029651d88cfb594c335011c`

`md5=44c641a07abb652e6299c7ac71a8945c`

## 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: 28 Jun 2022

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

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