README.md

Examples

This library holds worked examples: the security of authenticated encryption from ind-cca and int-ptxt, with its collision bound and its collision game (AuthenticatedEncryption); hardness and game hops in every instance of the games classes (Games); substitutions on interfaces (Substitution); PRG length extension, proved by the laws of one reply of memoryless systems (PRGLengthExtension); components, AES and an AEAD written in the DSL (DSL); and the proof commands on interfaces (Usability). Citations refer to the numbered references of THEORY.md.

Authenticated encryption

The security of authenticated encryption [9, Theorem 2.3.10(4)], corrected, is in Security. Let $R$ be the real system AE.Real, $E$ the encryption oracle Encryption.Real, and $I = \rho^{ae} E$ the ideal system (AE.Ideal • Encryption.Real): AE.Ideal, like AE.CTXT ($\rho^{ctxt}$), is a converter from AE M C to Encryption M C. Let $P$ and $C$ be the plaintext filter AE.PTXT and the random-message transformation AE.CCA, and $q = (q_e, q_d)$ the budgets per port. The corrected chain uses each assumption twice:

$$R \;\simeq_{\mathrm{ptxt}}\; P R \;\simeq_{\mathrm{cca}}\; P C R \;\simeq_{\mathrm{ptxt}}\; P C P R \;\simeq_{\mathrm{cca}}\; P C P C R \;\approx_{q_e^2 / \lvert \mathcal M \rvert}\; I .$$

The last step is the collision bound, which compares the hybrid with AE.Ideal.perPort • Encryption.Real.perPort (Collision). The results are the counted witness, with two uses of ind-cca and two of int-ptxt, the advantage form, and the distance form $\Delta(R, I) \le 2\,\Delta(R, P R) + 2\,\Delta(R, C R) + q_e^2 / \lvert \mathcal M \rvert$. The systems and the notions AE.INDCCA, AE.INTPTXT, AE.INTCTXT and AE.Secure are Commons definitions (AEAD); int-ctxt and ae read $R \simeq \rho^{ctxt} E$ and $R \simeq \rho^{ae} E$. The systems are compared as oracle automata (Oracle, Hybrid), each by a bisimulation of its compiled automaton: the real system, the encryption oracle, and the images under the plaintext filter, the random-message transformation and the ideal transformation.

Games

The examples are in Games. In every instance of Games: hardness through a reduction, two reductions and a lossy reduction, $W(G_1) \le k\, W(\alpha \cdot G_2) \le k\, \varepsilon$, the shape of a reduction that guesses one of $k$ sessions. In every instance of DistinctionGames: a game hop inside a construction, $\lvert D(\alpha\, G^-) - D(\alpha T) \rvert \le W(\alpha \cdot G)$ for $G \mathrel{|\!\equiv} T$. On interfaces, the collision game of authenticated encryption is the game the collision discrete game presents, with visible typed system the hybrid and conditionally equivalent to the ideal; every winner wins it with probability at most $q_e^2 / \lvert \mathcal M \rvert$, so every solver's advantage between the hybrid and the ideal is at most $q_e^2 / \lvert \mathcal M \rvert$, also inside any construction.

Substitutions on interfaces

Substitution gives single substitutions with a context on the right or on the left, and two statistical substitutions giving $\lbrace R \rbrace \xrightarrow{\pi,\ \varepsilon_1 + \varepsilon_2} \lbrace \sigma S \rbrace$.

DSL components

Components declares counters, fresh and persistent randomness, a padding converter with an inferred cost, the write-through cache typed by a partial port map, and a filter.

AES and AEAD in the DSL

AES and AEAD declare AES-256 as a system with a random key, from the Commons block cipher AES, with converters around it such as CBC-MAC; and AES-CTR followed by PMAC, from the Commons CTR and PMAC converters. The proof commands on interfaces are exercised in Usability.