# Formal Security Proofs of Cryptographic Standards: A necessity achieved using EasyCrypt

Cécile Baritel-Ruet

► To cite this version:

Cécile Baritel-Ruet. Formal Security Proofs of Cryptographic Standards: A necessity achieved using EasyCrypt. Cryptography and Security [cs.CR]. Université Côte d'Azur, 2020. English. NNT: 2020COAZ4049. tel-03150443v2

HAL Id: tel-03150443

https://theses.hal.science/tel-03150443v2

Submitted on 23 Mar 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
UNIVERSITÉ
CÔTE D'AZUR

<figure><img src="image_2.png" /></figure>

ÉCOLE DOCTORALE
SCIENCES ET
TECHNOLOGIES DE
L'INFORMATION ET DE
LA COMMUNICATION

THÈSE DE DOCTORAT

Preuves Formelles de la Sécurité de
Standards Cryptographiques

Un objectif nécessaire, possible grâce à EasyCrypt

Cécile BARITEL-RUET

INRIA Sophia Antipolis

Présentée en vue de l'obtention du
grade de docteur en Informatique
d'Université Côte d'Azur.

Dirigée par : Yves BERTOT

Co-encadrée par :
Benjamin GRÉGOIRE

Soutenue le : 02/10/2020

Devant le jury, composé de :

Manuel Barbosa,
Yves Bertot,
Sandrine Blazy,
François Dupressoir,
Steve Kremer,
Benjamin Grégoire,
Bruno Martin
<figure><img src="image_3.png" /></figure>
Preuves Formelles de la Sécurité de
Standards Cryptographiques

Un objectif nécessaire, possible grâce à EasyCrypt

Jury :

Directeurs

Yves Bertot, Directeur de recherche, Inria Sophia Antipolis Méditerrannée

Benjamin Grégoire, Chargé de recherche, Inria Sophia Antipolis Méditerrannée

Rapporteurs

Sandrine Blazy, Professeur et Chercheur, Université de Rennes 1 et IRISA

Steve Kremer, Directeur de recherche, Inria Nancy

Examinateurs

Manuel Barbosa, Lecturer and Researcher, University of Porto and HASLab

François Dupressoir, Senior Lecturer, University of Bristol

Bruno Martin, Professeur et Chercheur, Université Côte d'Azur et I3S
<figure><img src="image_4.png" /></figure>
# Formal Security Proofs of Cryptographic Standards

## A necessity achieved using EasyCrypt

Jury :

Advisors

Yves Bertot, Research director, Inria Sophia Antipolis Méditerrannée
Benjamin Grégoire, Researcher, Inria Sophia Antipolis Méditerrannée

Rapporteurs

Sandrine Blazy, Lecturer and Researcher, Université de Rennes 1 and IRISA
Steve Kremer, Research director, Inria Nancy

Examiners

Manuel Barbosa, Lecturer and Researcher, University of Porto and HASLab
François Dupressoir, Senior Lecturer, University of Bristol
Bruno Martin, Lecturer and Researcher, Université Côte d'Azur et I3S
<figure><img src="image_5.png" /></figure>
## Résumé :

En cryptographie, Shannon a montré que le secret parfait n'existe pas. Ainsi, la cryptographie moderne considère des propriétés de sécurité dans lesquelles un attaquant peut briser l'algorithme cryptographique mais seulement avec une faible probabilité. Dans ce contexte, les algorithmes cryptographiques et les propriétés/hypothèses de sécurité sontprimés sous forme de programmes probabilistes. Les preuves de sécurité consistent à borner la probabilité d'un événement dans de tels programmes. Ces preuves sont difficiles à prouver et malgré le système de relecture académique des erreurs continuent d'être publiées. Nous proposons l'utilisation des preuves formelles pour assurer une fiabilité suffisante des standards cryptographiques.

Ma thèse fournit les preuves formelles de sécurité de trois standards dans l'assistant de preuve EasyCrypt. Ces schémas sont CMAC (qui fournit l'authentification et l'intégrité des messages), SHA-3 (une fonction de hachage cryptographique), et ChaCha20-Poly1305 (un schéma de chiffrement authentifié avec données associées). L'objectif de la thèse n'est pas seulement de formaliser la preuve de sécurité de ces standards, mais aussi de développer des techniques génériques et des bibliothèques qui peuvent être réutilisées. Toutefois, les preuves formelles de sécurité n'assurent que la sécurité des algorithmes et non de leurs implémentations. Pour contourner cette lacune, avec mes collaborateurs, nous lions formellement nos implémentations sûres et efficaces avec la preuve de sécurité, ceci conduit à la première preuve de sécurité cryptographique d'implémentations.

**Mots clés** : Cryptographie, Standards, Sécurité prouvable, EasyCrypt, Preuve formelle, CMAC, SHA-3, ChaCha20-Poly1305.
<figure><img src="image_6.png" /></figure>
**Title:** Formal Security Proofs of Cryptographic Standards

**Abstract:**

In cryptography, Shannon showed that perfect secrecy does not exist. Thus, modern cryptography considers security properties in which attackers may break the cryptographic algorithm only with a small (negligible) probability. In this context, cryptographic algorithms and security properties/assumptions are expressed as probabilistic programs. Security proofs consist of bounding the probability of an event in such programs. Such proofs have been peer-reviewed for some decades, but since they are difficult to prove and to verify, fallacies keep emerging. We propose to use formal proofs to provide enough trustworthiness for crypto-systems such as cryptographic standards.

My thesis provides the formal security proofs of three standards that are formally verified using the proof assistant EasyCrypt. The cryptographic standards I have worked on are CMAC (that provides message authentication and integrity), SHA-3 (a cryptographic hash function), and ChaCha20-Poly1305 (an authenticated encryption scheme with associated data). The goal of the thesis is not only to provide formal proof of those standards, but also to develop generic techniques and libraries that can be reused. However, the formal security proofs only ensure the security of the algorithms and not its implementation. To circumvent this gap, with my collaborators, we have developed fast and secure implementations of the last two schemes that are also side-channel resistant. Furthermore, we formally link the implementation with the security proof, leading to the first formal security proof of an implementated standard.

**Keywords:** Cryptography, Standards, Provable security, EasyCrypt, Formal proof, CMAC, SHA-3, ChaCha20-Poly1305.
<figure><img src="image_7.png" /></figure>
Remerciements — Acknowledgements

Je souhaite remercier en tout premier lieu mes deux directeurs, Yves Bertot et Benjamin Grégoire, pour leur temps, leur soutien et leurs conseils que vous avez su m'offrir pendant ces quatre années de travail ensemble.

Merci à toi Benjamin pour le soutien indéfectible et la bienveillance que tu as su témoigner durant notre travail ensemble. Merci de m'avoir posé toutes ces questions auxquelles je ne savais pas répondre immédiatement, m'enseignant beaucoup et en particulier cette compétence fort utile qu'est la prise de recul. Je te suis reconnaissante pour tes efforts de relecture, que j'espère savoir apprécier à leur juste valeur.

Merci à toi Yves pour ton humanité, tes conseils et ton écoute pendant toute la durée de ma thèse. Malgré la différence dans nos domaines d'expertise respectifs, nos échanges ont toujours été non seulement enrichissant, mais aussi ont contribué à la prise de recul sur mon domaine de recherche et le domaine de la recherche de manière générale. Plus particulièrement, merci pour ton soutien pendant ce confinement de mars à mai 2020.

I want to humbly thank my jury for accepting to review my work.

In particular, I am wholeheartedly grateful to both Sandrine Blazy and Steve Kremer, who dared to be rapporteurs, even though the health crisis and the summer break would leave them little time to read this manuscript and write their report.

Thank you, François Dupressoir, Manuel Barbossa, and Bruno Martin for showing enough interest in my work to participate in this jury.

Je tiens à remercier tous les membres de l'équipe Marelle — maintenant l'équipe Stamp — qu'ils soient permanents ou non. L'ambiance que vous avez su maintenir est à la hauteur du temps de la région : chaleureuse, agréable et humaine. Merci Laurence, pour ta gentillesse, tes conseils, ta bienveillance et ton énergie. Merci à Laurent pour ses conseils sur l'Agreg, même si je ne souhaite plus m'y diriger. Merci à Reynald pour toutes les inspirations que tu m'as données à propos de la constitution de ces remerciements. Merci à Sophie et Damien pour ces discussions entre doctorants toujours très intéressantes et enrichissantes, notamment sur l'éducation. Thank you, Anders, for the pleasant co-habitation at the office. Merci à Mohammad et Adam pour la bonne humeur qu'ils ont instaurée dans le bureau. Merci à Pierre pour ces discussions autour d'un (un ?) café. Merci à Cyril pour son point de vue rafraichissant et bienveillant. Merci à Maxime et Enrico pour avoir animé les repas du midi. Merci à Nathalie pour son soutien, son humanité, sa bonne humeur et sa bienveillance. Son travail nous soulage d'un poids administratif et je pense ne pas savoir mesurer son importance tant elle fait bien son travail pour qu'on ne le remarque pas. Merci pour sa trilogie, que j'attends avec impatience en version électronique. Je souhaite rendre hommage à José qui nous a quitté en 2019, on pense à lui.
Merci à tous ceux qui ont bien voulu m'écouter parler de ma recherche. Je tiens notamment à remercier les deux membres de mon comité de suivi doctoral, François Dupressoir et Cinzia Di Guisto, pour vos retours, vos encouragements et vos éclairements.

Merci aux enseignants Cinzia Di Guisto, Sid Touati et Étienne Lozes, pour m'avoir permis de travailler avec vous pour mon service en tant que chargé de TP/TD. Je tiens aussi à remercier mes élèves avec qui le contact humain lors de l'échange pédagogique a été source de beaucoup d'enthousiasme et de motivation pour moi.

Merci à Madtree pour cette discussion sur le cours de cryptographie sur Coursera, et dont la présente thèse en est le produit fortuit. Merci à Xavier Urbain pour son aide et son soutien pour poursuivre le parcours académique qui m'intéressait. Merci à Serge Haddad pour m'avoir présenté le second concours d'entrée à l'ENS de Cachan. Merci à Stéphanie Delaune pour son soutien et de m'avoir fait découvrir qui allait être mon encadrant de thèse. Merci à Pierre-Alain Fouque pour son co-encadrement de mon stage de M2 et que j'ai eu le plaisir de retrouver à Crypto 2019. Merci à Cristina Onete pour son soutien pendant ce stage, et pour m'avoir fait découvrir le workshop CrossFyre. Je tiens à remercier François Dupressoir qui m'a accueilli pour une visite juste après l'édition 2018 de CrossFyre. Merci à Pierre-Yves Strub pour son soutien pendant la demande de bourse de thèse et pour le travail commun pendant la thèse. Merci à Gilles Barthe pour sa ligne de recherche qui a été indirectement déterminante pour mon travail de recherche.

Enfin, je remercie tous ceux qui m'ont soutenu et encouragé. Merci en particulier à mes amis et ma famille, que j'ai peu vus ces dernières années à cause de la distance, mais qui comptent beaucoup pour moi et m'accueillent comme si je n'étais jamais partie.

Merci à Nicole, Pascal, Audrey, Nathanaël, le petit Maël (qui est arrivé le 17 mars 2020), Marthe, Joëlle, Pauline, Luca, Hervé, Catherine, Philippe, Rémy, Thomas, Ophélie, Djamal, Thomas, Élodie, Fabien, Louis, Charly, Pierre, Tristan, Amélie, Nicolas, Olivier, Karina, Stéphane, Daniel et aux autres que j'oublie. Merci à Ahri, ma chienne, qui a été d'une aide précieuse, en particulier pour continuer à sortir pendant le confinement.
# Contents

Page

Introduction 1

I Methodology 7

1 Practice-Oriented Provable Security 9

1.1 Provable Security Models 10

1.1.1 Random Oracle Model 11

1.1.2 Ideal Cipher Model 12

1.2 Limitations and Related Work 12

2 EasyCrypt and General Formalization Techniques 15

2.1 Foundations 15

2.1.1 Probability Distributions 16

2.1.2 Modules in EasyCrypt 17

2.2 Adversarial Model 23

2.2.1 Restrictions on Oracle Procedure Calls 24

2.2.2 Adversarial Restrictions on Program Variables 24

2.2.3 Computation Time Restrictions 25

2.3 Formalization Techniques 27

2.3.1 PRP-PRF switching lemma 27

2.3.2 Eager Sampling [Almeida et al., 2019b] 32

2.3.3 Split Random Oracle 34

II Message Authentication 39

3 Security of a MAC Scheme 41

3.1 Security Definition : Forgery Resistance 42

3.2 Indistinguishability from a Random Function implies Forgery Resistance 43

3.2.1 Forgery Resistance of a Random Function 43

3.2.2 Indistinguishability 44

3.3 Block Cipher Mode of Operation 46

3.3.1 Security Definition of a Block Cipher 47

3.3.2 Security Definition of a Block Cipher Mode of Operation 47

4 CMAC's Formal Security Proof [Baritel-Ruet et al., 2018] 49

4.1 Historical presentation 49
<table><tr><td>4.2</td><td>MAC Security Proofs</td><td>55</td></tr><tr><td>4.2.1</td><td>Indistinguishability of ECBC from a Random Function</td><td>56</td></tr><tr><td>4.2.2</td><td>Indistinguishability of FCBC from ECBC</td><td>59</td></tr><tr><td>4.2.3</td><td>Indistinguishability of XCBC from FCBC</td><td>60</td></tr><tr><td>4.2.4</td><td>Indistinguishability of CMAC from FCBC</td><td>62</td></tr></table>

## III Cryptographic Hash Function 69

<table><tr><td>5</td><td>Security of a Hash Function</td><td>71</td></tr><tr><td>5.1</td><td>Security Definitions and Formalization</td><td>71</td></tr><tr><td>5.2</td><td>Random Function Security</td><td>74</td></tr><tr><td>5.3</td><td>Indifferentiability, not indistinguishability</td><td>74</td></tr><tr><td>5.4</td><td>Security from Indifferentiability</td><td>76</td></tr></table>

<table><tr><td>6</td><td>SHA3's Formal Security Proof [Almeida et al., 2019b]</td><td>77</td></tr><tr><td>6.1</td><td>The SPONGE construction</td><td>80</td></tr><tr><td>6.2</td><td>Security Statement</td><td>81</td></tr><tr><td>6.3</td><td>Layered Indifferentiability</td><td>82</td></tr><tr><td>6.3.1</td><td>General Decomposition</td><td>83</td></tr><tr><td>6.3.2</td><td>First Layer: SPONGE (not part of my contributions)</td><td>84</td></tr><tr><td>6.3.3</td><td>Second Layer: BLOCKSPONGE</td><td>86</td></tr><tr><td>6.3.4</td><td>Core Layer: CORESPONGE</td><td>88</td></tr><tr><td>6.3.5</td><td>The final SPONGE simulator</td><td>90</td></tr><tr><td>6.4</td><td>A deeper look at the upto-bad game</td><td>91</td></tr></table>

## IV Confidentiality and Authentication 101

<table><tr><td>7</td><td>Security of Authenticated Encryption</td><td>103</td></tr><tr><td>7.1</td><td>Authenticated Encryption</td><td>103</td></tr><tr><td>7.2</td><td>Security Definitions</td><td>104</td></tr><tr><td>7.2.1</td><td>IND-CPA</td><td>105</td></tr><tr><td>7.2.2</td><td>IND-CCA1 and IND-CCA2</td><td>105</td></tr><tr><td>7.2.3</td><td>INT-CTXT: Integrity of the CipherTeXT</td><td>107</td></tr><tr><td>7.3</td><td>Relations between IND-CCA, IND-CPA and INT-CTXT</td><td>108</td></tr><tr><td>7.3.1</td><td>IND-CCA from IND-CPA and INT-CTXT</td><td>109</td></tr><tr><td>7.3.2</td><td>Ideal Encryption Scheme</td><td>110</td></tr></table>

<table><tr><td>8</td><td>ChaCha20-Poly1305's Formal Proof</td><td>113</td></tr><tr><td>8.1</td><td>Description of ChaCha20-Poly1305</td><td>114</td></tr><tr><td>8.2</td><td>Security of ChaCha20-Poly1305</td><td>115</td></tr><tr><td>8.2.1</td><td>Adversarial Model</td><td>116</td></tr><tr><td>8.2.2</td><td>Security Statement</td><td>117</td></tr><tr><td>8.3</td><td>Security Proof</td><td>117</td></tr></table>
Conclusion

127

List of Figures

129
<figure><img src="image_8.png" /></figure>
# Introduction

Whenever I speak about my PhD in a non-expert context, I start talking about computer security and I get simple but meaningful questions that resemble to: “Are you actually breaking into software to exploit vulnerabilities ?”, “Do you know about this threatening vulnerability X ?”, or “Which anti-virus should I install to protect my data ?”. This kind of questions belongs to one particular field of computer security where the focus is on breaking security, while I work in the field where the focus is on ensuring security.

In computer networks, data flows from places to places. Some of the data is sensitive and attackers like hackers or spies want to find an access through vulnerabilities of the data flow. The objective of computer security is to analyze the flow of data, to find vulnerabilities and place barriers to prevent intruders from accessing it. Some of those barriers come from cryptography and my work is to analyze the “robustness” of some particular barriers.

Cryptography prior to the modern age was actually synonymous with encryption, the conversion of information from a readable meaningful state to apparent nonsense. The originator of an encrypted message shares the decoding technique (the encryption and decryption algorithms and the secret key) only with intended recipients to preclude access from adversaries. Because the adversary cannot understand and know the content of the encrypted message, this is one way of how the barriers are implemented.

There are two ways to ensure security, either the secrecy depends on hiding both the algorithm and the secret key, or the algorithm is known to the adversary and only the secret key needs to be hidden. History has shown that the first one is not practical, and leads to greater security flows, as the amount of secret data to keep the secrecy is much larger if the algorithm is included. This was first explicitly stated as a fundamental principle in 1883 by Auguste Kerckhoffs [Kerckhoffs, 1883] and is generally called Kerckhoffs's Principle; alternatively and more bluntly, it was restated by Claude Shannon, the inventor of information theory and the fundamentals of theoretical cryptography in [Shannon, 1949]:

> The enemy knows the system.

Since the development of rotor cipher machines in World War I and the advent of computers in World War II, the methods used to carry out cryptology have become increasingly complex and its application more widespread. In recent decades, the field has expanded beyond confidentiality concerns to include techniques for message integrity checking, sender/receiver identity authentication, digital signatures, interactive zero-knowledge proofs and secure computation, among others, as shown in Figure 1.

Modern cryptography is heavily based on mathematical theory and computer science practice. Cryptographic algorithms, or more generally cryptosystems, are based on mathematical problems that are easy to state but have been found difficult to solve. If one can
<figure><img src="image_9.png" /><figcaption>Figure 1 – Cryptography: a field composed of various security goals and techniques</figcaption></figure>

reduce any *adversary* that efficiently breaks a cryptosystem into an efficient solution to a
hard mathematical problem, this means that breaking this cryptosystem is harder than find-
ing an efficient solution to this hard mathematical problem. This reasoning pattern is called
a *security reduction proof* (or *reduction*, or *security proof*) and is instrumental in the modern
approach to cryptography: *provable security* [Katz and Lindell, 2014].

We use a mathematical method for the basis of our work that includes the reduction of
the number of concepts, for instance by reducing the number of actors, the form of attacks,
and using probabilities. This approach makes explicit a simple model and is well accepted
in the community. For instance, the standardization institute NIST recommends: « The
review of technical merit includes a precise, formal statement of security claims, based on
minimal security assumptions and supported as far as possible by documented cryptanalysis
and security reduction proofs. » (NIST Cryptographic Standards and Guidelines Development
Process [Regenscheid, 2016])

Provable Security

Traditionally, provable security is asymptotic: it classifies the hardness of computational
problems using *polynomial-time reducibility*. Secure schemes are defined to be those in
which the *advantage* of any computationally bounded adversary to break the cryptosystem
is *negligible*. While such a theoretical guarantee is important, in practice one needs to know
exactly how efficient a reduction is because of the need to instantiate the *security parameter*
(e.g. key length). It is not enough to know that "sufficiently large" security parameters will
do. An inefficient reduction results either in the success probability for the adversary or the resource requirement of the scheme being greater than desired.

*Concrete security* is a practice-oriented approach [Bellare, 1997] that needs a more precise estimate of the computational complexity of adversarial tasks than polynomial equivalence would allow. Concrete security aims at quantifying an *upper bound* on the probability of any adversary to break the system studied. More precisely, a proof of security involves an upper bound on the advantage of the adversary to break the system as a function of adversarial resources and of the problem size. The resource available to the adversary are commonly *running time* and *memory*, and other resources specific to the system in question, such as the number of plaintexts it can obtain or the number of *queries* it can make to any available oracle. The problem size usually is the size of the key, but it can also include the size of blocks when blocks are defined in the system.

There are several lines of research in provable security. One is to establish the "correct" *definition of security* for a given, intuitively understood task. Another is to suggest possible solutions: cryptographic constructions and their security proofs. The cryptography community is confronted to the difficulty to produce correct proofs. Several researchers found mathematical fallacies in proofs; proofs that had been used to make claims about the security of important protocols. This is illustrated in the list below where the name of a cryptosystem is followed by the initial paper when it was claimed to be proven secure then by the reference in which the first fallacy was reported. For some of those constructions, successive corrections were also shown to be defective.

— OAEP [Bellare and Rogaway, 1994] [Shoup, 2002];

— HMQV [Krawczyk, 2005] [Menezes, 2007];

— CBC-MAC and EMAC [Bellare et al., 2005] [Jha and Nandi, 2016];

— Boneh-Franklin IBE [Boneh and Franklin, 2003] [Galindo, 2005];

— GCM [McGrew and Viega, 2004b] [Iwata et al., 2012];

— XLS [Ristenpart and Rogaway, 2007] [Nandi, 2014];

— RSA screening [Bellare et al., 1998b] [Coron and Naccache, 1999];

— XCB [McGrew and Fluhrer, 2007] [Chakraborty et al., 2015];

— Cascade encryption [Bellare and Rogaway, 2006] [Gaži and Maurer, 2009];

— RSA-FDH [Coron, 2002] [Kakvi and Kiltz, 2012];

— OCB2 [Rogaway, 2004a] [Inoue et al., 2019].

The scientific community thinks that for any claim the claimer should be the one to produce enough non-fallacious material to convince of the correctness of its logical arguments. The referring process is here to ensure that no wrong proof is accepted. However, the list above shows that this is not enough. Delegating the verification of a proof's correctness to a computer is a way to answer this issue. This is my second field of expertise which is part of the larger field of *formal verification*.

## Formal Verification

The verification of a mathematical proof is a tedious work, and as a lot of tedious works, this can be eased by the use of machines. This is well explained by Thomas C. Hales in his advocacy for formal proofs [Hales, 2008]:
Traditional mathematical proofs are written in a way to make them easily un-
derstood by mathematicians. Routine logical steps are omitted. An enormous
amount of context is assumed on the part of the reader. Proofs, especially in
topology and geometry, rely on intuitive arguments in situations where a trained
mathematician would be capable of translating those intuitive arguments into a
more rigorous argument.

A formal proof is a proof in which every logical inference has been checked all
the way back to the fundamental axioms of mathematics. All the intermediate
logical steps are supplied, without exception. No appeal is made to intuition,
even if the translation from intuition to logic is routine. Thus, a formal proof is
less intuitive, and yet less susceptible to logical errors.

Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their *specifications* (expected behavior defined by a mathematical property). Formal verification requires describing hardware and software systems in mathematical terms, at which point establishing claims about their correctness becomes a form of theorem proving.

*Interactive theorem proving* focuses on the verification aspect of theorem proving requiring that every claim is supported by a proof in a suitable axiomatic foundation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. HOL [Gordon, 1988], Isabelle [Paulson, 1994], PVS [Owre et al., 1992], Coq [Coq, 1984] and Lean [Lea, 2012] are some of the most well-known interactive theorem provers, also known as *proof assistants*.

Without minimizing nor dismissing their respective strengths, they primary work on
mathematical proofs and aim to reduce towards a minimum its axiomatic basis. My work in-
volves the game-based technique of provable security, a feature that is included in EasyCrypt,
a proof assistant introduced as a proof of concept to address the problem of the security of
OAEP [Barthe et al., 2011b]. It implements a model in which the game-based technique
and distributions (probabilities) set up an interactive theorem prover for the formalization
of concrete security bounds. I will describe EasyCrypt along with the methodology used for
security proofs in detail in the next part.

Cryptographers have the intuition of why a system is secure, but translating this intuition
into formal logical steps is a long and tedious work and requires expertise in both cryptogra-
phy and formal verification. Deductive verification has the disadvantage that it requires the
user to understand in detail how the system works exactly, and to convey this information
to the verification system. There exist a lot of cryptographic constructions and not so many
cryptographers are also versed into formal verification.

Contributions

My work aims at extending the number of formally proven secure schemes with two
objectives in mind:

1. for the sake of verifying concrete security bounds of cryptographic standards,

2. to extend the proof of concept into a proof of usability, so that formal verification with EasyCrypt may be included in the process of standardization.
This extension includes the formalization of the security proof of three different cryptographic standards, each of them answering a different security requirement. Because of the downsides of formalization efforts, we have intentionally prioritized cryptographic standards. Those standards are from either NIST, or the IETF (Internet Engineering Task Force).

My first contribution is the study of the formal security bound of a standard MAC (message authentication code) scheme named CMAC [Baritel-Ruet et al., 2018].

My second contribution is part of a joint work to produce a fast and secure implementation of a standard hash function named SHA-3 [Almeida et al., 2019b]. My personal contribution on this is situated in the formal security bound.

The third contribution presented in my manuscript is the study of the formal security bound of an authenticated symmetric encryption scheme named ChaCha20-Poly1305. This last work has not been published yet.

## Organization of this thesis

Part I explains the scientific methodology and is composed of two chapters.

- Chapter 1 explains in more details practice-oriented provable security, and the limits and controversies of provable security.

- Chapter 2 exposes EasyCrypt.

Part II explores the notion of message authentication with the study of the security of one standardized MAC scheme and is composed of two chapters.

- Chapter 3 explains what message authentication actually means and state the formal security definition of a MAC scheme.

- Chapter 4 explains the security proof of the standardized MAC scheme named CMAC.

Part III explores the notion of cryptographic hash function with the study of the security of one standardized hash function and is composed of two chapters.

- Chapter 5 states the formal security definition of a cryptographic hash function.

- Chapter 6 explains the security proof of the standardized hash function named SHA-3.

Part IV explores the notion of authenticated encryption with the study of the security of an authenticated encryption and is composed of two chapters.

- Chapter 7 states the formal security definition of an authenticated encryption.

- Chapter 8 explains the security proof of ChaCha20-Poly1305, an authenticated encryption scheme.
<figure><img src="image_10.png" /></figure>
# Part I

## Methodology
<figure><img src="image_11.png" /></figure>
# Chapter 1

## Practice-Oriented Provable Security

The security of a service is its ability to be resilient against potential risks. In providing a service, the goal is to maximize its usefulness while minimizing the risks associated with its use. This balance between risk and efficiency is essential in IT security. However, this is not up to cryptographers to provide such a balance in the use of a cryptosystem, but rather the “architect” of the service. Instead, the responsibility of the cryptographers is to provide sufficient analytical material to the “architect” so that the choice on which cryptosystems and their parameters should be based on an *informed one*.

The choice of such a cryptosystem can be guided by the fact that the longer the cryptosystem remains unattacked, the more secure it is believed to be. Before modern cryptography, the common practice was to find a particular attack on a cryptographic scheme, then update the scheme, and do it again (and again). This practice is tantamount to playing the cat and mouse game and reveals an empirical approach that is not sufficiently relevant for computer risk management. On the other hand, the scientific approach of *provable security* refers to mathematically proven security properties that quantify on *all* attacking strategies.

<figure><img src="image_12.png" /></figure>

### Remark

This paradigm shift in cryptography — from empirical to mathematically proven — was first introduced for public-key signature and encryption. The security of the famous public-key encryption RSA [Rivest et al., 1983] relies on the fact that any efficient adversary that can break the security of RSA can be turned into an efficient algorithm for factoring the product of two large random numbers, which is assumed to be a *hard* mathematical problem.

In his 1998 survey article, *Why chosen ciphertext security matters* [Shoup, 1998], Shoup explained the rationale for attaching great importance to reductionist security arguments:

> This is the preferred approach of modern, mathematical cryptography. Here, one shows with mathematical rigor that any attacker that can break the cryptosystem can be transformed into an efficient program to solve the underlying well-studied problem (e.g., factoring large numbers) that is widely believed to be very hard. Turning this logic around: if the hardness assumption is correct as presumed, the cryptosystem is secure. This approach is about the best we can do. If we can prove security in this way, then we essentially rule out all possible shortcuts, even ones we have not yet even imagined. The only way to attack the cryptosystem is a full-frontal attack on the underlying hard problem. Period.
Classical provable safety is mainly aimed at studying the *asymptotic* relationship between objects. Secure schemes are then defined as those in which any algorithm capable of breaking the cryptographic system can be asymptotically reduced to an algorithm that can solve a difficult mathematical problem. While such a theoretical guarantee is important, in practice it is necessary to know exactly how effective a reduction is because of the practical need to instantiate the security parameter. It is not enough for an informed choice to know that "sufficiently large" security parameters will suffice. Therefore, a reduction that is in polynomial time but in an ineffective way is reflected either in the probability of success for the adversary or in the resource requirements of the regime being greater than desired. As Rogaway stated in [Rogaway, 2009]:

> The provable-security approach begins by identifying the cryptographic problem of interest, an often ignored but crucial first step. Next, one gives a precise *definition* for the problem at hand. This entails identifying *what* the adversary can do and *when* it is deemed successful. A protocol is then given for problem, that protocol depending on some other, hopefully-simpler protocol for solving some other, hopefully-more-basic problem that has likewise been defined. Evidence of security for the high-level protocol takes the form of a *reduction*, the reduction showing how to transform an adversary attacking the high-level goal into one for attacking the low-level goal.

> [...] The association of an adversary to a real number is the *definition of security*.

The next sections are organized as follows.

- Section 1.1 introduces different models used in provable security.

- Section 1.2 discusses about limitations of provable security and its models, and then discusses related work.

# 1.1 Provable Security Models

A model for provable security defines “*what* the adversary can do” and the collection of assumptions and proof methods in which the reduction can be expressed.

Traditionally, cryptographic protocols are analyzed with the *Dolev-Yao* symbolic model [Dolev and Yao, 1983]. This model assumes perfect cryptography. Messages are assumed to be elements of some abstract algebra, and cryptographic primitives, such as encryption, are abstract operations on this algebra. In this model, the adversary can hear, intercept, and synthesize any message and is limited only by the constraints of the cryptographic method used. In other words, "the adversary carries the message." These messages consist of formal terms that may reveal part of their internal structure, but some parts remain opaque to the adversary. Modelled as a specific non-deterministic state machine, the only way for the adversary to extract this internal structure is to perform some of the operations on messages it already "knows".

This model has an extremely nice feature: simplicity, but has a disadvantage: Dolev-Yao's adversary is actually quite weak. Because the calculation model is symbolic and complete knowledge of the adversary can be computed, it is possible to explicitly represent all possible behaviors of the adversary in a compact way. Although he can choose among the allowed operations in a non-deterministic way, the set of allowed operations is fixed and quite small.
Therefore, the models are very well suited to be automatically analyzed to show that a protocol is broken, rather than secure, under the assumptions about the adversary's capabilities, e.g. [Dalal et al., 2010, Blanchet, 2013].

Dolev-Yao's symbolic model is often compared [Herzog, 2005] to the computational model [Goldwasser and Micali, 1984, Goldwasser et al., 1988, Yao, 1982], because the latter is much more realistic, but complicates the proofs. Instead of defining adversarial capabilities in the symbolic model, adversarial restrictions extend security claims to a larger set of adversaries. In the computational model, a cryptographic construction exchanges messages that are bitstrings from some distribution, an adversary is an arbitrary probabilistic algorithm with restrictions and primitives are modeled as (tuples of) algorithms that satisfy security and constructive assumptions (e.g. decryption and encryption are inverse to each other).

The computational model in which the adversary is limited only by time and computing power is called the *standard model*. Schemes whose safety can be proven using only complexity assumptions are said to be *secure in the standard model*. Proofs of security are known to be difficult to achieve in the standard model. In many proofs, cryptographic primitives are replaced by idealized versions.

In the next two subsections, I detail two other computational models used in the formal security proofs I have worked on, namely the *random oracle model* and the *ideal cipher model*.

### 1.1.1 Random Oracle Model

A *random oracle* is an *oracle* — a theoretical black-box — that answers to every fresh query with a truly random response chosen from the uniform distribution on its output domain. Random oracles are typically used as an ideal replacement for cryptographic hash functions (see Chapter 5) where strong randomness on its output domain is needed. In the *random oracle model*, a random oracle is assumed to exist and be accessible to the adversary. In [Bellare and Rogaway, 1995], Bellare and Rogaway were the first to advocate their use in cryptographic constructions. In their definition, the random oracle produces a bit-string of infinite length which can be truncated to the desired length. However, the formalization of such a random oracle would raise problems such as how to sample a value uniformly from the output set $\{0, 1\}^\infty$. Therefore, a random oracle is formalized to either set the output type to be finite or the random oracle waits for a second input: the desired length<fnref n="1" />.

Such a model has its own limitations. In [Impagliazzo and Rudich, 1989], Impagliazzo and Rudich showed that the existence of a random oracle alone is not sufficient for a secure exchange of secret keys. Moreover, if a cryptographic construct proves to be secure in the standard model, attacks against this construct must either be outside the behaviour of the adversary considered in the model or break one of the assumptions. For example, if the proof is based on the hardness of the factorization of large integers, in order to break it, a fast integer factorization algorithm must be discovered. Instead, to break the random oracle hypothesis, one must only discover an unknown and undesirable property of the current hash function. For a good hash function when such properties are deemed unlikely or difficult to discover by computation, the intended cryptographic construct remains secure.

Furthermore, consider a cryptographic construction built using a hash function that has a security proof in the random oracle model. Even though some hash function is found to be broken, e.g. SHA-1 [Stevens et al., 2017], the cryptographic construction remains secure in the sense that one only has to change the hash function to restore security. In

<footnote n="1">1. see Chapter 6 for more details</footnote>
other words, the difficulty to find a secure hash function does not affect the overall security of the cryptograhpic construction that has a proof in the random oracle model.

1.1.2 Ideal Cipher Model

An ideal cipher is a random permutation oracle that is used to model an idealized block
cipher (see Chapter 3). A random permutation decrypts each ciphertext block into one and
only one plaintext block and vice versa, so there is a one-to-one correspondence. Some
cryptographic proofs give to the adversary also access to the reverse permutation.

<figure><img src="image_13.png" /></figure>

Remark

Recent works showed that an ideal cipher can be constructed from a finite ran-
dom oracle using Feistel networks, with 10 rounds [Dachman-Soled et al., 2016] or 8
rounds [Dai and Steinberger, 2016a].

1.2 Limitations and Related Work

When cryptographers publish their security analysis, often as a security proof, a non-
specialist is very unlikely to read (or even think about) the proof, hoping to find some in-
structions about how to implement the cryptosystem. This involves a certain trust in security
proofs from non-specialist communities about their credibility. Since security proofs are left
aside, the responsibility of cryptographers is to strive for clarity in security statements, in-
cluding the theoretical model, meaning of all parameters, and all assumptions (security
assumptions, independance assumptions, access granted or banned to oracles, etc...).

The promise of quantifiable proof of safety on each adversarial strategy is attractive and
tight security statements are great tools to enable practitioners to make informed choices,
when they are sufficiently clear. For this reason, one of the emphasis of this manuscript is
about clear security statements and proof models. However, clarity does not guarantee the
correctness of the proof of security, as shown in the next two examples.

<figure><img src="image_14.png" /></figure>

Example

In [McGrew and Viega, 2004b], the AES-GCM authenticated encryption scheme was proven secure. Eight years after [Iwata et al., 2012], the proof was found to have some fallacies and the authors gave a procedure to break the first security bound, without contradicting the overall security of AES-GCM. Indeed, they also proposed a repaired security proof with a worse security bound than the incorrect one.

<figure><img src="image_15.png" /></figure>

Example

In [Inoue et al., 2019], they found a fallacy in the security proof of OCB2, leading to a very dangerous and powerful attack on this authenticated encryption still in use. They propose a fix for OCB2, and argue that OCB1 and OCB3 do not share this flaw.
As Stern, Pointcheval, Malone-Lee, and Smart [Stern et al., 2002] reported:

> Methods from provable security, developed over the last twenty years, have been recently extensively used to support emerging standards. However, the fact that proofs also need time to be validated through public discussion was somehow overlooked. [...] the use of provable security is more subtle than it appears, and flaws in security proofs themselves might have a devastating effect on the trustworthiness of cryptography.

This is not to claim that the correctness of a proof is a problem that stems from the limits of provable safety. However, the impact on real systems that rely on the correctness of security proofs can be extremely detrimental, as in the case of OCB2 [Inoue et al., 2019]. Instead, my thesis tackles this problem using *formal proofs* which gives a stronger guarantee that the proof is correct, increasing the confidence non-specialists may have in cryptosystems, when the clarity of the security statement is emphasized.

The application of formal proofs on reductionist arguments also has its limitations in terms of the cost of such an analysis. They involve the time necessary to analyse a cryptosystem and expertise in two different fields of computer science. This is a huge cost on time and expertise, therefore an emphasis should be made when this effort is reasonably expectable. A potential candidate would be the process of standardization (e.g. SHA-3 [Kayser, 2007], see Chapter 6), or in the process of a competition that aims to determine the best cryptosystem, e.g. the CEASAR competition [CAE, 2013].

I also argue that for each security property about each cryptosystem, only a single formal proof is needed. Indeed, once a result has been formally proven using a proof assistant, this result can be trusted — at least until a flaw is found in the proof assistant. For this reason, one could argue that a proof assistant is as trustworthy as a cryptographer, if not less. However, pen-and-paper proofs are much more sensible to intuition shortcuts that may lead to a fallacy. The constant requirement to formalize all of the logical steps of every intuition is still a fastidious effort, but on the other side it gives the opportunity to deeply understand the reductionist argument and all of the assumptions made about the cryptosystem.

<figure><img src="image_16.png" /></figure>

**Example**

> When a proof assistant is implemented so that composition of cryptosystems is possible, assumptions on independence of components are checked along the way, which in practice are even hardly looked at. For instance, in a hybrid system that uses a cryptosystem — also used elsewhere — to generate the key of another cryptosystem, no guarantee about the security of the combination is provided, even if each primitive is provably secure and their parameters are set so that security requirements are met. A security proof of the combination needs to be provided (see Chapter 8).

This discussion remains in the field of the study of the security of cryptographic algorithms. The final purpose of provable security and security proofs is to guarantee the real security of a cryptosystem's implementation, not just of its algorithm.

Even the computational model is just a model that ignores many important aspects of reality. In particular, it ignores physical attacks against devices: side-channel attacks that may exploit for instance power consumption, timing, noise and fault attacks — an attack that introduces faults in the system in order to break its security from provoking unexpected behaviour. As cryptosystems are better studied and verified formally, physical attacks become
increasingly important and are an area of active research. Some of my collaborators have worked in this direction, producing the Jasmin programming language whose « compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. » ([Almeida et al., 2017])

In [Almeida et al., 2019b], we propose both a formal security proof and an efficient implementation of the SHA-3 hash function family:

Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. [...] Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks.

In [Almeida et al., 2019a], my collaborators propose a fast and side-channel secure implementation of the authenticated encryption ChaCha20&Poly1305. In Chapter 8, I propose a formal security proof of ChaCha20&Poly1305, that is functionally equivalent to their implementation in Jasmin.
# Chapter 2

## EasyCrypt and General Formalization
Techniques

The interactive theorem prover EasyCrypt was first presented in [Barthe et al., 2011a] as an implementation of a *code-based game-based* approach to practice-oriented provable security in the computational model. It diverged from CertiCrypt [Barthe et al., 2009], a Coq framework used to prove the formal semantic security of OAEP.

This chapter gives a general presentation of EasyCrypt, states clearly *what an adversary can do* (i.e. adversarial strategies included in the security statements), and regroups formalization techniques that are used in the different proofs.

### 2.1 Foundations

EasyCrypt is a proof assistant that relies on the *goal directed proof* approach. Also described in [Bertot, 2006] for Coq, this approach usually has the following type of scenario:

1. the user enters a statement that he wants to prove (using the command lemma) along with a name for later reference,

2. the EasyCrypt system displays the formula as a formula to be proved, possibly giving a context of local facts that can be used for this particular proof,

3. the user enters a command to decompose the goal into simpler ones, ideally upto axioms or formula that evaluate to true,

4. the EasyCrypt system displays a list of formulas that still need to be proven,

5. back to step 3.

The commands used at step 3 are called *tactics*. Some of these tactics actually decrease the number of goals. When there are no more goals, the proof is complete. When the user enters the command qed, the lemma is saved with the name given at step 1.

Before stating a lemma to prove, the user may define the structures he will work on, some axioms he assumes, or import libraries that contain such definitions. For that, EasyCrypt has a typed expression language based on the polymorphic typed lambda calculus. In EasyCrypt, *types* are non-empty sets of values and *operators* are typed functions on these sets. The internal kernel of EasyCrypt provides basic built-in types such as *bool*, *int*, *real*, and *unit* (the type inhabited by the single element `tt` or `()`). The standard libraries includes formalization of lists, arrays, sets, finite sets, maps, finite maps, distributions, etc....
<figure><img src="image_17.png" /></figure>

**Remark**

In EasyCrypt, an integer n can be recast to the real type using the notation n%r.

<figure><img src="image_18.png" /></figure>

**EasyCrypt**

The polymorphic option type encapsulates an optional value. A value of type α option is either Some x where x is of type α, or None.

type α option = [ None | Some of α ].

The operator oget extracts the optional value by associating to the value None a default value named witness in EasyCrypt (as mentioned above, all types are inhabited).

op oget [α] (o : α option) : α =

with o = None ⇒ witness

with o = Some a ⇒ a.

The system of *theory* in EasyCrypt allows the user to regroup related types, predicates, operators, modules, axioms, and lemmas. EasyCrypt allows users to declare and specify their data-types and operators, including inductive data-types and operators defined by pattern matching. Types and operators without definitions are said *abstract* and can be seen as *parameters* to the rest of the context. Theory parameters (types, operators, and predicates) left abstract when proving its lemmas may be instantiated via a *cloning process*. For instance, theory cloning allows the development of generic proofs that can later be instantiated with concrete parameters.

<figure><img src="image_19.png" /></figure>

**EasyCrypt**

Axioms can restrict parameters and are discharged during particular instanciation.

op σ : int.

axiom σ_gt0 : 0 < σ. (* we assume that σ is positive *)

2.1.1 Probability Distributions

To every type t is associated the type t distr of real discrete sub-distribution . In some cases, we may use the notation D (t) to express the set of all sub-distributions on a type t. A discrete sub-distribution over a type t is fully defined by its mass function . A mass function f is a non-negative function from t to R and is defined over a discrete support while verifying:

$$
\sum_{x:t} f(x) \le 1
$$

<figure><img src="image_20.png" /></figure>

**EasyCrypt**

When the sum is equal to 1, the sub-distribution is called a *distribution* and the keyword for this assumption is *is_lossless*.

type t.

op dt : t distr.

axiom dt_\_ll : is\_lossless dt.
When the mass function of the sub-distribution is positive over all of the elements of type t, the sub-distribution is said to be full.

**axiom** dt_full : is_full dt.

When the mass function of the sub-distribution associates every value of the support of the sub-distribution to the same mass, the sub-distribution is said to be *uniform*.

**axiom** dtUniform : isUniform dt.

The keyword for a sub-distribution that is full and uniform is `is funiform`.

**axiom** dtFuniform : isFuniform dt.

The mass function of a sub-distribution is represented by the operator `mu1`, while `mu` `dt` `P` represents the mass of the set of all values that satisfy the proposition `P`. In fact, internally, `mu1` is defined using the operator `mu`.

**op** mu : t distr → t prop → real.

**op** mu1 (dt : t distr) (x : t) : real = mu dt (**fun** y ⇒ x = y).

## 2.1.2 Modules in EasyCrypt

Programs are formalized in EasyCrypt as *modules*: stateful “objects” consisting of *global variables* and *procedures*. Global variables are visible outside the modules and define the internal state of the module at any given time. A procedure is composed of the declarations of local variables and a sequence of *instructions*. An instruction can be an assignment, a random sampling (denoted by $\leftarrow$), a call to another procedure (possibly obtaining the return value), a conditional branch, a while loop, or a return statement. This simple imperative probabilistic programming language is named **pWhile**.

<figure><img src="image_21.png" /></figure>

### EasyCrypt

This exemple defines a module with one global variable `Multiply.factor`, and defines one procedure `Multiply.mul` that outputs the product of its input to its global variable.

```python
module Multiply = {
    var factor : int (* global variable *)
    proc mul (n : int) : int = {
        (* factor refers to Multiply.factor *)
        return n * factor;
    }
}
```

The module system in EasyCrypt manages higher-order modules. This feature allows a cryptographer to define a general game by taking an adversary and a cryptosystem as parameters. Before declaring a game that takes some modules as parameters, a *module type* needs to be defined for each different type of parameter.

<figure><img src="image_22.png" /></figure>

### EasyCrypt

In this example, the module type `Oracle` declares the interface of the cryptosystem, `Adversary` declares the interface of the adversary, and the module `Game` defines the cryptographic game when given an adversary and a cryptosystem.
module type Oracle = {
  proc init () : unit
  proc f (_: int) : bool
}.

module type Adversary (O : Oracle) = {
  proc guess () : bool
}.

module Game (A : Adversary) (O : Oracle) = {
  proc main () : bool = {
    var b : bool;
    O.init();
    b ← A(O).guess();
    return b;
  }}.

## Probability of some event in a game

Formally, an instruction operates on program *memories*, which map local and global variables to values. Let $\mathcal{M}$ be the set of memories.

<figure><img src="image_23.png" /></figure>

### EasyCrypt

A memory is handled differently from other types. For instance, anonymous functions (fun ($x : t$) $=>$ ...) and operators cannot take memories as input, while quantification on memories is allowed. The quantification $\forall \&m$ ranges over all memories with domain equal to the set of all variables declared as global in currently declared modules. For instance, with those declarations:

module X = { var a : int }.

module Y = { var b : int }.

the following formula is well-formed and evaluates to true:

$$ \forall \&m, X.a\{m\} < Y.b\{m\} \Rightarrow X.a\{m\} + 1 \le Y.b\{m\} $$

An *event* is a boolean expression over non-free logical variables and program variables that are tagged with a memory. If $&m$ is a memory and $x$ is a program variable in the domain of $&m$, then $x \langle m \rangle^1$ is the expression for the value of $x$ in $&m$, and $\psi \langle m \rangle$ is the expression where all the program variables occurring in $\psi$ are replaced with their value in $&m$.

The semantics of a sequence $c$ of instructions is a function $[[c]] : \mathcal{M} \to \mathcal{D}(\mathcal{M})$ from program memories to sub-distributions on program memories. If one possible execution of $c$ does not terminate, $c$ generates a sub-distribution with total probability less than 1. The probability of some *event* $\psi$ in a program $c$ when starting with initial memory $&m$ is defined as the sum of the masses of all memories in the distribution $[[c]] \langle m \rangle$ that satisfy $\psi$:

$$ \Pr[c, m : \psi] $$

The EasyCrypt notation $\Pr[c@&m : \psi]$ is equivalent to $\Pr[c, m : \phi]$, the latter being more readable and the former more accurate to what EasyCrypt is expecting.

## Adversary as a module, Quantification over all adversaries

Adversaries are modeled in EasyCrypt as *abstract modules* of a defined module type. The module type defines the type of procedures, but the code of an abstract module is unknown.

<footnote n="1">1. This notation has been chosen for text readability, even if $x\{m\}$ is the notation used in EasyCrypt</footnote>
<figure><img src="image_24.png" /></figure>

## EasyCrypt

An abstract module is declared locally using quantification over a module type: $\forall$ (A <: Adversary). Another way to declare an abstract module is using inside a section the declare module feature of EasyCrypt. The system of *sections* has the primary goal to hide intermediate details of a proof. Inside a section, which may be named, an abstract module can be declared so that all lemmas that appear in the section will appear with a supplementary quantification. In the following, some notations have not been described so far, but they are not relevant for the EasyCrypt notion of *sections*, so we explain them in the following sections.

Imagine the following example of a lemma that is declared in a section in a context with the module Game declared as follows and with a defined (but not presented) module O : Oracle.

```haskell
module Game (A : Adversary) (O : Oracle) = {
  var i : bool
  proc main () = {
    A(O).guess();
    i $← {0,1};
  }.
}
```

**section** Proof.

**declare module** A : Adversary.

**axiom** A_II : ( ∀ (O1 <: Oracle{A}),

islossless O1.f ⇒ islossless A(O1).guess.

**lemma** toto &m : Pr [ Game(A,O).main() @ &m : Game.i = true ] = 1%r / 2%r.

**end section** Proof.

When used outside of the section, the lemma toto looks like:

**lemma** toto : ∀ (A <: Adversary),

( ∀ (O1 <: Oracle{A}), islossless O1.f ⇒ islossless A(O1).guess) ⇒

∀ &m, Pr [ Game(A,O).main() @ &m : Game.i = true ] = 1%r / 2%r.

<figure><img src="image_25.png" /></figure>

## Remark

In the previous example, the procedure A(O).guess may call all procedures of O, but EasyCrypt features restrictions on which procedures can be queried. This point is described in more details in Section 2.2.2.

<figure><img src="image_26.png" /></figure>

## Remark

Consider a module A declared with module type Adversary. Its procedures may be referred to (in lemmas, judgments, or code) only when an oracle O is provided. The procedure A(O).guess is correct, whereas A.guess is not well-formed.

EasyCrypt allows the user to reason about three different types of facts about probabilistic programs. They are called *judgments* and each type specifies what it actually means for the programs:

- HL, *Hoare Logic*, with probabilistic programs,

- pHL, *probabilistic Hoare Logic*, that allows one to carry out proofs about the probability of a procedure's execution resulting in a post-condition holding, and

- pRHL, *probabilistic Relational Hoare Logic*, that relates a pair of procedures.
## Hoare Logic

A Hoare judgment is a triplet $[c : \phi \Rightarrow \psi]$ composed of a (probabilistic) program c and two predicates $\phi$ and $\psi$. It states that for all memory &m satisfying the precondition $\phi$, then all memories in the support of the sub-distribution $[[c]] \langle m \rangle$ satisfy the post-condition $\psi$. When the program c is deterministic, $[[c]] \langle m \rangle$ has a support of at most one element.

<figure><img src="image_27.png" /></figure>

### EasyCrypt

The main tactic for an abstract procedure call is the tactic named proc. Consider a Hoare judgment $[A(O).g : \phi \Rightarrow \psi]$ in the context of an abstract procedure named A(O).g of the abstract module A that takes a module O as parameter. The tactic proc takes one input: a formula I that represents an invariant.

One constraint needs to be checked for the tactic proc to work: A *should have no write access to any global variable that appears in I*. The intuition is that the rule for the adversary is analogous to the rule with the loops. If each iteration keeps the validity of the invariant, and the invariant is valid before the loop, then the full loop respects the invariant. Unspecified code with oracle access to some procedures is analogous to a “loop” that “iterates” on oracle calls, with some code between calls.

The rule checks that the unspecified code of the procedure A(O).g cannot modify the invariant I, and asks to prove that each oracle call which A(O).g can query respects the invariant. The procedures accessible by A(O).g are from the module type of A.

$$ \frac{\forall f \text{ accessible procedure by } A(O).g, [O.f : I \Rightarrow I]}{[A(O).g : I \Rightarrow I]} [\text{proc I}] $$

## Probabilistic Hoare Logic

A probabilistic Hoare judgment is a quintuplet $[c : \phi \Rightarrow \psi] \diamond p$ composed of a program c, two predicates $\phi$ and $\psi$, a relation on reals $\diamond$ taken from the set $\{\leq, =, \geq\}$, and a real $p$. It states that $\forall \& m, \phi \langle m \rangle \Rightarrow \text{Pr}[c, m : \psi] \diamond p$.

<figure><img src="image_28.png" /></figure>

### EasyCrypt

A very useful tactic in the context of a pHL statement about a sequence of instructions $[c_1; c_2 : \phi \Rightarrow \psi] \diamond p$ is the tactic named seq i : b p_1 p_2 p_3 p_4 l. The arguments mean:

i: the line number that specify the beginning of c_2,

b: a boolean formula that may be evaluated to true or false,

p_1: the probability that b holds at the end of c_1, i.e. $[c_1 : \phi \Rightarrow b] \diamond p_1$,

p_2: the probability that $\psi$ holds after c_2 if b holds, i.e. $[c_2 : l \land b \Rightarrow \psi] \diamond p_2$,

p_3: the probability that b does not hold at the end of c_1, i.e. $[c_1 : \phi \Rightarrow \neg b] \diamond p_3$,

p_4: the probability that $\psi$ holds after c_2 if b does not hold, i.e. $[c_2 : l \land \neg b \Rightarrow \psi] \diamond p_4$,

l: a property always satisfied at the end of c_1, regardless of the evaluation of b, i.e. $[c_1 : \phi \Rightarrow l]$.

When applied, the tactic also asks the user to prove the goal: $p_1 p_2 + p_3 p_4 \diamond p$.
## Probabilistic Relational Hoare Logic

A probabilistic relational Hoare judgment<fnref n="2" /> is a quadruplet $[c_1 \sim c_2 : \phi \Rightarrow \psi]$ composed of two programs $c_1$ and $c_2$, and two relations $\phi$ and $\psi$. More specifically, the precondition $\phi$ and post-condition $\psi$ are first-order formulate built from relational expressions that are then interpreted as a relation on program memories.

Whereas for HL and pHL judgments only one memory is considered, a pRHL judgment distinguishes between the two memories for each side. Therefore, relational expressions are arbitrary boolean expressions over program variables tagged with $\langle 1 \rangle$ or $\langle 2 \rangle$ (to specify from which of the programs they are from: $\langle 1 \rangle$ for $c_1$, $\langle 2 \rangle$ for $c_2$) and logical variables that only appear when quantified. By abuse of notation, $e \langle i \rangle$ stands for the expression $e$ in which all program variables have been tagged with $\langle i \rangle$.

### EasyCrypt

The notation for the equality of a program variable X.x in both memories is $=\{X.x\}$, and the notation $=\{X.x, Y.y\}$ stands for $=\{X.x\} \land =\{Y.y\}$. For any module M, the set of all the variables a module accesses is denoted glob M. The precondition $=\{\text{glob A}\}$ is particularly useful for an abstract module A when one wants to state that it will have the same behavior in both memories.

A pRHL judgment $[c_1 \sim c_2 : \phi \Rightarrow \psi]$ states that for any pair of initial memories $m_1, m_2$ satisfying the precondition $\phi$, denoted $\langle m_1, m_2 \rangle \vdash \phi$, the distributions $\llbracket c_1 \rrbracket \langle m_1 \rangle$ and $\llbracket c_2 \rrbracket \langle m_2 \rangle$ satisfy the lifting $\mathcal{L}$ of post-condition $\psi$, denoted $\langle (\llbracket c_1 \rrbracket \langle m_1 \rangle), (\llbracket c_2 \rrbracket \langle m_2 \rangle) \rangle \vdash \mathcal{L}(\psi)$. The lifting of a relation on memories to a relation on memory distributions is defined as a max-cut min-flow problem, in the style of [Jonsson et al., 2001]. Formally, let $\mu_1 \in \mathcal{D}(A)$ be a probability distribution on a set A and $\mu_2 \in \mathcal{D}(B)$ a probability distribution on a set B. The lifting $\langle \mu_1, \mu_2 \rangle \vdash \mathcal{L}(R)$ of a relation $R \subseteq A \times B$ to $\mu_1$ and $\mu_2$ is defined as follows:

$$ \exists \mu : \mathcal{D}(A \times B), \pi_1(\mu) = \mu_1 \land \pi_2(\mu) = \mu_2 \land \forall (a, b) \in A \times B, \mu(a, b) > 0 \Rightarrow \langle a, b \rangle \vdash R $$

where the projections $\pi_1(\mu)$ and $\pi_2(\mu)$ are defined as

$$ \pi_1(\mu)(a) \stackrel{\text{def}}{=} \sum_{b \in B} \mu(a, b) $$

$$ \pi_2(\mu)(b) \stackrel{\text{def}}{=} \sum_{a \in A} \mu(a, b) $$

Claims about probabilities can be derived from valid pRHL judgments by means of the following rules:

$$ \frac{\langle m_1, m_2 \rangle \vdash \phi \quad [c_1 \sim c_2 : \phi \Rightarrow \psi] \quad \forall \& m'_1, \& m'_2, \langle m'_1, m'_2 \rangle \vdash \psi \Rightarrow (E_1 \langle m'_1 \rangle \Leftrightarrow E_2 \langle m'_2 \rangle) \quad \text{[PrEq]} \\ \text{Pr}[c_1, m_1 : E_1] = \text{Pr}[c_2, m_2 : E_2] $$

$$ \frac{\langle m_1, m_2 \rangle \vdash \phi \quad [c_1 \sim c_2 : \phi \Rightarrow \psi] \quad \forall \& m'_1, \& m'_2, \langle m'_1, m'_2 \rangle \vdash \psi \Rightarrow (E_1 \langle m'_1 \rangle \Leftrightarrow E_2 \langle m'_2 \rangle) \quad \text{[PrLe]} \\ \text{Pr}[c_1, m_1 : E_1] \le \text{Pr}[c_2, m_2 : E_2] $$

<footnote n="2">2. This description is from [Barthe et al., 2011a], in which more details can be found.</footnote>
EasyCrypt

The tactic proc also exists in pRHL. It is used to relate two instances of the same
abstract procedure A(·).g that may use different implementations of its oracles. The
tactic takes one input: a relation I that represents an invariant. The invariant should
not include any global variable that may be overwritten by the abstract module A (same
as for HL).

This tactic formalizes the intuition that the abstract procedure will have the same
behavior with both implementations and preserve the invariant I if the abstract module
starts with the same global state and, for every procedure, both implementations stay
in relation by the invariant I while answering the same output for the same query.

$$
\frac{\forall f \text{ accessible procedure by A, } [O1.f \sim O2.f : I \wedge =\{arg\} \Rightarrow I \wedge =\{res\}] \text{ [proc I]} \\ [A(O1).g \sim A(O2).g : I \wedge =\{arg, glob A\} \Rightarrow I \wedge =\{res, glob A\}]]}{[A(O1).g \sim A(O2).g : I \wedge =\{arg, glob A\} \Rightarrow I \wedge =\{res, glob A\}]} \text{ [proc I]}
$$

Remark

When an equivalence of two events in each program is lifted to relate those two
programs, then, from the definition of the projections, both must have the same termi-
nation probability. This is particularly important for the theorem about failure events
that is explained in the next paragraph.

EasyCrypt

The EasyCrypt keyword islossless is a predicate on a procedure that states that for
all input, the procedure terminates with probability 1, i.e.

$$
\text{islossless } O.f := \text{"[O.f : true} \Rightarrow \text{true]} = \text{"1"
$$

Failure Event

A relation between games defines a transition of equivalent games in a cryptographic
security proof. However, games are not always equivalent, and a lossy transformation may
be needed. One common technique to justify such a lossy transformation is to annotate both
games with a fresh boolean flag (often named bad) that is initialized to the false value and
set to true whenever the code of games differ. Such transitions are justified using the Fun-
damental Lemma, first used and introduced in [Shoup, 2004, Bellare and Rogaway, 2006].

**Lemma 2.1.1 (Fundamental Lemma [Barthe et al., 2010])**. For any pair of games $G_1, G_2$ and events $E_1, E_2$, and B, such that $E_1$ is well-defined in $G_1$, $E_2$ in $G_2$, and B in both games:

$$
\Pr[G_1, m : E_1 \land \neg B] = \Pr[G_2, m : E_2 \land \neg B] \\
\Rightarrow |\Pr[G_1, m : E_1] - \Pr[G_2, m : E_2]| \le \max(\Pr[G_1, m : B], \Pr[G_2, m : B])
$$

When an adversary is involved in both games, then one more assumption is needed: the
adversarial computation should terminate with probability 1 in at least one game. Assuming
that $G_1$ terminates with probability 1, then $\Pr[G_2, m : B] \le \Pr[G_1, m : B]$. In this case, the
upper bound on the loss of the transition is quantified by $\Pr[G_1, m : B]$.
EasyCrypt

The assumption on the termination of adversarial code is generalized in EasyCrypt; it requires the adversary to end with probability 1 with any terminating oracles. Such an hypothesis should be manually added whenever it is required.

The following axiom is an example using the module types of Section 2.1.2:

declare module A : Adversary.
axiom A_II : ∀ (O <: Oracle{A}),
            islossless O.init ⇒ islossless O.f ⇒
            islossless A(O).guess.

EasyCrypt

The tactic proc can also be applied for an upto-bad reasoning that relates the same abstract procedure with different implementations of its oracles. The tactic proc B I J takes three inputs — a failure event B (defined in the right implementation), the invariant I that holds as long as B does not hold, and the invariant J that holds when B holds. The tactic proc B I is a shortcut for proc B I true.

To prove the conclusion C, EasyCrypt creates the sub-goals $H_1, H_2, H_3, H_4$:

$H_1$ The adversary always terminates if its oracles terminate:

$$ \forall (O <: Oracle\{A\}), (* \forall f *) \text{islossless } O.f \Rightarrow \text{islossless } A(O).g $$

$H_2$ Assuming the failure event B does not hold before a query, the relation at the end of the query depends on the occurrence of the failure event:

$$ \forall f \text{ procedure, } [O1.f \sim O2.f : \neg B(2) \wedge =\{arg\} \wedge I \implies \text{if } B(2) \text{ then } J \text{ else } =\{res\} \wedge I] $$

$H_3$ If the failure B event has already occurred, then, in the left implementation, the relation J remains true with probability 1 even when the right memory is fixed:

$$ \forall f \text{ procedure, } \forall \& m_2, B(m_2) \Rightarrow [O1.f : J(\cdot, m_2) \implies J(\cdot, m_2)] = 1 $$

where the event $J(\cdot, m_2)$ is the predicate: $\&m \to (m, m_2) \vdash J$.

$H_4$ The failure event B in the right implementation remains true with probability 1:

$$ \forall f \text{ procedure, } [O2.f : B \implies B] = 1 $$

C If all those conditions are provable, this use case for the tactic proc makes it possible to prove the following goal:

$$ [A(O1).g \sim A(O2).g : =\{arg, \text{glob } A \wedge I\} \implies \text{if } B(2) \text{ then } J \text{ else } =\{\text{res, glob } A\} \wedge I] $$

## 2.2 Adversarial Model

All security statements in my manuscript rely on the same definition of adversaries based on the EasyCrypt adversarial model. Therefore, any strategy that cannot be captured in this
model is not captured by the security statements. Some restrictions on adversaries are local to the security statements, but are expressed using the same terminology.

Cryptographic security statements are expressed by quantifying on all adversaries. In EasyCrypt, this quantification is done using abstract modules and module types. Therefore, all algorithms that may be expressed as an EasyCrypt module that satisfy all the restrictions of the security statement are captured by the quantification.

## 2.2.1 Restrictions on Oracle Procedure Calls

In the implementation of an oracle, some of its procedures are used to initialize its internal state. This kind of procedure is meant to be accessible to the game from the security definition, but not to the adversary. This kind of restriction can be achieved either using different module types between the adversary's oracles and the game's oracles or by restricting the oracle procedures allowed to query directly in the module type of an adversary.

<figure><img src="image_29.png" /></figure>

### EasyCrypt

In the following example, any module A: Adversary should have a procedure named guess that may only call the procedures f and g of its oracle O. Therefore, a module with a procedure guess that calls its oracle's procedure init is not of module type Adversary.

```python
type f_input, g_input, f_output, g_output.
module type Oracle = {
    proc init() : unit
    proc f (x : f_input) : f_output
    proc g (x : g_input) : g_output
}
module type Adversary (O : Oracle) = {
    proc guess() : bool { O.f, O.g }
}
```

## 2.2.2 Adversarial Restrictions on Program Variables

In EasyCrypt, *program variables* may be *local* to a procedure or *global* to the full scope. Local program variables are inaccessible to any other procedure other than the one in which they are defined. In a security game, the adversary should not be able to access some global variables, e.g. the secret key of an encryption scheme. This is expressed in EasyCrypt when an abstract module is declared either in a quantification or in a section using `declare module`.

Some tactics require the declared abstract module to have no access on global variables that appear in the invariant, e.g. the `proc` tactic and all its declinations. This kind of restriction is possible when the abstract module is declared.
EasyCrypt

In the following example, the adversary A on which the property is quantifying over should never use the global variable Enc.key, either reading or overwriting its content.

type key.
module Enc {
  var key : key
  proc (* ... *)
}.
lemma security : ∀ (A <: Adversary { Enc }),
  (* some property *).

In the case of a module declared inside a section, new modules may be implemented after this declaration. The local keyword binds the implementation of a module inside a section and states that any abstract module previously declared may have no access to its global variables. For instance, the two following scripts are equivalent in meaning, except that in practice the module O is hidden in the left script when applying any lemma from the section.

section.

declare module A : Adversary.

local module O : Oracle = { var c : int }.

end section.

module O : Oracle = { var c : int }.

section.

declare module A : Adversary { O }.

end section.

Remark

This feature restricts all accesses, both for reading and writing. If one may want an abstract module to have reading access to a global variable without being able to alter it, direct access to the global variable should remain restricted in the declaration of the abstract module. Then, provide to the module type another oracle which outputs the value of the desired global variable, this acts like a “getter”. This concept can be extended to the inclusion of a “setter”.

2.2.3 Computation Time Restrictions

Usually, in cryptography, adversaries are *probabilistic polynomial-time* (PPT) algorithms<fnref n="3" />, i.e. their running time is upper bounded by a polynomial expression in the size of the input of the algorithm, also named *security parameter* in cryptography.

*Security statements* are usually of the form:

$$
\forall \mathcal{A} \text{ PPT}, \exists \mathcal{B} \text{ PPT}, \text{Adv}_{\mathcal{X}}^{\text{xxx}}(\mathcal{A}) \le \alpha + \text{Adv}_{\mathcal{Y}}^{\text{yyy}}(\mathcal{B})
$$

while security assumptions are usually:

$$
\forall \mathcal{B} \text{ PPT}, \text{Adv}_{\mathcal{Y}}^{\text{yyy}}(\mathcal{B}) \text{ is "negligible" in the security parameter.}
$$

<footnote n="3">3. Complexity is also bounded in terms of computation space, but we do not discuss it here.</footnote>
<figure><img src="image_30.png" /></figure>

**Remark**

The PPT property for adversarial algorithms is important for the “negligibility” of the bound. Often in cryptography, a negligible bound is about (or less than) $2^{-80}$. Of course, this is dependent on the risks and security goals of particular applications.

<figure><img src="image_31.png" /></figure>

**EasyCrypt**

Computation time, for example number of processor clock cycles, is not embedded in the logics of EasyCrypt but can be modeled using, for example, ghost variables that simulates computation times. Since adversaries can be any module of the specified module type, security statements are expressed in EasyCrypt without PPT restriction:

$$ \forall \mathcal{A}, \mathrm{Adv}_{\mathcal{X}}^{\mathrm{xxx}}(\mathcal{A}) \leq \alpha + \mathrm{Adv}_{\mathcal{Y}}^{\mathrm{yyy}}(\mathcal{B}(\mathcal{A})) $$

with a concrete implementation of $\mathcal{B}(\cdot)$ from $\mathcal{A}$ that needs to be checked so that:

$$ \forall \mathcal{A}, \mathcal{A} \text{ is PPT} \Rightarrow \mathcal{B}(\mathcal{A}) \text{ is PPT.} $$

<figure><img src="image_32.png" /></figure>

**Example**

In certain games, there may exist a non-PPT adversary C that has a non-negligible advantage $\mathrm{Adv}_{\mathcal{Y}}^{\mathrm{yyy}}(\mathcal{C})$. For instance, consider the case of any scheme that relies on the difficulty in finding the decomposition in prime factors of a large number, e.g. RSA, or the discrete logarithm, e.g. ElGamal. There exists a non-PPT adversary decomposing a large number into prime factors: the one that tests every prime inferior to the input number for divisibility. This adversary has the maximum advantage because it always succeeds. However, this cannot be considered to be a successful attack, since it would take too much time and effort because of the (sub-)exponential complexity.

When analyzing the security of a cryptosystem, adversarial computation time can be restricted indirectly. For instance, a common restriction is to bound the number of queries an adversary can make, where oracle queries formalize the computation of cryptographic primitives. In those cases, the bound on the number of query calls often appears in the security statement and the security bound. Counting queries may be more complex and such an example is shown in Chapter 6.

<figure><img src="image_33.png" /></figure>

**EasyCrypt**

To summarize what an adversary can do:

- It is a probabilistic program, expressible in EasyCrypt as a module from the given module type.

- It has access to some oracles (accessible procedures).

- It is restricted in the internal states it can access and interfere with.

- Its computation space is *unbounded*.

- Its computation time is *unbounded*. If the proof involves an upto-bad argument, it should terminate with probability 1 for any implementation of its oracles.
## 2.3 Formalization Techniques

In the following chapters of my manuscript, I describe security proofs of three cryptographic standards. In those proofs, a few formalization techniques are often used, and I choose to gather them in this autonomous section so that each proof can be followed on its own, without pointing to another security proof.

### 2.3.1 PRP-PRF switching lemma

In game-based proofs, it is often useful to switch between a random permutation and a random function (see Chapter 4 and Chapter 6). This section starts with the definition of a random permutation and a random function. Then I describe their formalization in EasyCrypt and state the PRP-PRF switching and the strong PRP-PRF switching lemmas.

<figure><img src="image_34.png" /></figure>

**Remark**

This formalization has been done time and time again (in [Affeldt et al., 2007, Barthe et al., 2010], to only cite a few formalizations), and is not part of my personal contribution. However, this is a good introduction to the techniques of EasyCrypt.

Let $S$ be a finite set, $Perm(S)$ the set of all permutations over $S$, and $Fun(S)$ be the set of all functions over $S$. In this context, the sampling $p \leftarrow \text{Perm}(S)$ means sampling a random permutation $p$ uniformly from the set of all permutations. Respectively $f \leftarrow \text{Fun}(S)$ means sampling a random function $f$ uniformly from the set of all functions.

<figure><img src="image_35.png" /></figure>

#### EasyCrypt

The formalization in EasyCrypt of a random permutation and a random function uses modules that are defined over an abstract type `t` that represents the set `S` and an abstract distribution operator `dt` that represents the uniform distribution over the finite abstract type `t`.

The module `Map` declares the finite map of the oracle that is visible by the adversary. The module type `Oracle` defines the expected oracle interface.

type `t`.

op `dt`: `t` distr.

axiom `dt_II`: `is_lossless` `dt`.

axiom `dt_funi`: `is_funiform` `dt`.

Listing 2.1 – Abstract parameters.

module `Map` = { var `m`: `(t, t)` `fmap` }.

module `type Oracle` = {

proc `init ()`: `unit`

proc `f (_: t)`: `t`

}

The predicate `rng Map.m` `x` is true if the element `x` is in the range of the finite map `Map.m`. The distribution `dt \ rng Map.m` is the uniform distribution over the set of elements in `S` that do not validate the predicate `rng Map.m`.
```hml
module RF : Oracle = {
    proc init () : unit = { Map.m ← empty; }
    proc f (x : t) : t = {
        if (x \ notin Map.m) {
            Map.m[x] $← dt;
        }
        return oget Map.m[x];
    }}.
```

<caption>Listing 2.2 – Random function</caption>

```hml
module RP : Oracle = {
    proc init () : unit = { Map.m ← empty; }
    proc f (x : t) : t = {
        if (x \ notin Map.m) {
            Map.m[x] $← dt \ rng Map.m;
        }
        return oget Map.m[x];
    }}.
```

<caption>Listing 2.3 – Random permutation</caption>

The indistinguishability advantage is bounded by a formula that involves the maximum number of oracle calls it can make. Indeed, if the adversary can query all values of the domain of its oracle, it has a high probability to distinguish between RP/RF. This restriction is formalized in the following module named Count.

```hml
op c : int.
```

```hml
module Count (E : Oracle) : Oracle = {
    var counter : int
    proc init () : unit = {
        counter ← 0;
        E.init();
    }
    proc f (x : t) : t = {
        var y : t ← witness;
        if (counter < c) {
            y ← E.f(x);
            counter ← counter + 1;
        }
        return y;
    }}.
```

An adversary may not (re-)initialize its oracle. This is either done by restricting procedure accesses in the declaration of the procedures, or by declaring another module type for oracles. The second option requires module type management and is possible, but may be tedious.

```hml
module type Adversary (O : Oracle) = {
    proc guess () : bool { O.f }
}.
```

The distinguishing game Dist, when given an adversary and an oracle, initializes the oracle and the counter, gives to the adversary the restricted oracle, and outputs the answer of the adversary.

```hml
module Dist (A : Adversary) (O : Oracle) = {
    proc main () : bool = {
        var b:
            Count(O).init();
        b ← A(Count(O)).guess();
        return b;
    }}.
```

**Lemma 2.3.1 (PRP-PRF switching).** For any natural number $c$, any lossless adversary $\mathcal{A}$ distinguishes a random permutation from a random function with probability:

$$ \left| \Pr\left[ \pi \stackrel{\$}{\leftarrow} \text{Perm}(S); b \leftarrow \mathcal{A}^\pi : b = 1 \right] - \Pr\left[ f \stackrel{\$}{\leftarrow} \text{Fun}(S); b \leftarrow \mathcal{A}^f : b = 1 \right] \right| \le \frac{c \cdot (c-1)}{2 \cdot |S|} $$

when the oracle starts to always output a default value witness after $c$ queries.

**lemma prp_prf_switching &m :**

(* $\forall$ adversary $A$ that cannot access internal states of Map and Count *)

$\forall$ ($A \prec$: Adversary { Map, Count }),

`| Pr[Dist(A,RP).main() @ &m : res] - Pr[Dist(A,RF).main() @ &m : res] | \le`
$(c*(c-1)/2) * \text{mu dt witness.}$

(* 'mu dt witness' represents the probability a value sampled from 'dt' is equal to 'witness' *)

*Proof.* Let &m be the initial memory, and Event.bad be the failure event.

module Event = { var bad : bool }.

This proof has a simple sequence of games:

1. $\mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RP}).\mathrm{main()} , m : \mathrm{res}] = \mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RPbad}).\mathrm{main()} , m : \mathrm{res}]$

2. $\mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RF}).\mathrm{main()} , m : \mathrm{res}] = \mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RFbad}).\mathrm{main()} , m : \mathrm{res}]$

3. $|\mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RFbad}).\mathrm{main()} , m : \mathrm{res}] - \mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RPbad}).\mathrm{main()} , m : \mathrm{res}]| \le \mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RFbad}).\mathrm{main()} , m : \mathrm{Event.bad}]$

4. $\mathrm{Pr}[\mathrm{Dist}(A, \mathrm{RFbad}).\mathrm{main()} , m : \mathrm{Event.bad}] \le c \cdot (c-1)/(2 \cdot |S|)$

where the oracles RFbad and RPbad are defined in the following way and are respec-
tively equivalent to RF and RP while capturing the failure event directly in their code.

module RFbad : Oracle = {
proc init () : unit = {
  Map.m ← empty;
  Event.bad ← false;
}
proc f (x : t) : t = {
  var y : t ← witness;
  if (x \ notin Map.m) {
    y ← $ dt;
    if (rng Map.m y) {
      Event.bad ← true;
      (* y ← $ dt | rng Map.m; *)
    }
    Map.m[x] ← y;
  }
return oget Map.m[x];
}}.

module RPbad : Oracle = {
proc init () : unit = {
  Map.m ← empty;
  Event.bad ← false;
}
proc f (x : t) : t = {
  var y : t ← witness;
  if (x \ notin Map.m) {
    y ← $ dt;
    if (rng Map.m y) {
      Event.bad ← true;
      y ← $ dt \ rng Map.m;
    }
    Map.m[x] ← y;
  }
return oget Map.m[x];
}}.

1. The functional equivalence between RF and RFbad is easy to show in EasyCrypt.

2. The functional equivalence between RP and RPbad relies on the fact that sampling from either of the following distributions yields the same probability:

- sample directly from 'dt \ rng Map.m' and

- sample from 'dt', then if the value belongs to the range of 'Map.m', re-sample another value from 'dt \ rng Map.m'.

3. The upto-bad step is a direct application of the Fundamental Lemma.

4. The computation of the probability of setting Event.bad ← true is done using the advanced tactic named fel for which a documentation can be found online at https://www.easycrypt.info/documentation/refman.pdf. This tactic captures the intuition that if the adversary has a limited number of queries it can
make, if the probability of the event for one query is bounded by some expres-
sion, then the probability the adversary triggers the event is bounded by the sum
of all those expressions.

<figure><img src="image_36.png" /></figure>

Stronger version

The stronger version of this theorem, used in Chapter 6, gives to the adversary an access to the inverse. Because the inverse of a random function is not defined on elements (but mathematically on sets), it is replaced it by a random transformation. It is formalized as a module with an internal state that keeps track of all previous queries to both the direct oracle and its inverse, and for any fresh query to either samples an output and updates its internal state. This last step may overwrite a previous query to the other oracle, therefore, a random transformation does not ensure the full consistency of the output of previous queries.

Because of this instability of behavior, the set of all transformations is not well defined.
Therefore, by abuse of notation, in the next lemma the sampling $f \leftarrow Fun(S)$ represents the
initialization of a random transformation, given to the adversary along with its “inverse”
$f^{-1}$, and whose internal state is updated as the adversary asks its queries.

<figure><img src="image_37.png" /></figure>

EasyCrypt

The formalization of the random transformation involves two finite maps that keep track of all the queries, one for the direct oracle Map.m and one for its inverse Map.mi.

Both maps are updated for each indi-
vidual query, and in the case of the ran-
dom transformation, no check is made
to ensure the consistency of the output
of previous queries.

module Map = {
  var m : (t, t) fmap
  var mi : (t, t) fmap
};
module type Oracle = {
  proc init () : unit
  proc f (_: t) : t
  proc fi (_: t) : t
};

module Count (O : Oracle) = {
  var counter : int
  proc init () : unit = {
    counter ← 0;
    O.init();
  }
  proc f (x : t) : t = {
    var y : t ← witness;
    if (counter < c) {
      y ← O.f(x);
    }
    counter ← counter + 1;
    return y;
  }
  proc fi (x : t) : t = {
    var y : t ← witness;
    if (counter < c) {
      y ← O.fi(x);
    }
    counter ← counter + 1;
    return y;
  }}.
```hml
module RT : Oracle = {
  proc init () : unit = {
    Map.m ← empty;
    Map.mi ← empty;
  }
  proc f (x : t) : t = {
    var y : t;
    if (x \ notin Map.m) { y ←$ dt; }
    Map.m[x] ← y;
    Map.mi[y] ← x;
    return y;
  }
  proc fi (x : t) : t = {
    var y : t;
    if (x \ notin Map.mi) { y ←$ dt; }
    Map.m[y] ← x;
    Map.mi[x] ← y;
    return y;
  }}.
```

<caption>Listing 2.4 – Random transformation</caption>

The definition of the adversarial module type and the game are close, but they differ in the set of procedures the adversary can call from its input module. In this example, the adversary can call both O.f and O.fi.

```hml
module RP : Oracle = {
  proc init () : unit = {
    Map.m ← empty;
    Map.mi ← empty;
  }
  proc f (x : t) : t = {
    var y : t;
    if (x \ notin Map.m) { y ←$ dt \ rng Map.m; }
    Map.m[x] ← y;
    Map.mi[y] ← x;
    return y;
  }
  proc fi (x : t) : t = {
    var y : t;
    if (x \ notin Map.mi) { y ←$ dt \ rng Map.mi; }
    Map.m[y] ← x;
    Map.mi[x] ← y;
    return y;
  }}.
```

<caption>Listing 2.5 – Random permutation</caption>

```hml
module type Adversary (O : Oracle) = {
  proc guess () : bool { O.f O.fi }
}.
```

```hml
module Dist (A : Adversary) (O : Oracle) = {
  proc main () : bool = {
    var b;
    Count(O).init();
    b ← A(Count(O)).guess();
    return b;
  }}.
```

**Lemma 2.3.2 (Strong PRP-PRF switching).** For any natural number $c$, any lossless adversary $\mathcal{A}$ can distinguish a random permutation from a random transformation with probability:

$$ \left| \Pr\left[ \pi \stackrel{\$}{\leftarrow} \text{Perm}(S); b \stackrel{\mathcal{A}, \pi, \pi^{-1}}{\leftarrow} b = 1 \right] - \Pr\left[ f \stackrel{\$}{\leftarrow} \text{Fun}(S); b \stackrel{\mathcal{A}, f, f^{-1}}{\leftarrow} b = 1 \right] \right| \\ \le \frac{c \cdot (c-1)}{2 \cdot |S|} $$

when its oracle starts to always answer a default value witness after $c$ queries.

**lemma strong_prp_prf_switching &m :**

$$ \forall (A < : \text{Adversary} \{ \text{Map}, \text{Count} \}), $$

$$ \left| \Pr[\text{Dist}(A, \text{RP}).\text{main}() @ \&m : \text{res}] - \Pr[\text{Dist}(A, \text{RT}).\text{main}() @ \&m : \text{res}] \right| \le \frac{(c*(c-1)/2) * \text{mu}}{2} \text{ witness.} $$
The proof of the stronger version of the PRP-PRF switching lemma is very similar and has the same structure as previously.

### 2.3.2 Eager Sampling [Almeida et al., 2019b]

Eager sampling is a standard argument when working with random oracles in cryptographic proofs, which consists in switching between two different views of a random oracle:

i. an *eager* view, in which the random oracle is sampled at random in a distribution over the space of functions (of the appropriate type) when the game is initialized; and

ii. a *lazy* view, in which the random oracle's responses are individually sampled upon fresh requests.

Although it is clear that no adversary that can only query the random oracle can distinguish between these two views, this restriction is often much too strict for the argument to be applicable directly.

<figure><img src="image_38.png" /></figure>

**Example**

In Section 6.3.2, the step in the proof that states that padding and truncation preserve indifferentiability, boils down to proving that the oracles E and L shown on the outside of Figure 2.1 cannot be distinguished — when instantiated with a random oracle RF with domain $D \times \mathbb{N}$ and range $\{0, 1\}$ — by any algorithm (even unbounded) with oracle access to one of them. Note here that it is impossible to simply eagerly sample the random oracle RF, since its domain is countably infinite, preventing us from defining a uniform distribution over the function space.

$E(x \in D, n \in \mathbb{N})$

$z \leftarrow \varepsilon;$

for ($i = 0; i < n; i++$)

$z \leftarrow z \parallel \text{RF}.\text{get}(x, i);$

for ($i = n; i < \lfloor n/r \rfloor \cdot r; i++$)

RF$.\text{get}(x, i);$

return $z$;

$H^0(x \in D, n \in \mathbb{N})$

$z \leftarrow \varepsilon;$

for ($i = 0; i < n; i++$)

$z \leftarrow z \parallel \text{O}.\text{get}(x, i);$

for ($i = n; i < \lfloor n/r \rfloor \cdot r; i++$)

O$.\text{sample}(x, i);$

return $z$;

$L(x \in D, n \in \mathbb{N})$

$z \leftarrow \varepsilon;$

for ($i = 0; i < n; i++$)

$z \leftarrow z \parallel \text{RF}.\text{get}(x, i);$

return $z$;

<caption>Figure 2.1 – Eager-lazy random sampling example.</caption>

Rather than forcing the EasyCrypt user to use low-level tactics to reason about this equivalence, we define a new abstraction for random oracles that supports eager arguments, not only in situations like the one of Figure 2.1 (where definitional difficulties arise from the use of infinite domains), but also in the presence of programming queries, such as scenarios in which answers to some queries are deterministically set or removed by the context.

Our new abstraction models a random oracle with input in set D, output in C, and output distribution $d_C$ as 4 oracles that share state, and whose canonical eager and lazy implementations are shown in Figure 2.2. They differ only in their sample oracle: an eager implementation (shown on a grey background), which samples values even though they are not returned; and a lazy implementation, which does nothing.
<figure><img src="image_39.png" /><figcaption>Figure 2.2 – The eager and lazy programmable random oracle</figcaption></figure>

Even given this much extended interface (over the “traditional” interface which only exposes `get`), we can prove the following lemma, which states that the eager and lazy implementations are strictly equivalent.

**Lemma 2.3.3** (Eager sampling for programmable random oracles). For any map $m_0 \in D \to C$, and for any unbounded adversary $\mathcal{D}$ with unbounded oracle access to `get`, `set`, `rem` and `sample` oracles as specified above, we have

$$ \mathcal{D}^{\text{Eager}}_{m_0} \sim \mathcal{D}^{\text{Lazy}}_{m_0} $$

Proving this lemma makes heavy use of EasyCrypt's advanced eager tactic which can be found online at https://www.easycrypt.info/documentation/refman.pdf. This tactic formalizes and confirms the standard intuition that, even when oracles can be externally programmed, sampling operations whose results do not influence the adversary's view can safely be delayed, either until the point where they do influence the adversary's view, or until the end of the game's execution.

<figure><img src="image_40.png" /></figure>

**Example**

Continuing our example, the extended interface can be used as shown in Figure 2.1 to define a hybrid oracle $H^0$ that uses `O.sample` as well as `O.get` for $O \in \{\text{Eager}, \text{Lazy}\}$. Then $E$ and $H^{\text{Eager}}$ are equivalent, since their second loops do nothing with the values they sample: both oracles sample $\lfloor n/r \rfloor \cdot r$ bits, returning the first $n$ of them. Also $H^{\text{Lazy}}$ is equivalent to $L$, since the second loop in $H^{\text{Lazy}}$ does nothing. Finally, if $\mathcal{D}$ is a distinguisher for $E/L$, then by Lemma 2.3.3, we have that $\mathcal{D}^E \sim \mathcal{D}^{H^{\text{Eager}}} \sim \mathcal{D}^{H^{\text{Lazy}}} \sim \mathcal{D}^L$, considering the distinguisher $\mathcal{D}^H$ when applying Lemma 2.3.3.

<figure><img src="image_41.png" /></figure>

**Remark**

In the previous Section, the sampling $p \stackrel{\$}{\leftarrow} \text{Perm}(S)$ represents the full-eager sampling whereas the EasyCrypt lemma involves the lazy representations of a random per-
mutation and a random function. From this section, those representations are equiva-
lent and one can switch between the two as much as one's will.

2.3.3 Split Random Oracle

A random oracle is a useful tool that cryptographers manipulate in the random oracle model. Common random oracle manipulations involve splitting the domain of the random oracle separated by a predicate, or splitting the co-domain when the output type is isomorphic to a pair. We have developed this simple yet useful library for Chapter 8.

Split Domain

In the situation of all calls to a random oracle that satisfy a predicate test may be delayed
and the rest may stay as is, the best way to delay such queries is to split the domain according
to the predicate test and then use the previous library to delay the wanted ones.

<figure><img src="image_42.png" /><figcaption>Figure 2.3 – Split domain</figcaption></figure>
<figure><img src="image_43.png" /></figure>

The abstract theory named SplitDom implements this idea. It uses the same interface (module types) as the lazy-eager theory named PROM (and described in Section 2.3.2). It provides two random oracles (named ROT and ROF) and the module `RO DOM`.

abstract theory SplitDom.
type from, to, input, output.
op sampleto : from → to distr.
clone import PROM.Ideal as IdealAll with
type from ← from,
type to ← to,
type input ← input,
type output ← output,
op sampleto ← sampleto.
module RO = PROM.RO.
clone IdealAll.MkRO as ROT.
clone IdealAll.MkRO as ROF.

Represented in Figure 2.3, the module `RO DOM` builds a full domain random oracle from two random oracles separated by predicate named test. Specifically it redirects queries:

`RO DOM[ROT,ROF].get(x)` will either output `ROT.get(x)` if `x` satisfies test, or output `ROF.get(x)` otherwise.

op test : from → bool.
module RO DOM(ROT:RO, ROF:RO): RO = {
    proc init () = { ROT.init(); ROF.init(); }
    proc get(x : from) = {
        var r;
        if (test x) r ← ROT.get(x);
        else r ← ROF.get(x);
        return r;
    }
    proc set(x : from, y : to) = {
        if (test x) ROT.set(x, y);
        else ROF.set(x, y);
    }
    proc rem(x : from) = {
        if (test x) ROT.rem(x);
        else ROF.rem(x);
    }
    proc sample(x : from) = {
        if (test x) ROT.sample(x);
        else ROF.sample(x);
    }
}.

The more general lemma states that any game using `RO DOM[ROT,ROF]` is equivalent to the same game using a direct random oracle `RO`. The following lemma is a pRHL equivalence of procedures:

section PROOFS.
declare module D: IdealAll.RO_Distinguish { RO, ROT.RO, ROF.RO }.
lemma RO_split:
equiv [ IdealAll>MainD(D,RO).distinguish
    ~ IdealAll>MainD(D,RO DOM(ROT.RO,ROF.RO)).distinguish
    : = {glob D, x}
⇒ = {res, glob D} ∧ RO.m{1} = union_map ROT.RO.m{2} ROF.RO.m{2} ∧
    (∀ x, x ∈ ROT.RO.m{2} ⇒ test x) ∧
    (∀ x, x ∈ ROF.RO.m{2} ⇒ ¬test x)].
proof. (* ... *) qed.

The corolary `pr_RO_split` is in the form of equality of probabilities, where some of the information about the relations between the finite maps is lost.

lemma pr_RO_split (p: glob D → output → bool) &m x0:
    Pr[ MainD(D,RO).distinguish(x0) @ &m : p (glob D) res] =
    Pr[ MainD(D,RO DOM(ROT.RO,ROF.RO)).distinguish(x0) @ &m : p (glob D) res].

proof. by byequiv RO_split. qed.

end section PROOFS.

end SplitDom.
## Split co-domain

When the output type to of a random oracle is isomorphic to a pair of two different types, to1 and to2, one may want to split the random oracle into the pairing of two uncorrelated random oracles with output type to1 and to2, respectively. This co-domain split allows cryptographers to delay (or erase) one of them, making the proof of an upper bound on some event easier, as in Chapter 8.

<figure><img src="image_44.png" /><figcaption>Figure 2.4 – Split co-domain</figcaption></figure>

<figure><img src="image_45.png" /></figure>

EasyCrypt

The abstract theory SplitCodom implements this idea. It uses the same interface for module types as the theory PROM and provides two sub theories cloned from PROM, named I1 and I2.

```haskell
abstract theory SplitCodom.
type to1, to2.
op topair : to -> to1 * to2.
op ofpair : to1 * to2 -> to.
axiom topairK: cancel topair ofpair.
axiom ofpairK: cancel ofpair topair.
op sampleto1 : from -> to1 distr.
op sampleto2 : from -> to2 distr.
axiom sample_spec (f:from) :
    sampleto f =
    dmap (sampleto1 f `*` sampleto2 f) ofpair.
```

```haskell
clone PROM.Ideal as I1 with
    type from ← from,
    type to ← to1,
    type input ← input,
    type output ← output,
    op sampleto ← sampleto1.
```

```haskell
clone PROM.Ideal as I2 with
    type from ← from,
    type to ← to2,
    type input ← input,
    type output ← output,
    op sampleto ← sampleto2.
```

```haskell
module RO_Pair(RO1:I1.RO, RO2:I2.RO): RO = {
    proc init () = { RO1.init(); RO2.init(); }
    proc get(x : from) = {
        var r1, r2;
        r1 ← RO1.get(x);
        r2 ← RO2.get(x);
        return ofpair(r1,r2);
    }
    proc set(x : from, y : to) = {
        var y1, y2;
        (y1,y2) ← to pair y;
        RO1.set(x,y1); RO2.set(x,y2);
    }
    proc rem(x : from) = {
        RO1.rem(x); RO2.rem(x);
    }
    proc sample(x : from) = {
        RO1.sample(x); RO2.sample(x);
    }.
};
```
The more general lemma states that any game using `RO_pair[I1.RO, I2.RO]` is equivalent to the same game using a direct random oracle `RO`. The following lemma is a pRHL equivalence of procedures:

**section PROOFS.**

**declare module D : RO_Distinguish { RO, I1.RO, I2.RO } .**

**lemma RO_split:**

equiv [ MainD(D,RO).distinguish
  ~ MainD(D,RO_Pair(I1.RO,I2.RO)).distinguish
  : = {glob D, x}
  ⇒ = {res, glob D} ∧
  RO.m{1} = map (fun _ ⇒ ofpair) (pair_map I1.RO.m{2} I2.RO.m{2}) ∧
  ∀ x, x ∈ RO.m{1} = x ∈ I1.RO.m{2} ∧ x ∈ RO.m{1} = x ∈ I2.RO.m{2}].

**proof.** (* ... *) qed.

The corolary `pr_RO_split` is in the form of equality of probabilities, where some of
the information about the relations between the finite maps is lost.

**lemma pr_RO_split (p: glob D → output → bool) &m x0:**

Pr[ MainD(D,RO).distinguish(x0) @ &m : p (glob D) res] =
Pr[ MainD(D,RO_Pair(I1.RO,I2.RO)).distinguish(x0) @ &m : p (glob D) res].

**proof.** **by byequiv RO_split. qed.**

**end section PROOFS.**

**end SplitCodom.**
<figure><img src="image_46.png" /></figure>
# Part II

## Message Authentication
<figure><img src="image_47.png" /></figure>
# Chapter 3

## Security of a MAC Scheme

Passive attacks such as eavesdropping, can be prevented using confidentiality preserving techniques. A different requirement is to protect against active attack, such as falsification of data and transactions. Protection against such attacks is known as *message authentication*.

<figure><img src="image_48.png" /></figure>

### Example

If you're using Windows, all the Windows operating files on disk are the same for each Windows operating system, and are frequently used. Even if they are public and known to the world, it is rather important to ensure that they are not modified by a malware or some other unauthorized entity, without having to decrypt them anytime you access a different functionality of your operating system.

In the case of an ads' banner, the ads' provider does not care about the ads being copied and shown to other people (in fact, it may even benefit them). There is no confidentiality issue at all. What they do care about is modifying the ads in an unauthorized way. An example would be to change the name and the logo of the ads' provider.

<figure><img src="image_49.png" /></figure>

### Remark

In both cases, the usability of the functionality should not be more difficult than accessing the plaintext. This issue corresponds to the balance between security and usability of systems. The importance of such a balance according to the risks in the system's environment cannot be emphasized enough, even if I do not discuss further this issue in this manuscript.

### Message authentication

Message authentication is a procedure that allows communicating parties to verify that the source is *authentic* — the actual source can be verified to be the expected one — and *message integrity* — the message content has not been altered.

The overall intent of any message integrity technique is the same: upon retrieval, ensure the message is exactly the same as it was originally transmitted over a possibly malicious network. In other words, message integrity aims to prevent unintentional and unauthorized changes to transmitted information while the message itself is not encrypted and can be read by anyone receiving the message or listening to the transmission.
One authentication technique involves the use of a secret key to generate a small block of data, known as message authentication code (MAC) or a tag, that is appended to the message. This technique assumes that two communicating parties, say A and B, share a common secret key $k_{AB}$. When A has a message m to send to B, whatever the message length is, it computes the message authentication code as a complex function of the message and the key: $tag_m = MAC_{k_{AB}}(m)$. The message plus tag are transmitted to the intended recipient. The recipient performs the same computation on the received message, using the same secret key, to generate a new tag. The received tag is compared to the computed tag. If they are equal, the message is authenticated, otherwise the couple message-tag can be assumed to be falsified.

## 3.1 Security Definition : Forgery Resistance

Assuming the secret key is only possessed by intended parties, if any entity that does not know the secret key is able to produce a valid tag for a message, the authentication procedure described before does not provide authentication nor message integrity at all. Therefore, the security of such a MAC algorithm resides in the difficulty to forge a valid tag to a message without knowing the secret key, versus the efficiency to compute a valid tag for any message using the secret key. A forgery is the production of $(m, t)$ where $t$ is a valid tag for $m$ when the entity providing it does not own the secret key.

A stronger definition of a forgery is to allow the entity, called adversary, to query the MAC algorithm so that it can obtain valid tags for any message of the adversary's choosing before the attempt of the forgery. The adversary's forgery attempt is successful if the tag is valid for the message, and the message was not previously queried. In other words, even if the adversary can obtain valid tags for any message, it should still be very difficult to produce a valid tag that does not come from the parties knowing the secret key.

**Definition 3.1.1.** The forgery advantage $Adv_M^{\text{forge}}(\mathcal{A})$ of an adversary $\mathcal{A}$ against a MAC scheme M is the probability of $\mathcal{A}$ succeeding in producing a valid forgery :

$$Adv_M^{\text{forge}}(\mathcal{A}) := \Pr \left[ k \stackrel{\$}{\leftarrow} \mathbb{K}; (m,t) \leftarrow \mathcal{A}^{M_k(\cdot)}; t^* \leftarrow M_k(m) : t = t^* \land m \notin \mathcal{Q}_{\mathcal{A}}^{M_k(\cdot)} \right]$$

where $\mathcal{Q}_{\mathcal{A}}^{M_k(\cdot)}$ is the set of all queries $\mathcal{A}$ made to its oracle during its computation.

### Forgery Resistance of a Random Function

#### EasyCrypt

The forgery game is formalized in EasyCrypt as a *module* which takes two modules as parameters, the adversary A and the MAC scheme M.

The Trace module is the formalization of the restriction given to the adversary that depends on the cryptographic game. In the forgery game, the adversary cannot win if the message in the forge attempt has already been queried to its oracle. The module Trace logs all the queries asked by the adversary in its *global variable* Trace.queries and the game tests at the end if the forgery attempt was not previously asked. The init procedure of Trace sets its variable to be empty at the beginning of the forgery game. It then calls the init procedure of the MAC algorithm M. Very often, it stands for the sampling of the MAC key that is stored in a global variable of the module M. This key
is then used for all queries to the procedure mac.

type message, mac.

module type MAC = {
    proc init () : unit
    proc mac (m : message) : mac
}.

module type Adversary (O : MAC) = {
    proc forge () : message * mac { O.mac }
}.

module Trace (M : MAC) : MAC = {
    var queries : (message, mac) fmap
    proc init () : unit = {
        queries ← empty;
        M.init();
    }
    proc mac (m : message) : mac = {
        if (¬ m ∈ Trace.queries) {
            Trace.queries[m] ← M.mac(m);
        }
        return oget Trace.queries[m];
    }}.

module Forge (A : Adversary, M : MAC) = {
    proc game () : bool = {
        var m, t, t';
        Trace(M).init();
        (m,t) ← A(Trace(M)).forge();
        t' ← M.mac(m);
        return t = t' ∧ ¬ m ∈ Trace.queries;
    }}.

In EasyCrypt, to state the security of
a MAC scheme, the forgery advantage

is proven to be bounded for all adversaries by an explicit bound. The adversary module can appear in the bound, and, in this case, it exhibits the security assumption on which the MAC algorithm is secure. This is the general approach to provide a proof of any provable secure scheme in EasyCrypt.

In this setting, the adversary with access to either Trace.queries or the secret MAC key M.k has a trivial forgery attack. Therefore, in the quantification for all adversaries, the adversaries that have access to those global variables should not be considered. A lemma about forgery resistance will appear in the proof script as :

module M : MAC = {
    var k : key
    proc init () = { (* ... *) }
    proc mac (m : message) = {
        (* code of the MAC scheme *)
    }.
}

section Proof.

declare module A : Adversary { M, Trace } .

(* intermediate lemmas *)

lemma forgery : ∀ &m,
Pr [ Forge(A, M).game() @ &m : res ]
≤ (* explicit bound *) .

proof.

(* formal proof script *)

qed.

end section Proof.

## 3.2 Indistinguishability from a Random Function implies
# Forgery Resistance

In this section, I state the forgery advantage of such a random oracle in order to relate
it to the forgery advantage of any MAC scheme and the advantage to distinguish this MAC
scheme from a random oracle.

3.2.1 Forgery Resistance of a Random Function
<figure><img src="image_50.png" /></figure>

EasyCrypt

A random oracle (or random function) named RF is modelized as follows.

type message, mac.

op dmac : mac distr.

axiom dmac_funi : is_funiform dmac.

axiom dmac Il : is_lossless dmac.

The type mac models the output set
F of the MAC algorithm.

module RF : MAC = {
  var map : (message, mac) fmap
  proc init () : unit = { map ← empty; }
  proc mac (x : message) : mac = {
    if (¬ x ∈ map) { map[x] $←$ dmac; }
    return oget map[x];
  }.
}

**Theorem 3.2.1** (Forgery Advantage against a Random Function). For all adversary A that have no access to Trace nor RF, the forgery advantage of A against RF is bounded by the inverse of the size of the output space F.

$$
\mathrm{Adv}_{\mathrm{RF}}^{\mathrm{forge}}(A) \leq \frac{1}{|F|} = \mathrm{mu1} \ \mathrm{dmac} \ \mathrm{witness}
$$

*Proof.* The forgery advantage of A against RF is:

— equal to 0 if $m \in \text{Trace.queries}$, since $\text{Trace.queries} = \text{RF.map}$ is an invariant;

- equal to $\frac{1}{|F|}$ otherwise, since we assume that dmac is the uniform distribution on F.

☐

<figure><img src="image_51.png" /></figure>

EasyCrypt

lemma random_function_is_forgery_resistant :
  ∀ &m (A <: Adversary{Trace, RF}),
  Pr [ Forge(A,RF).game() @ &m : res ] ≤ mu1 dmac witness.

<figure><img src="image_52.png" /></figure>

Remark

Consider the adversary that samples uniformly at random its forgery attempt with
no query. This adversary has a forgery advantage of $\frac{1}{|F|}$ against every MAC scheme
that has the output space F. Therefore, when bounding the forgery advantage for all
adversaries, it can never be less than $\frac{1}{|F|}$. As a consequence, a random function acheives
the *optimal bound* on the forgery advantage when quantified *for all* adversaries.

**3.2.2 Indistinguishability**

In the real world, random function does not exist. Since they achieve the best security
in terms of forgery resistance, one could want to prove that even if a MAC scheme is not
a random function, its behaviour is as close to a random function as possible so that the
forgery advantage of any adversary is close to the forgery advantage of a random function.
In cryptography, two distributions are computationally <fnref n="1" /> indistinguishable if no efficient adversary can tell the difference between them except with small probability. This probability is called the distinguishing advantage of an adversary. It is called prf-distinguishing advantage, for pseudo-random function, when one of them is a random function.

**Definition 3.2.1** (Distingguishing Advantage). Let D and E be two distributions of functions, for any adversary $\mathcal{A}$ that has access to one oracle sampled from one of the distributions and outputs one bit guessing which distribution it was given. The distinguishing advantage of $\mathcal{A}$ about D and E is defined as:

$$ \mathrm{Adv}_{\mathrm{D},\mathrm{E}}^{\mathrm{dist}}(\mathcal{A}) := \left| \Pr\left[d \leftarrow \mathrm{D}; b \leftarrow \mathcal{A}^{d(\cdot)} : b = 1\right] - \Pr\left[e \leftarrow \mathrm{E}; b \leftarrow \mathcal{A}^{e(\cdot)} : b = 1\right] \right| $$

<figure><img src="image_53.png" /></figure>

EasyCrypt

type t_in, t_out.

module type Function = {
  proc init () : unit
  proc f (x : t_in) : t_out
}.

module type Distinguisher (F : Function) = {
  proc guess () : bool { F.f }
}.

module Dist (D : Distinguisher) (F : Function) = {
  proc game () : bool = {
    var b : bool;
    F.init();
    b ← D(F).guess();
    return b;
  }
}.

module F : Function = (* some function *).

module G : Function = (* some function *).

lemma indistinguishable :

$$ \forall \&m (D <: Distinguisher\{F, G\}), $$

$$ `| \Pr[\mathrm{Dist}(D,F).\mathrm{game}() @ \&m : \mathrm{res}] - \Pr[\mathrm{Dist}(D,G).\mathrm{game}() @ \&m : \mathrm{res}] | \leq (* some \ concrete \ bound *)$. $$

proof. (* some proof script *) qed.

## Forgery Resistance from Indistinguishability with a Random Function

**Theorem 3.2.2.** Let the program $\mathcal{B}(\cdot)$ build a distinguishing adversary given a forgery adversary $\mathcal{A}$ that aims to distinguish a MAC scheme M from a random function pictured as $\$$, i.e. $\mathcal{B}(\mathcal{A})^{O(\cdot)} := \mathrm{Forge}[\mathcal{A}, \mathrm{O}].\mathrm{main}$. For any adversary $\mathcal{A}$, its forgery advantage against M

<footnote n="1">1. The specification “computationally” refers to the fact that only efficient adversaries are taken into account in this definition of indistinguishability. In EasyCrypt, there is no analysis of complexity in time but analysis of probabilistic terminaison. Therefore all adversaries that are considered in the proofs are not bounded in time. Instead they are often assumed to be lossless. This is the assumption that adversaries will terminate with probability 1. This is a stronger result on indistinguishability than computational indistinguishability.</footnote>
is bounded by the advantage of the distinguishing adversary $\mathcal{B}(\mathcal{A})$ to distinguish M from a random function plus the inverse of the size of the tag space $\mathcal{B}$.

$$ \mathrm{Adv}_{\mathrm{M}}^{\mathrm{forge}}(\mathcal{A}) \le \mathrm{Adv}_{\mathrm{M},\mathcal{S}}^{\mathrm{dist}}(\mathcal{B}(\mathcal{A})) + \frac{1}{|\mathcal{B}|} $$

*Proof.* By unfolding the definition of $\mathcal{B}$ and the distinguishing advantage:

$$ \mathrm{Adv}_{\mathrm{M},\mathrm{LazyRF}}^{\mathrm{dist}}(\mathcal{B}(\mathcal{A})) = \left| \mathrm{Adv}_{\mathrm{M}}^{\mathrm{forge}}(\mathcal{A}) - \mathrm{Adv}_{\mathrm{LazyRF}}^{\mathrm{forge}}(\mathcal{A}) \right| \ge \mathrm{Adv}_{\mathrm{M}}^{\mathrm{forge}}(\mathcal{A}) - \frac{1}{|\mathcal{B}|} $$

□

## 3.3 Block Cipher Mode of Operation

A block cipher is a deterministic algorithm operating on fixed-length group of bits, called block, with an unvarying transformation (encryption or decryption) that is specified by a symmetric key. The most used block cipher is the Advanced Encryption Standard (AES [Daemen and Rijmen, 1999]), even if older block ciphers are still used: Data Encryption Standard (DES [Morris et al., 1977]), or triple DES.

A block cipher by itself is only suitable for the secure cryptographic transformation (encryption or decryption) of one block. A block cipher mode of operation is an algorithm that uses a block cipher to provide information security such as confidentiality or authenticity. However, the security of a mode of operation does not entirely depends on the security of the underlying block cipher. When a block cipher is used in a given mode of operation, the resulting algorithm should ideally be about as secure as the underlying block cipher itself.

<figure><img src="image_54.png" /></figure>

**Example**

Consider the algorithm that encrypts an arbitrary long message by encrypting each block separately, with the same symmetric key. It is named ECB, for Electronic Codebook. Even if the block cipher correctly hides information of each block, the pattern of a longer message may be revealed as shown in Figure 3.1.

<figure><img src="image_55.png" /><figcaption>Plaintext.</figcaption></figure>

<figure><img src="image_56.png" /><figcaption>Encrypted using ECB.</figcaption></figure>

<figure><img src="image_57.png" /><figcaption>Securely encrypted.</figcaption></figure>

<caption>Figure 3.1 – ECB reveals patterns, even when using a secure block cipher.</caption>
### 3.3.1 Security Definition of a Block Cipher

A block cipher consists of two paired algorithms, one for encryption denoted E, and one for decryption denoted D. Both algorithms expect two inputs: a block in $\mathbb{B}$ and a private key $k \in \mathbb{K}$; and both algorithms output a block in $\mathbb{B}$. The decryption is defined to be the inverse function of encryption, when they both use the same private key.

More formally, a block cipher is specified by an encryption function:

$$E_k(p) := E(k, p) : \mathbb{K} \times \mathbb{B} \to \mathbb{B}$$

which takes as input a key $k \in \mathbb{K}$, and the plaintext, a block $p \in \mathbb{B}$ and returns the ciphertext, a string $c \in \mathbb{B}$. For each key $k \in \mathbb{K}$, the function $E_k(\cdot)$ is required to be an invertible mapping on $\mathbb{B}$, where the inverse $D_k$ is defined as:

$$D_k(c) := D(k, c) : \mathbb{K} \times \mathbb{B} \to \mathbb{B}$$

We denote $\text{Perm}(\mathbb{B})$ the family of all permutations on $\mathbb{B}$ that is equipped with the uniform distribution. The *prp-distinguishing advantage* (for pseudo-random permutation) against a block cipher is the advantage to distinguish it, when the key is randomly sampled, from a random permutation sampled from $\text{Perm}(\mathbb{B})$.

**Definition 3.3.1** (prp-distinguishing advantage). The prp-distinguishing advantage of any adversary $\mathcal{A}$ to tell apart a block cipher (E, D) equipped with a random key from a random permutation over the same block space $\mathbb{B}$ is defined as follows:

$$\text{Adv}_{(\text{E,D})}^{\text{prp}}(\mathcal{A}) := \\ \left| \Pr\left[ k \stackrel{\$}{\leftarrow} \mathbb{K}; b \leftarrow \mathcal{A}^{E_k(\cdot), D_k(\cdot)} : b = 1 \right] - \Pr\left[ \pi \stackrel{\$}{\leftarrow} \text{Perm}(\mathbb{B}); b \leftarrow \mathcal{A}^{\pi(\cdot), \pi^{-1}(\cdot)} : b = 1 \right] \right|$$

### 3.3.2 Security Definition of a Block Cipher Mode of Operation

Some MAC algorithms are constructed using a *mode of operation*. A mode of operation describes how to repeatedly apply a block cipher operation to securely transform amounts of data larger than a block. The security of such a mode often relies on the security assumption that the underlying block cipher is secure, so that in the analysis of the structure of the mode, one can replace calls to a block cipher with different keys by independent random permutations.
<figure><img src="image_58.png" /></figure>

EasyCrypt

In EasyCrypt, such a formalization
looks like the following.

type key.

type block.

op dblock : block distr.

axiom dblock_funi : is_funiform dblock.

axiom dblock_\_\_ : is_lossless dblock.

module type Permutation = {
  proc init () : unit
  proc enc (p : block) : block
  proc dec (p : block) : block
}.

module type Distinguisher
  (O : Permutation) = {
    proc distinguish () : bool { O.enc.O.dec }
  }.

module Dist (D : Distinguisher)
  (P : Permutation) = {
    proc game () : bool = {
      var b : bool;
      P.init();
      b ← D(P).distinguish();
      return b;
    }.
  }.

lemma mode_of_operationsecure :
  ∀ &m
  (OM <: OperationMode{Trace, RP})
  (P <: Permutation{Trace, RP, OM})
  (A <: Adversary{Trace, RP, OM, P}),
  Pr [ Forge(A,OM(P)).game() @ &m : res ]
  ≤ Pr [ Forge(A,OM(RP)).game() @ &m : res ] (* concrete upper bound *)
  + |Pr [ Dist(B(A),P).game() @ &m : res ] - Pr [ Dist(B(A),RP).game() @ &m : res ]|.
  (* security assumption *)

module type OperationMode
  (P : Permutation) = MAC.

module RP : Permutation = {
  var map : (block, block) fmap
  var mapi : (block, block) fmap
  proc init () : unit = {
    map ← empty;
    mapi ← empty;
  }
  proc enc (x : block) : block = {
    if (¬ x ∈ map) {
      map[x] $← dblock \ (rng map);
      mapi[oget map[x]] ← x;
    }
    return oget map[x];
  }
  proc dec (x : block) : block = {
    if (¬ x ∈ mapi) {
      mapi[x] $← dblock \ (rng mapi);
      map[oget mapi[x]] ← x;
    }
    return oget mapi[x];
  }.
}.
# Chapter 4

## CMAC's Formal Security Proof
[Baritel-Ruet et al., 2018]

The Cipher-based Message Authentication Code, shortened as CMAC [Song et al., 2006], is a block cipher-based message authentication code algorithm. The structure of CMAC's algorithm is sequential and its computation does not require to know the length of the message to authenticate.

### 4.1 Historical presentation

The CMAC scheme was first introduced by Iwata and Kurosawa as OMAC1, for One-key MAC, in [Iwata and Kurosawa, 2003]. It is now a standardized MAC [Dworkin, 2016]. The scheme is based on the CBC (chained block cipher) mode of operation [Ehrsam et al., 1978], and more precisely on the MAC scheme derived from it. We denote $CBC-MAC_{E_k}$ to represent the CBC-MAC scheme using the underlying block cipher $E_k$.

In CBC-MAC, the message to authenticate is split into a list of blocks. The first block is encrypted by $E_k$, and each next block is first xored using the last computed cipher then encrypted by $E_k$. This constructs a chain linked by the output of the block cipher. This dependence ensures that a change to any bit of a message will change the rest of the MAC in an unpredictable way.

<figure><img src="image_59.png" /><figcaption>Figure 4.1 – Representation of $CBC-MAC_{E_k}(m_1||m_2||m_3||m_4)$</figcaption></figure>
<figure><img src="image_60.png" /></figure>

EasyCrypt

```python
module type MACN = {
    proc init() : unit
    proc mac (m : block list) : block
}
module CBCMAC (F : Permutation) : MACN = {
    proc init = F.init
    proc mac (m : block list) : block = {
        var i : int ← 0;
        var c : block ← zeros;
        while (i < size m) {
            c ← F.enc(m[i] ^ + c); (* ^+ denotes the xor operation *)
            i ← i + 1;
        }
        return c;
    }}.
```

Bellare, Kilian and Rogaway [Bellare et al., 1994] prove the security of the CBC-MAC construction, by proving, as is the practice in cryptography, that any algorithm that finds CBC-MAC forgeries with non-negligible probability can be used to break the underlying block cipher with the same time complexity. However, their proof — and indeed the security of CBC-MAC — is limited to the case where the length *m* of the message (in blocks) is fixed in advance. Indeed, it is easy to produce a chosen message forgery as follows when the tagging and verification algorithm accepts arbitrary length messages:

1. Through chosen-message queries, obtain $t = \text{CBC}(m)$ and $t' = \text{CBC}(m')$ for some messages $m$ and $m'$ of respective lengths $m > 0$ and $m' > 0$.

2. Then $t'$ is also a valid tag for the fresh message: $m_1 || \dots || m_m || [t \oplus m'_1] || \dots || m'_{m'}$.

Thus CBC-MAC suffers from two major issues: i. the size of messages should be a multiple of *n*, the block size, and ii. all messages must contain the same, fixed, number of blocks. To overcome these restrictions, Black and Rogaway [Black and Rogaway, 2005] propose three extensions of CBC-MAC:¹i. ECBC, ii. FCBC and iii. XCBC. CMAC is a variant of XCBC that was first proposed by Iwata and Kurosawa [Iwata and Kurosawa, 2003] as OMAC1.

Description of ECBC

The first issue of CBC-MAC, that is being limited to computing tags for messages whose length is a multiple of the block length, is often dealt with using some injective padding scheme. However, such schemes require flexibility in the number of blocks that can be processed, as their injectivity may require them to add a full block of padding onto a message. The MAC scheme ECBC combines two ideas to: i. allow padding messages to a multiple of the block length without overhead; and ii. securely support computing MAC tags for messages of different lengths.

<footnote n="1">1. A simpler fix is to prepend the length of the input message to the message itself before processing it: if this does indeed yield a secure MAC algorithm, it is not always possible to know the length of the payload when the processing begins. For example, the TLS protocol computes a MAC over the concatenation of all messages exchanged during its handshake protocol—the length of which is only known after it is over. These engineering considerations are often kept separate from security considerations when defining the syntax and security of cryptographic schemes. This provides abstraction but brings its own set of problems.</footnote>
First, in order to support messages with different numbers of blocks, it is possible to apply additional treatment to the final tag before releasing it. This is to ensure that it cannot predictably be used as a known intermediate value in the computation of a tag for a chosen message. In ECBC, this is done, using an idea by Vaudenay [Vaudenay, 2000], which was first proposed in the book [Bosselaers and Preneel, 1995], by computing a CBC-MAC tag using a block cipher key $k_1$ and encrypting this tag with a different key $k_2$ before releasing it.

This first idea then brings an opportunity to do padding only when needed. Indeed, rather than ensuring the padding is injective, it is possible to apply padding to the message only when its length is not a multiple of $n$, but then compute the final encryption using a different key $k_3$ when padding was applied.

Given some injective padding function pad : $\Sigma^* \to \mathbb{B}^+$ that pads arbitrary strings over some alphabet $\Sigma$ as non-empty sequence of blocks, and combining the two ideas above, the ECBC scheme (also shown in Figure 4.2) can be defined as the following three-key construction.

$$ \text{ECBC}_{E_{k_1}, E_{k_2}, E_{k_3}}(m) = \begin{cases} E_{k_2}(\text{CBC}_{k_1}(m)) & \text{if } m \in \mathbb{B}^+ \\ E_{k_3}(\text{CBC}_{k_1}(\text{pad}(m))) & \text{otherwise} \end{cases} $$

<figure><img src="image_61.png" /><figcaption>Figure 4.2 – Representation of $\text{ECBC}_{E_{k_1}, E_{k_2}, E_{k_3}}(m_1||m_2||m_3||m_4)$</figcaption></figure>
<figure><img src="image_62.png" /></figure>

## EasyCrypt

```pascal
op pad (s:bitstring) : bitstring =
  if ^|s| mod n = 0 then s else s || ones 1 || zeros (n - 1 - (^|s| mod n)).
```

```pascal
op towords (s:bitstring) : block list = let indexes = iota_0 (^|pad s| %/ n) in
let l = map (fun (i:int) -> from_bits (sub (pad s) (i*n) n)) indexes in
mkarray l.
```

```pascal
op ofwords (t : block list) : bitstring = let l = ofarray t in
foldr (fun a b -> to_bits a || b) (ABitstring.zeros 0) l.
```

```pascal
module type MAC = {
  proc init () : unit
  proc mac (_: bistring) : block
}.
```

```pascal
module EPAD (H : MACN) (F2 F3 : BlockCipher) : MAC = {
  proc init() : unit = {
    H.init(); F2.init(); F3.init();
  }
  proc mac (m : bitstring) : block = {
    var t : block;
    if ((size m) mod n = 0) {
      t ← H.mac(towords m);
      t ← F2.f(t);
    } else {
      t ← H.mac(towords m);
      t ← F3.f(t);
    }
    return t;
  }.
```

```pascal
module ECBC (F1 F2 F3 : BlockCipher) : MAC = EPAD(CBCMAC(F1),F2,F3).
```

## Description of FCBC

In ECBC, as shown in Figure 4.2, processing the last block of message involves two consecutive calls to the block cipher with independent keys. This brings an opportunity for optimization. Indeed, since block ciphers are meant to be indistinguishable from random permutations, a single block cipher invocation is in fact sufficient for security. The FCBC construction, shown in Figure 4.3, implements this idea.

<figure><img src="image_63.png" /></figure>

## EasyCrypt

```pascal
module PartialCBCMAC (F : BlockCipher) : MACN = {
  proc init = F.init
  proc mac (m : word list) : word = {
    var i : int ← 0;
    var c : word ← zeros;
    while (i < size m - 1) {
      c ← F.f(m[i] ^+ c); (* ^+ denotes the xor operation *)
      i ← i + 1;
    }
    return c ^+ m[i];
  }.
```
<figure><img src="image_64.png" /><figcaption>Figure 4.3 – Representation of FCBC$_{E_{k_1}, E_{k_2}, E_{k_3}}$ $(m_1||m_2||m_3||m_4)$.</figcaption></figure>

module FCBC (F1 F2 F3 : BlockCipher) : MAC = EPAD(PartialCBCMAC(F1),F2,F3).

## Description of XCBC

Both of the above constructions do solve CBC-MAC's main issues, with FCBC giving a small performance advantage. However, their use of block ciphers keyed with independent keys makes them expensive to compute using block ciphers like the AES [Daemen and Rijmen, 2013]. Indeed, AES involves a costly key expansion phase that can only be amortized if the same key is used many times. To better suit this engineering constraint, the XCBC construction (Figure 4.4) uses the same key $k$ for all block cipher invocations, and uses the other two keys $(k_2, k_3)$ to mask the final block before processing it. This is done without loss of security.

<figure><img src="image_65.png" /></figure>

### EasyCrypt

module XOR2 (E : BlockCipher) = {
    proc init(q : int) : unit = {}
    proc f (x : word) : word = {
        var y : word;
        y ← E.f(x ^+ XOR.k2);
        return y;
    }.
}

module XOR3 (E : BlockCipher) = {
    proc init(q : int) : unit = {}
    proc f (x : word) : word = {
        var y : word;
        y ← E.f(x ^+ XOR.k3);
        return y;
    }.
<figure><img src="image_66.png" /><figcaption>Figure 4.4 – Representation of XCBC<sub>E<sub>k</sub>,k<sub>2</sub>,k<sub>3</sub></sub>(m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</figcaption></figure>

```pascal
}}.
module FCBC (F1 F2 F3 : BlockCipher) : MAC =
    EPAD(PartialCBCMAC(F1), XOR2(F1), XOR3(F3)).
```

## Description of CMAC

One final performance constraint needs dealt with: the key size for XCBC is indeed 2n plus the key size for CBC-MAC. CMAC (also known as OMAC1) proposes to derive k<sub>2</sub> and k<sub>3</sub> from k using the block cipher. We note that this makes CMAC easier to express as a refinement of FCBC—rather than XCBC. In particular, the security of XCBC cannot be easily used to prove the security of CMAC, as it requires that the three keys be independent.

At this stage, it is necessary to concretely instantiate the block space $\mathbb{B} = \text{GF}(2^n)$, that is represented as the quotient of the polynomial ring $\text{GF}(2)[x]$ by a fixed irreducible polynomial of degree $n$. With this choice of block space, CMAC derives k<sub>2</sub> and k<sub>3</sub> as:

- $k_2 := 2 \times E_k(0^n)$, when the constant 2 can be seen as the hexadecimal number 0x02, or the bitstring 0...010, or the polynomial $x \in \text{GF}(2^n)$, and

- $k_3 := 4 \times E_k(0^n)$, when the constant 4 can be seen as the hexadecimal number 0x04, or the bitstring 0...0100, or the polynomial $x^2 \in \text{GF}(2^n)$.

<figure><img src="image_67.png" /></figure>

### EasyCrypt

```pascal
module Tweak1 (E : BlockCipher) = {
  proc init(q : int) : unit = {}
  proc f (x : word) : word = {
    var y : word;
```
<figure><img src="image_68.png" /><figcaption>Figure 4.5 – Representation of CMAC<sub>E<sub>k</sub></sub>(m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</figcaption></figure>

```pascal
y ← E.f(x ^+ tweak1 XOR.k);
return y;
}
}
module Tweak2 (E : BlockCipher) = {
  proc init(q : int) : unit = {}
  proc f (x : word) : word = {
    var y : word;
    y ← E.f(x ^+ tweak2 XOR.k);
    return y;
  }
}
module CMAC (E1 : BlockCipher) = {
  proc init (σ : int, q : int) : unit = {
    E1.init(σ+1); (* this is an artefact from the security proof about counters *)
    XOR.k ← E1.f(AWord.zeros);
  }
  proc f = EPAD(CBCpartial(E1), Tweak1(E1), Tweak2(E1)).f
}
```

## 4.2 MAC Security Proofs

This section describes a formalization verifying a concrete bound of the security of CMAC. The proof is articulated as shown in Figure 4.6. The security of both CMAC and XCBC relies on the security proof of FCBC, which is equivalent to the security of ECBC. Finally, the security of ECBC relies on the unlikeliness that two different messages chosen before the block cipher key k is sampled will have the same CBC-MAC<sub>E<sub>k</sub></sub> value.
<figure><img src="image_69.png" /><figcaption>Figure 4.6 – Layers of the CMAC’s security proof.</figcaption></figure>

Our security proofs for ECBC, FCBC, XCBC and CMAC are in fact proofs that they cannot be distinguished from a random function assuming that the underlying block cipher is secure. Therefore, the block ciphers used with independent random keys can be replaced by independent random permutations, using the lemma in section 3.3.2. Only in the last theorem statements, the advantage of an adversary distinguishing between a block cipher instance and a random permutation will appear. From now on, the implicit function parameters of a parameterized MAC scheme are independent random permutations.

We provide a verified security bound on the advantage of any adversary to:

a) distinguish ECBC and a random function;

b) distinguish FCBC and ECBC (the bound is actually equal to 0);

c) distinguish XCBC and FCBC; and

d) distinguish CMAC and FCBC.

The first three statements follow those by Black and Rogaway [Black and Rogaway, 2005].

### 4.2.1 Indistinguishability of ECBC from a Random Function

For any independent random permutations $\pi_1, \pi_2, \pi_3$:

$$ 
\begin{aligned}
\text{ECBC}[\pi_1, \pi_2, \pi_3](m) &= \text{EPAD}[\text{CBC-MAC}[\pi_1], \pi_2, \pi_3](m) \\
&= \begin{cases} \pi_2(\text{CBC-MAC}[\pi_1](m)) & \text{if m's size is a multiple of } n \\ \pi_3(\text{CBC-MAC}[\pi_1](\text{pad}(m))) & \text{otherwise} \end{cases}
\end{aligned}
$$

**Idea of the proof.** Since the output of ECBC is either the output of $\pi_2$ or $\pi_3$, which are both random permutations, it should look random if their input is fresh. This input is the output of CBC-MAC, therefore the probability of distinguishing ECBC from a random function is closely related to the probability to find a collision of outputs in CBC-MAC for two different messages without knowing the values CBC-MAC produced. We call this distinguishing event collision finding. It is unrelated to the primitive CBC-MAC, so we choose to generalize it.

**Generalization.** The security of ECBC is formalized by generalizing the first parameter of EPAD. In EasyCrypt, we quantify over all modules ($H <: \text{MACN}$).

**Definition of collision-finding probability.** This probability is defined as a game-based notion, through the following collision-finding game. The adversary $\mathcal{A}$ is asked to provide a list of messages of its choice, without access to the hash values and before the hash function represented by the module ($H <: \text{MACN}$) is initialized. The success of $\mathcal{A}$ is defined as the event that the list of messages contains two distinct messages that have the same image by $H$. This yields the following definition of an adversary $\mathcal{A}$'s collision-finding advantage against a probabilistic program represented by the module $H$.

$$ \Pr[\text{I} \leftarrow \mathcal{A}; \text{H.init()} : \exists m, m' \in \text{I}. m \neq m' \land \text{H}(m) = \text{H}(m')] $$
**Statement.** If H is collision-finding resistant, then EPAD[H] is a pseudo-random function.

**Proof.** First, the independent random permutations $\pi_2, \pi_3$ are replaced by independent random functions $f_2, f_3$ using twice the PRP-PRF switching lemma (Lemma 2.3.1). This adds a term in the bound of indistinguishability of EPAD[H] from a random function.

We apply the PRP-PRF switching lemma on both $\pi_2$ and $\pi_3$. Following our oracle query counting, the adversary could cause either of these to be queried at most $q$ times, yielding the following probability bound:

$$ \left| \Pr\left[ h \stackrel{\$}{\leftarrow} H; \pi_2 \stackrel{\$}{\leftarrow} \operatorname{Perm}(\mathcal{B}); \pi_3 \stackrel{\$}{\leftarrow} \operatorname{Perm}(\mathcal{B}); b \stackrel{\mathcal{A}_{\sigma,q}^{\operatorname{EPAD}[h, \pi_2, \pi_3]}}{\leftarrow} b = 1 \right] \\ - \Pr\left[ h \stackrel{\$}{\leftarrow} H; f_2 \stackrel{\$}{\leftarrow} \operatorname{Rand}(\mathcal{B}); f_3 \stackrel{\$}{\leftarrow} \operatorname{Rand}(\mathcal{B}); b \stackrel{\mathcal{A}_{\sigma,q}^{\operatorname{EPAD}[h, f_2, f_3]}}{\leftarrow} b = 1 \right] \right| \le \frac{q(q-1)}{|\mathcal{B}|} $$

From now on, we refer using EPAD[h] to the function composed of EPAD[h, $f_2, f_3$] when $f_2, f_3$ are two independent random functions and $h \stackrel{\$}{\leftarrow} H$.

In EPAD[h], all inputs of both $f_2$ and $f_3$ are the output of h. As $f_2, f_3$ are two independent random functions, the output of EPAD[h] on fresh messages will be sampled at random unless h maps it to an already produced output value. This corresponds to the definition of a collision in h. Formalizing this argument, we prove that EPAD[h] is indistinguishable from a random function unless a collision, as formally defined below, occurs in h.

$$ \mathrm{Coll}_h(M, M') := M \neq M' \wedge h(M) = h(M') $$

$$ \mathrm{Coll}_h(S) := \exists(M, M') \in S^2, \mathrm{Coll}_h(M, M') $$

This proof is a standard cryptographic reduction, whereby, given a prf-distinguishing adversary $\mathcal{A}$, we construct a collision-finding adversary $\mathcal{B}(\mathcal{A})$ against h that operates with similar time complexity. $\mathcal{B}$ is constructed as follows. $\mathcal{B}$ samples a random function $f \stackrel{\$}{\leftarrow} \operatorname{Rand}(*, \mathcal{B})$ and runs $\mathcal{A}^f$. While doing so, $\mathcal{B}$ stores all the queries of $\mathcal{A}$ in a set $S^2$, pads all the queries whose length is not a multiple of $n$, then outputs the resulting set. It can then be shown that the following inequality holds, and it remains to bound the right-hand side, which is an instance of the collision-finding game.

$$ \mathrm{Adv}_{\mathrm{EPAD}_H^\mathrm{prf}}(\mathcal{A}) \le \Pr\left[S \leftarrow \mathcal{B}(\mathcal{A})_{\sigma,q}; h \stackrel{\$}{\leftarrow} H : \mathrm{Coll}_h(S)\right] $$

## CBC-MAC is collision-finding Resistant

The mode of operation CBC-MAC can be seen as a function family indexed by the block cipher key space $\mathbb{K}$. Sampling a key uniformly at random in $\mathbb{K}$ induces a distribution over $\mathbb{B}^+ \to \mathbb{B}$ for the hash function family $H = \mathrm{CBC-MAC}_{\mathrm{E}_{\mathbb{K}}}$.

<footnote n="2">2. We note that the choice of data structure for formalizing collisions does not keep track of query order or multiplicity (in particular, when padding maps an unpadded message to a padded message that is separately queried to h). This relaxation is done without loss of precision since $\mathrm{CBC}_f$ is deterministic and two consecutive calls to $\mathrm{CBC}_f$ can be swapped without effect on the random function – even if it is sampled lazily.</footnote>
**Difference from Black and Rogaway's proof [Black and Rogaway, 2005].** From here on, our proof for ECBC differs from that by Black and Rogaway [Black and Rogaway, 2005], due to the impossibility of precisely formalizing their arguments in EasyCrypt.

Using their notations, in the proof of their Lemma 3, they compute probabilities of events of the form $Pr[Y_{i-1} \oplus M_i = Y_{j-1} \oplus M_j]$, relying on their ability to compute the probability of sampling a particular value for $Y_{i-1}$. However, this sampling occurs in a previous iteration of the loop, and may in fact be overwritten, losing its “randomness” for the next iteration where the events are tested.

One may argue that every value it may be overwritten with in fact follows the same distribution. However, EasyCrypt's logics-and indeed entire proof methodology relies on reasoning about values rather than distributions, and its logics cannot express the fact that some intermediate value follows a particular distribution. On the other hand, a standard way of dealing with similar issues would be to delay the random sampling until the value is used, allowing a precise probability computation. However, in this case, the value could in fact be overwritten between the point where it is initially sampled and the point where it is used. This introduces dependencies between random values and the adversary's view of the system that make it impossible to delay sampling operations as desired.

**Our method.** If we cannot formalize precisely their argument, we can formalize a simpler and less precise bound that does not discount internal collisions when they are caused by a common prefix. In particular, instead of computing the collision probability for the full set S of messages, we guess which of the couples of messages may produce a collision and use standard arguments to bound the probability that any of them collide. We sample two of the messages from S and only compute their collision probability. Let $\mathcal{C}(\mathcal{B})$ be the adversary that calls the adversary $\mathcal{B}$ which outputs a set $S \subset \mathbb{B}^+$, then samples two distinct messages $M, M' \leftarrow S$ and outputs $(M, M')$. There are at most $\frac{|S|(|S|-1)}{2}$ different pairs.

**Lemma 4.2.1.** For any function family $H \in \{\mathbb{B}^+ \to \mathbb{B}\}$, any adversary $\mathcal{B}$ that outputs a set of size at most $c$ (with $2 \le c$) has a comparable collision probability to the adversary that tries to guess where the collision may happen and only test this collision.

$$ \Pr[S \leftarrow \mathcal{B}_c; h \stackrel{\$}{\leftarrow} H : \mathrm{Coll}_h(S)] \le \frac{c(c-1)}{2} \cdot \Pr[m, m' \leftarrow \mathcal{C}(\mathcal{B})_c; h \stackrel{\$}{\leftarrow} H : \mathrm{Coll}_h(m, m')] $$

In the context of ECBC, the hash function family is concretely CBC-MAC, parametrized by a random permutation $\pi$. However, the PRP-PRF switching lemma applied on $\pi$ allows to consider the collision-finding probability on CBC-MAC that is parametrized by a random function instead of a random permutation. This makes the collision-finding probability to be more easily bounded in CBC-MAC.

$$ \begin{aligned} \mathrm{Adv}_{\mathrm{ECBC}}^{\mathrm{prf}}(\mathcal{A}) & \le \frac{q(q-1)}{2^n} + \mathrm{Pr}\left[S \leftarrow \mathcal{B}[\mathcal{A}]_\sigma; \pi \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B}) : \mathrm{Coll}_{\mathrm{CBC-MAC}_\pi}(S)\right] \\ & \le \frac{q(q-1)}{2^n} + \frac{\sigma(\sigma-1)}{2^{n+1}} + \frac{q(q-1)}{2} \cdot \mathrm{Pr}\left[m, m' \leftarrow \mathcal{C}[\mathcal{B}[\mathcal{A}]]_q; f \stackrel{\$}{\leftarrow} \mathrm{Rand}(\mathbb{B}) : \mathrm{Coll}_{\mathrm{CBC-MAC}_f}(m, m')\right] \end{aligned} $$

It therefore remains to bound the probability of collisions of two different messages in CBC-MAC$_f$ when f is a random function.
**Theorem 4.2.2** (CBC-MAC collision probability of two messages). For any natural number $c$, an adversary $\mathcal{A}_c$ that outputs two bit-strings $(m, m')$ whose lengths are at most $cn$, with $0 < c$, has a low probability of producing a collision with CBC-MAC when parameterized by a random function.

$$ \Pr[m, m' \leftarrow \mathcal{A}_c; f \stackrel{\$}{\leftarrow} \mathrm{Rand}(\mathbb{B}) : \mathrm{Coll}_{\mathrm{CBC-MAC}_f}(m, m')] \le \frac{2c(2c-1)}{2^n} + \frac{1}{2^n} $$

*Proof.* Let $(m, m')$ be two distinct messages output by the adversary $\mathcal{A}_c$, and $f$ the random function sampled by the experiment. If there is no collision in any of the inputs of $f$ during the CBC chaining, $\mathrm{CBC}_f(m)$ will collide with $\mathrm{CBC}_f(m')$ only if the final call to $f$ yields a collision. This occurs with probability at most $\frac{1}{2^n}$.

It remains to bound the probability that a collision occurs somewhere along the chain of inputs to $f$. The chaining for the longest common prefix of $m$ and $m'$ is computed only once, and collisions are only considered afterwards. We then bound the probability of a collision occurring in one of the inputs to $f$ by the probability of a collision occurring when those $2c$ inputs are sampled. $\square$

Combining all results above allows us to conclude with a security bound for ECBC.

**Theorem 4.2.3** (prf-advantage of ECBC). For any natural numbers $q, l, \sigma, n$, an adversary $\mathcal{A}$ making at most $q$ queries, each query of maximum size $ln$ and of total size in the number of blocks at most $\sigma$, has a low probability to distinguish ECBC from a random function, when parameterized by independent random permutations.

$$ \mathrm{Adv}_{\mathrm{ECBC}}^{\mathrm{prf}}(\mathcal{A}) \le \frac{0.5\sigma^2 + 2q^2l^2 + q^2}{2^n} \quad (4.1) $$

## 4.2.2 Indistinguishability of FCBC from ECBC

We now relate the structure of FCBC with that of ECBC. Indeed, we note that ECBC is a particular instance of FCBC with non-independent permutations. Given three independent permutations $\pi_1, \pi_2, \pi_3$, we have

$$ \mathrm{ECBC}_{\pi_1, \pi_2, \pi_3} = \mathrm{FCBC}_{\pi_1, \pi_2 \circ \pi_1, \pi_3 \circ \pi_1} $$

The security proof for FCBC then simply relies on the fact that the composition of two independent random permutations remains independent from the first one. In other words, given two independent random permutations $\pi_1, \pi_2$, the distributions of $(\pi_1, \pi_2 \circ \pi_1)$ and $(\pi_1, \pi_2)$ are the same.

**Lemma 4.2.4.** An adversary $\mathcal{A}$ making an unbounded number of oracle queries cannot distinguish the composition of two independent random permutations.

$$ \Pr[\pi_1, \pi_2 \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B})^2 : \mathcal{A}^{\pi_1, \pi_2} = 1] = \Pr[\pi_1, \pi_2 \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B})^2 : \mathcal{A}^{\pi_1, \pi_2 \circ \pi_1} = 1] $$

*Proof of Lemma 4.2.4.* It is possible to pre-sample outputs for all inputs of both $\pi_1$ and $\pi_2$. This makes it clear that answers to $\pi_2 \circ \pi_1$ queries are independent from past queries to $\pi_1$ and that, with $\pi_1$ fixed, the distributions of $\pi_2 \circ \pi_1$ and $\pi_2$ are equal. $\square$
**Theorem 4.2.5 (Security of FCBC).** An adversary $\mathcal{A}$ cannot distinguish FCBC from ECBC, when parameterized by independent random permutations.

$$ \mathrm{Adv}_{\mathrm{FCBC}}^{\mathrm{prf}}(\mathcal{A}) = \mathrm{Adv}_{\mathrm{ECBC}}^{\mathrm{prf}}(\mathcal{A}) \qquad (4.2) $$

*Proof.* This is a direct application of Lemma 4.2.4 (applied twice). □

### 4.2.3 Indistinguishability of XCBC from FCBC

The proof that XCBC is indistinguishable from FCBC is based on a more general lemma from [Black and Rogaway, 2005], which states that an adversary with oracle access to two independent random permutations $\pi_1(\cdot)$ and $\pi_2(\cdot)$ cannot distinguish them from oracles $\pi(\cdot)$ and $\pi(k \oplus \cdot)$, when $\pi$ is a random permutation and $k$ is chosen uniformly at random and independently from $\pi$ (and remains hidden from the adversary).

We view XCBC as a particular instance of FCBC. Indeed, given a permutation $\pi$ and two blocks $k_2, k_3$, we have

$$ \mathrm{XCBC}_{\pi, k_2, k_3} = \mathrm{FCBC}_{\pi, \pi(k_2 \oplus \cdot), \pi(k_3 \oplus \cdot)} $$

We thus prove that the security of XCBC is implied by that of FCBC. The proof crucially relies on the following lemma, which states that one can always (computationally) simulate two independent random permutations using a unique random permutation and a random constant.

**Lemma 4.2.6.** For any natural number $c$, an adversary $\mathcal{A}$ making at most $c$ oracle queries, with $0 < c \le \frac{2^n}{2}$, has a low probability of distinguishing between two independent permutations $(\pi_1, \pi_2)$ and the pair of permutations $(\pi, \pi(k \oplus \cdot))$.

$$ \left| \mathrm{Pr} \left[ \pi_1, \pi_2 \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B})^2; b \leftarrow \mathcal{A}_c^{\pi_1, \pi_2} : b = 1 \right] - \mathrm{Pr} \left[ \pi, k \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B}) \times \mathbb{B}; b \leftarrow \mathcal{A}_c^{\pi, \pi(k \oplus \cdot)} : b = 1 \right] \right| \le \frac{1.25c^2}{2^n} $$

*Proof of Lemma 4.2.6.* The proof closely follows that of [Black and Rogaway, 2005]. Let $\mathcal{A}$ be an adversary that expects two permutations (as in the given game). The adversary's goal here is to find which distribution the oracles it was given come from. On one hand, there are two independent random permutations, and on the other hand there is a random permutation that simulates two permutations with a random constant.

We prove that the distributions are equal unless the adversary makes two queries $x$ and $y$ to $[O]_1$ and $[O]_2$ such that $[O]_1(x) = [O]_2(y)$. When two independent permutations are used, this may happen with low probability for any pair $(x, y)$. On the other hand, when the second permutation is a masked version of the first, this can only occur when $x \oplus y = k$. Once such a pair of queries has been found, the adversary can decide with very high probability which oracles she is interacting with by simply checking, for some $z \neq x$ whether $[O]_1(z) = [O]_2(z \oplus x \oplus y)$, which is very unlikely if $[O]_1$ and $[O]_2$ are independent, but will hold with probability 1 otherwise.

We further prove that an adversary that makes such a pair of queries must have either: i. queried $x$ to $[O]_1$ and $x \oplus k$ to $[O]_2$ without knowing the value of $k$; or ii. queried $x$ to $[O]_1$ and $y \neq x \oplus k$ to $[O]_2$ and obtained $O_1(x) = O_2(y)$. We can then bound the probability of the first event by $\frac{0.25c^2}{2^n}$, and the probability of the second event by $\frac{c^2}{2^n}$. □
**Lemma 4.2.7 (Security of XCBC).** For any natural numbers $q, \sigma, n$, an adversary $\mathcal{A}$ making at most $q$ queries, of total size in the number of blocks at most $\sigma$, has a low probability of distinguishing XCBC from FCBC, when XCBC is parameterized by a random permutation and two independent random constants, and FCBC is parameterized by three independent random permutations.

$$ \mathrm{Adv}_{\mathrm{XCBC}}^{\mathrm{prf}}(\mathcal{A}) \le \mathrm{Adv}_{\mathrm{FCBC}}^{\mathrm{prf}}(\mathcal{A}) + \frac{2.5\sigma^2}{2^n} \qquad (4.3) $$

*Proof.* When an adversary succeeds in distinguishing XCBC from a random function, either it has distinguished XCBC from FCBC, or FCBC from a random function. To bound the distinguishing advantage of any adversary between FCBC and XCBC, let $\pi_1, \pi_2, \pi_3$ be three independent random permutations and $k_1, k_2$ two independent random constants. Lemma 4.2.6 is instantiated twice with the bound $\sigma$, making $\mathrm{FCBC}_{\pi_1, \pi_2, \pi_3}$ indistinguishable from $\mathrm{FCBC}_{\pi_1, \pi_1(k_1 \oplus \cdot), \pi_3}$, and indistinguishable from $\mathrm{FCBC}_{\pi_1, \pi_1(k_1 \oplus \cdot), \pi_1(k_2 \oplus \cdot)}$, i.e. $\mathrm{XCBC}_{\pi_1, k_1, k_2}$. $\square$

**A small flaw** Note that our bound on the security of XCBC is different from Black and Rogaway's [Black and Rogaway, 2005]. They instantiate their lemma called *Two Permutations From One* (Lemma 4.2.6 in the present paper) with the wrong bound on the total number of oracle queries. Indeed, the bound $c$ on the number of queries in Lemma 4.2.6 is a bound on the *total* number of oracle queries. On the other hand, in both instantiations of Lemma 4.2.6, Black and Rogaway only count the number of MAC queries that do not need padding (accounting only for queries to the first oracle in Lemma 4.2.6). The flaw is subtle, and has no effect on the security bound (which we improve below), but is present nonetheless, adding to the body of evidence that cryptographic proofs are difficult both to write and to evaluate.

**An improvement** Furthermore, to tighten the bound back, we extend Lemma 4.2.6 into the following Lemma 4.2.8, which states that a random permutation can simulate three independent random permutations using two independent random constants. Proving this lemma directly, rather than relying on Lemma 4.2.6 twice allows us to improve the bound slightly, by allowing us to count queries to the first permutation once only.

**Lemma 4.2.8.** For any natural number $c$, an adversary $\mathcal{A}$ making at most $c$ total oracle queries, with $0 < c \le 2^{n-1}$, has a low probability to distinguish between three independent permutations $(\pi_1, \pi_2, \pi_3)$ and the tuple of permutations $(\pi, \pi(k_1 \oplus \cdot), \pi(k_2 \oplus \cdot))$.

$$ \left| \mathrm{Pr} \left[ \pi_1, \pi_2, \pi_3 \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B})^3; b \leftarrow \mathcal{A}_c^{\pi_1, \pi_2, \pi_3} : b = 1 \right] - \mathrm{Pr} \left[ \pi \stackrel{\$}{\leftarrow} \mathrm{Perm}(\mathbb{B}); (k_1, k_2) \stackrel{\$}{\leftarrow} \mathbb{B}^2; b \leftarrow \mathcal{A}_c^{\pi, \pi(k_1 \oplus \cdot), \pi(k_2 \oplus \cdot)} : b = 1 \right] \right| \le \frac{1.75c^2}{2^n} $$

*Proof.* This is very similar to Lemma 4.2.6 and Lemma 4.2.9. The proof needs to bound the events $\mathrm{coll}_{\mathrm{rang}}$ (defined for Lemma 4.2.9) and another one. The bound of $\mathrm{coll}_{\mathrm{rang}}$ has been proved as a generic result and then instanciated in Lemmas 4.2.8 and 4.2.9. The probability of the other one is bounded by $\frac{0.75\sigma^2}{2^n}$. $\square$
### 4.2.4 Indistinguishability of CMAC from FCBC

The security of CMAC cannot be easily deduced from that of XCBC, since the core lemma of the security of XCBC imposes that the masks be independent from the permutation. Since this is not the case for CMAC, we use ideas from [Iwata and Kurosawa, 2003] to relate the security of CMAC to that of FCBC. Their key idea is to prevent the adversary from directly accessing the block cipher oracle by adding an independent random variable.

Our security proof generalises CMAC slightly in that we use abstract public functions $f_1, f_2: \mathbb{B} \to \mathbb{B}$ to capture the derivation of $k_2$ and $k_3$ from $\pi(0^n)$. The security of CMAC follows by instantiating $f_1 = x \mapsto 2 \times x$ and $f_2 = x \mapsto 4 \times x$.

The security of this generalised CMAC (or indeed of concrete CMAC) does not immediately follow from that of XCBC, since its constants $k_2 = f_1(\pi(0^n))$ and $k_3 = f_2(\pi(0^n))$ are not independent between themselves, and furthermore not independent from $\pi$. However, the security of CMAC is easily implied by that of FCBC, of which it is an instance. Indeed, given $\pi$,

$$CMAC_{\pi} = FCBC_{\pi, \pi(f_1(\pi(0^n))\oplus\cdot), \pi(f_2(\pi(0^n))\oplus\cdot)}$$

Here again, our security proof is close to that of [Iwata and Kurosawa, 2003], which relies on a more general construction, MOMAC, that generalises both CMAC and FCBC. We provide a game-based proof and go into more details.

#### MOMAC

The MOMAC construction [Iwata and Kurosawa, 2003] is parameterised by 6 oracles $O_{1\le i\le 6}$, which are used as follows.

$$MOMAC_{O_1, O_2, O_3, O_4, O_5, O_6}(m) := \begin{cases} O_5(\text{pad}(m)) & \text{if } 0 \le |m| < n \\ O_3(m) & \text{if } |m| = n \\ FCBC_{O_1, O_4, O_6}(m) & \text{if } n < |m| \le 2n \\ FCBC_{O_2, O_4, O_6}(m_{O_1}) & \text{if } 2n < |m| \wedge \lceil|m|/n \rceil = m \end{cases}$$

when $m_{O_1} = (O_1(m_1) \oplus m_2) \parallel \dots \parallel m_m$.

The resulting construction is also illustrated in Figure 4.7.

<figure><img src="image_70.png" /><figcaption>Figure 4.7 – Illustration of MOMAC, by increasing size order: $|m| < n$, $|m| = n$, $2n < |m| < 3n$, $|m| = 3n$,</figcaption></figure>
## CMAC and FCBC as instances of MOMAC

Given a random permutation $\pi$ and a random $n$-bit string $r$, the following six oracles $Q_{1 \le i \le 6}$, where $L^\pi = \pi(0^n)$, can be used with MOMAC to build CMAC.

$$Q_1(x) := \pi(x) \oplus r$$

$$Q_3(x) := \pi(x \oplus f_1(L^\pi))$$

$$Q_5(x) := \pi(x \oplus f_2(L^\pi))$$

$$Q_2(x) := \pi(x \oplus r) \oplus r$$

$$Q_4(x) := \pi(x \oplus r \oplus f_1(L^\pi))$$

$$Q_6(x) := \pi(x \oplus r \oplus f_2(L^\pi))$$

Given three independent random permutations $\pi_1, \pi_2, \pi_3$ and a random $n$-bit string $r$, the following six oracles $R_{1 \le i \le 6}$ can be used with MOMAC to build FCBC.

$$R_1(x) := \pi_1(x) \oplus r$$

$$R_3(x) := \pi_2(x)$$

$$R_5(x) := \pi_3(x)$$

$$R_2(x) := \pi_1(x \oplus r) \oplus r$$

$$R_4(x) := \pi_2(x \oplus r)$$

$$R_6(x) := \pi_3(x \oplus r)$$

## Security proof

For any value of $r$, the following functional equivalences follow from these definitions.

$$CMAC_{\pi} \sim MOMAC_{Q_1, Q_2, Q_3, Q_4, Q_5, Q_6}$$

$$FCBC_{\pi_1, \pi_2, \pi_3} \sim MOMAC_{R_1, R_2, R_3, R_4, R_5, R_6}$$

Therefore, distinguishing CMAC from FCBC can be reduced to distinguishing the $Q_i$ from the $R_i$. In the following, for any adversary $\mathcal{A}$, expecting six oracles and making at most $q$ oracle queries to $O_3, O_4, O_5, O_6$ and at most $\sigma$ total oracle queries before returning a boolean, we name $Q(\mathcal{A})$ (resp. $R(\mathcal{A})$) the game that initializes the oracles $Q_{1 \le i \le 6}$ (resp. $R_{1 \le i \le 6}$), then calls the adversary $\mathcal{A}^{Q_i}$ (resp. $\mathcal{A}^{R_i}$).

$$Q(\mathcal{A}) := \left[ \pi \leftarrow \text{Perm}(\mathbb{B}), r \leftarrow \mathbb{B}; b \leftarrow \mathcal{A}_{\sigma,q}^{Q_{1 \le i \le 6}} \right]$$

$$R(\mathcal{A}) := \left[ \pi_1, \pi_2, \pi_3 \leftarrow \text{Perm}(\mathbb{B}), r \leftarrow \mathbb{B}; b \leftarrow \mathcal{A}_{\sigma,q}^{R_{1 \le i \le 6}} \right]$$

**Lemma 4.2.9.** For any bijective $f_1$ and $f_2$ such that $x \mapsto x \oplus f_1(x)$, $x \mapsto x \oplus f_2(x)$, $x \mapsto f_1(x) \oplus f_2(x)$, $x \mapsto x \oplus f_1(x) \oplus f_2(x)$ are also bijective, an adversary $\mathcal{A}$, making at most $q$ oracle queries to $O_3, O_4, O_5, O_6$ and at most $\sigma$ total oracle queries, has a low probability of distinguishing the game with the $R_i$ from the game with the $Q_i$.

$$|\Pr[Q(\mathcal{A}) : b = 1] - \Pr[R(\mathcal{A}) : b = 1]| \le \frac{\sigma(\sigma + 1)}{2^n} + \frac{\frac{1}{4}(\sigma + 1)^2 + \frac{1}{2}q^2}{2^n} + \frac{\frac{3}{4}(\sigma + 1)^2}{2^n}$$

We first give an overview of the proof, using names that are defined later. The rest of this section details individual steps.

We formally prove that, for any adversary $\mathcal{A}$, the game $Q(\mathcal{A})$ is equivalent to $R(\mathcal{A})$ upto the event $\text{find}_L \lor \text{coll}_{\text{rang}}$. It is easy to bound the probability of $\text{coll}_{\text{rang}}$ occurring, but the probability of $\text{find}_L$ occurring in $R(\mathcal{A})$ requires additional work. We introduce two new games $S(\mathcal{A})$ and $T(\mathcal{A})$, represented in Figure 4.8. Game $S(\mathcal{A})$ is perfectly equivalent to $R(\mathcal{A})$, thus the probability of $\text{find}_L$ occurring is equal in both games. We then prove that $T(\mathcal{A})$ is equivalent to $S(\mathcal{A})$ upto a third event $\text{find}_r$.
<table><caption>Figure 4.8 – Sequence of games.</caption><thead><tr><th>Game</th><th>O<sub>1</sub></th><th>O<sub>2</sub></th><th>O<sub>3</sub></th><th>O<sub>4</sub></th><th>O<sub>5</sub></th><th>O<sub>6</sub></th></tr></thead><tbody><tr><td>Q(&#x1d504;)</td><td>&pi;(&middot;) &oplus; r</td><td>&pi;(&middot;r) &oplus; r</td><td>&pi;(&middot; &oplus; f<sub>1</sub>(&pi; (0<sup>n</sup>)))</td><td>&pi;(&middot;r &oplus; f<sub>1</sub>(&pi; (0<sup>n</sup>)))</td><td>&pi;(&middot; &oplus; f<sub>2</sub>(&pi; (0<sup>n</sup>)))</td><td>&pi;(&middot;r &oplus; f<sub>2</sub>(&pi; (0<sup>n</sup>)))</td></tr><tr><td>R(&#x1d504;)</td><td>&pi;<sub>1</sub>(&middot;) &oplus; r</td><td>&pi;<sub>1</sub>(&middot;r) &oplus; r</td><td>&pi;<sub>2</sub>(&middot;)</td><td>&pi;<sub>2</sub>(&middot;r)</td><td>&pi;<sub>3</sub>(&middot;)</td><td>&pi;<sub>3</sub>(&middot;r)</td></tr><tr><td>S(&#x1d504;)</td><td>&pi;<sub>1</sub>(&middot;)</td><td>&pi;<sub>1</sub>(&middot;r)</td><td>&pi;<sub>2</sub>(&middot;)</td><td>&pi;<sub>2</sub>(&middot;r)</td><td>&pi;<sub>3</sub>(&middot;)</td><td>&pi;<sub>3</sub>(&middot;r)</td></tr><tr><td>T(&#x1d504;)</td><td>&pi;<sub>1</sub>(&middot;)</td><td>&pi;<sub>1</sub>'(&middot;)</td><td>&pi;<sub>2</sub>(&middot;)</td><td>&pi;<sub>2</sub>'(&middot;)</td><td>&pi;<sub>3</sub>(&middot;)</td><td>&pi;<sub>3</sub>'(&middot;)</td></tr></tbody></table>

The following sequence of inequalities shows an outline of our detailed proof, with the justification for each non-trivial step given in the paragraph whose heading is listed beside the step.

$$
\begin{align*}
& |\Pr[Q(\mathcal{A}) : b = 1] - \Pr[R(\mathcal{A}) : b = 1]| && (\text{using } Q(\mathcal{A}) \sim R(\mathcal{A}) \text{ upto } \mathrm{coll}_{\mathrm{rang}} \lor \mathrm{find}_{\mathrm{L}}) \\
& \le \Pr[R(\mathcal{A}) : \mathrm{coll}_{\mathrm{rang}}] + \Pr[R(\mathcal{A}) : \mathrm{find}_{\mathrm{L}}] && (\text{using } R(\mathcal{A}) \sim S(\mathcal{A})) \\
& = \Pr[R(\mathcal{A}) : \mathrm{coll}_{\mathrm{rang}}] + \Pr[S(\mathcal{A}) : \mathrm{find}_{\mathrm{L}}] \\
& \le \Pr[R(\mathcal{A}) : \mathrm{coll}_{\mathrm{rang}}] + \Pr[T(\mathcal{A}) : \mathrm{find}_{\mathrm{L}}] + |\Pr[S(\mathcal{A}) : \mathrm{find}_{\mathrm{L}}] - \Pr[T(\mathcal{A}) : \mathrm{find}_{\mathrm{L}}]| && (\text{using } S(\mathcal{A}) \sim T(\mathcal{A}) \text{ upto } \mathrm{find}_{\mathrm{r}}) \\
& \le \Pr[R(\mathcal{A}) : \mathrm{coll}_{\mathrm{rang}}] + \Pr[T(\mathcal{A}) : \mathrm{find}_{\mathrm{L}}] + \Pr[T(\mathcal{A}) : \mathrm{find}_{\mathrm{r}}]
\end{align*}
$$

The conclusion then only needs to bound the probability of $\mathrm{coll}_{\mathrm{rang}}$ and $\mathrm{find}_{\mathrm{r}}$ in $T(\mathcal{A})$. We now discuss individual steps in the proof, including definitions for the events. In Figure 4.8 and below, $L^\pi$ denotes the value $\pi(0^n)$ and $L_i^\pi$ denotes the value $f_i(L^\pi)$ for $i \in \{1, 2\}$.

$$Q(\mathcal{A}) \sim R(\mathcal{A}) \text{ upto } \mathrm{coll}_{\mathrm{rang}} \lor \mathrm{find}_{\mathrm{L}}$$

In a proof reminiscent of that of Lemma 4.2.6, we note that games $Q(\mathcal{A})$ and $R(\mathcal{A})$ are equivalent unless $\mathcal{A}$ queries some $x$ to $O_i$ and some $y$ to $O_j$, with $(i, j) \in \{(1, 3), (1, 5), (3, 5)\}$ and such that $O_i(x) = O_j(y)$. If this event (which we simply call bad below) occurs, then $\mathcal{A}$ can distinguish the two sets of oracles with high probability by testing, for some $z \neq x$ whether $O_i(z) = O_j(z \oplus x \oplus y)$. We now prove that event bad as defined above completely captures all cases in which the two games can be distinguished. To simplify bounding the probability of bad occurring, we consider instead a disjunction of two disjoint events $\mathrm{find}_L$ and $\mathrm{coll}_{\mathrm{rang}}$, depending on the value of $x \oplus y$. Event $\mathrm{find}_L$ occurs if $\mathcal{A}$ queries, for some $x$:

- $O_1(x)$ and $O_3(x \oplus f_1(L^\pi))$; or

- $O_1(x)$ and $O_5(x \oplus f_2(L^\pi))$; or

- $O_3(x)$ and $O_5(x \oplus f_1(L^\pi) \oplus f_2(L^\pi))$.

Event $\mathrm{coll}_{\mathrm{rang}}$ captures the remainder of the cases in bad, and thus occurs when $\mathcal{A}$ queries, for some $x$ and $y$:

- $O_1(x)$ and $O_3(y)$ such that $O_1(x) = O_3(y)$ and $y \neq x \oplus f_1(L^\pi)$; or

- $O_1(x)$ and $O_5(y)$ such that $O_1(x) = O_5(y)$ and $y \neq x \oplus f_2(L^\pi)$; or

- $O_3(x)$ and $O_5(y)$ such that $O_3(x) = O_5(y)$ and $y \neq x \oplus f_1(L^\pi) \oplus f_2(L^\pi)$.

We consider two games $X_1(\mathcal{A})$ and $X_2(\mathcal{A})$, which are respectively equivalent to $Q(\mathcal{A})$ and $R(\mathcal{A})$. $X_1(\mathcal{A})$ and $X_2(\mathcal{A})$ are shown in Figure 4.9, where code inside the dotted boxes appears only in $X_1(\mathcal{A})$. Figure 4.9 only shows definitions for $O_1$, $O_3$ and $O_5$, which are sufficient to define the entire games. Indeed, we note that, in both $Q(\mathcal{A})$ and $R(\mathcal{A})$, we have $O_2(x) = O_1(x \oplus L_1^\pi)$ and that $O_4$ and $O_3$, and $O_6$ and $O_5$ obey the same relation.
$X_1(\mathcal{A})$ or $X_2(\mathcal{A})$
$\pi, \pi_1, \pi_2, \pi_3 \leftarrow$ Undefined
$L \stackrel{\$}{\leftarrow} \mathbb{B}$
$\pi[0^n] \leftarrow L$
$\pi_1[0^n] \leftarrow L$
$r \stackrel{\$}{\leftarrow} \mathbb{B}$
$\text{coll}_{\text{rang}} \leftarrow$ false
$\text{find}_L \leftarrow$ false
$b \leftarrow \mathcal{A}_{\sigma,q}^{O_1, O_3, O_5}$

$O_1(m)$

if ($m \in \text{dom}(\pi_1)$)

return $\pi_1[m]$

else if ($m \in \text{dom}(\pi)$)

$\text{find}_L \leftarrow$ true

$\pi_1[m] \leftarrow \pi[m]$

$y \stackrel{\$}{\leftarrow} \mathbb{B} \setminus \text{rang}(\pi_1)$

if ($y \in \text{rang}(\pi)$)

$\text{coll}_{\text{rang}} \leftarrow$ true

$y \stackrel{\$}{\leftarrow} \mathbb{B} \setminus \text{rang}(\pi)$

$\pi_1[m] \leftarrow y$

$\pi[m] \leftarrow y$

return y

$O_3(m)$

if ($m \in \text{dom}(\pi_2)$)

return $\pi_2[m]$

else if ($m \oplus f_1(L) \in \text{dom}(\pi)$)

$\text{find}_L \leftarrow$ true

$\pi_2[m] \leftarrow \pi[m \oplus f_1(L)]$

$y \stackrel{\$}{\leftarrow} \mathbb{B} \setminus \text{rang}(\pi_2)$

if ($y \in \text{rang}(\pi)$)

$\text{coll}_{\text{rang}} \leftarrow$ true

$y \stackrel{\$}{\leftarrow} \mathbb{B} \setminus \text{rang}(\pi)$

$\pi_2[m] \leftarrow y$

$\pi[m \oplus f_1(L)] \leftarrow y$

return y

$O_5(m)$

if ($m \in \text{dom}(\pi_3)$)

return $\pi_3[m]$

else if ($m \oplus f_2(L) \in \text{dom}(\pi)$)

$\text{find}_L \leftarrow$ true

$\pi_3[m] \leftarrow \pi[m \oplus f_2(L)]$

$y \stackrel{\$}{\leftarrow} \mathbb{B} \setminus \text{rang}(\pi_3)$

if ($y \in \text{rang}(\pi)$)

$\text{coll}_{\text{rang}} \leftarrow$ true

$y \stackrel{\$}{\leftarrow} \mathbb{B} \setminus \text{rang}(\pi)$

$\pi_3[m] \leftarrow y$

$\pi[m \oplus f_2(L)] \leftarrow y$

return y

<caption>Figure 4.9 – Games $X_1(\mathcal{A})$ (including dotted boxes) and $X_2(\mathcal{A})$ (excluding dotted boxes).</caption>

Figure 4.9 shows very clearly that $Q(\mathcal{A})$ (or $X_1$) and $R(\mathcal{A})$ (or $X_2$) cease to be equivalent only when one of $\text{find}_L$ or $\text{coll}_{\text{rang}}$ becomes true. Thus, we have:

$$ \begin{align*} & |\text{Pr}[Q(\mathcal{A}) : b = 1] - \text{Pr}[R(\mathcal{A}) : b = 1]| \\ &= |\text{Pr}[X_1(\mathcal{A}) : b = 1] - \text{Pr}[X_2(\mathcal{A}) : b = 1]| \\ &\le \text{Pr}[X_2(\mathcal{A}) : \text{coll}_{\text{rang}} \lor \text{find}_L] \\ &\le \text{Pr}[X_2(\mathcal{A}) : \text{coll}_{\text{rang}}] + \text{Pr}[X_2(\mathcal{A}) : \text{find}_L] \end{align*} $$

**Bounding** $\text{Pr}[X_2(\mathcal{A}) : \text{coll}_{\text{rang}}]$

We note that $\text{coll}_{\text{rang}}$ is essentially the probability of a freshly sampled variable already appearing in some set. This can easily be bound, knowing that the total number of oracle queries is at most $\sigma \le 2^{n-1}$.
For any adversary $\mathcal{A}$ that makes at most $\sigma$ oracle queries, we have,

$$ \Pr[X_2(\mathcal{A}) : \mathrm{coll}_{\mathrm{rang}}] \le \frac{\sigma(\sigma+1)}{2} \cdot \frac{1}{2^n - (\sigma+1)} \le \frac{\sigma(\sigma+1)}{2^n} $$

$$ R(\mathcal{A}) \sim S(\mathcal{A}) $$

Event $\mathrm{find}_L$ in game $X_2(\mathcal{A})$ can also be expressed as follows.

$$ \mathrm{find}_L \iff \bigvee \left\{ \begin{array}{ll} L_1^{\pi_1} & \in \mathrm{dom}(\pi_1) \oplus \mathrm{dom}(\pi_2), \\ L_2^{\pi_1} & \in \mathrm{dom}(\pi_1) \oplus \mathrm{dom}(\pi_3), \\ L_1^{\pi_1} \oplus L_2^{\pi_1} & \in \mathrm{dom}(\pi_2) \oplus \mathrm{dom}(\pi_3) \end{array} \right\} $$

Its probability cannot be computed directly in $X_2(\mathcal{A})$, since the collision involves $L^\pi$, which is not independent from the adversary's view. We therefore need to modify $X_2(\mathcal{A})$ somewhat into a game $S(\mathcal{A})$ shown in Figure 4.10 to bound this probability. The objective of game $S(\mathcal{A})$ is to extend the $\mathrm{find}_L$ event to include fresh and independent randomness $r$ in its definition. This will then enable us to make use of it to bound the probability of $\mathrm{find}_L$, since it is independent from the oracles' outputs. It is easy to see that for any adversary $\mathcal{A}$, $S(\mathcal{A})$ is perfectly equivalent to $X_2(\mathcal{A})$. We formally prove

$$ \Pr[X_2(\mathcal{A}) : \mathrm{find}_L] = \Pr[S(\mathcal{A}) : \mathrm{find}_L] $$

**Event find$_L$ in game $S(\mathcal{A})$**

In game $X_2(\mathcal{A})$, the value of $L^{\pi_1}$ as it appears in event $\mathrm{find}_L$ is equal to $\pi_1(0^n)$. In game $S(\mathcal{A})$, its value is related to $r$ is equal to $r \oplus \pi_1(0^n)$. Event $\mathrm{find}_L$ in game $S(\mathcal{A})$ can now be expressed as follows.

$$ \mathrm{find}_L \iff \bigvee \left\{ \begin{array}{ll} f_1(L^{\pi_1} \oplus r) & \in \mathrm{dom}(\pi_1) \oplus \mathrm{dom}(\pi_2), \\ f_2(L^{\pi_1} \oplus r) & \in \mathrm{dom}(\pi_1) \oplus \mathrm{dom}(\pi_3), \\ f_1(L^{\pi_1} \oplus r) \oplus f_2(L^{\pi_1} \oplus r) & \in \mathrm{dom}(\pi_2) \oplus \mathrm{dom}(\pi_3) \end{array} \right\} $$

$$ S(\mathcal{A}) \sim T(\mathcal{A}) \text{ upto } \mathrm{find}_r $$

As it stands in game $S(\mathcal{A})$, the use of $r$ in $\mathrm{find}_L$ is not sufficient to allow us to bound its probability of occurring. To do so, we wish to show that it is possible to delay sampling $r$ until the end of the game. However, $r$ is correlated to the output of oracles $S_2$, $S_4$ and $S_6$. Again, we observe that $r$ is a random value, unknown to the adversary, and independent from the permutations. Rather than using this fact as in Lemma 4.2.6 to replace the three permutations and their re-randomised version with six truly independent permutations, we simply use it to replace the three permutations with six permutations that are simply independent from the value of $r$.

In our formal proof, we use three pairs of incomplete functions $(\pi_i, \pi'_i)$ that are guaranteed to never output the same result for any fresh input. We implement this by sampling each new fresh output from the uniform distribution over $\mathbb{B} \setminus (\mathrm{rang}(\pi_i) \cup \mathrm{rang}(\pi'_i))$. The games we use to formally prove that $(\pi_1, \pi'_1)$ are equivalent to $(\pi_1, \pi_1(\cdot \oplus r))$ upto the event $\mathrm{find}_r$ are illustrated in Figure 4.10. We extend this definition to $(\pi_2, \pi'_2)$ and $(\pi_3, \pi'_3)$ and name $T(\mathcal{A})$ the game that uses the corresponding definitions for $O_{1 \le i \le 6}$ (which can be seen in Figure 4.8).
<figure><img src="image_71.png" /><figcaption>Figure 4.10 – Games $S(\mathcal{A})$ (including dotted boxes) and $T(\mathcal{A})$ (excluding dotted boxes).</figcaption></figure>

Thanks to this more flexible goal we need only consider a smaller event, $find_r$, whose occurrence allows the adversary to distinguish between the $S_i$ and the $T_i$. In essence, $find_r$ corresponds in this setting to the coll$_{rang}$ event from the first step. With this in mind, it is easy to prove that the behaviour of $S(\mathcal{A})$ and $T(\mathcal{A})$ can only diverge if $find_r$ occurs. This allows us to prove the following inequality.

$$|\Pr[S(\mathcal{A}) : find_L] - \Pr[T(\mathcal{A}) : find_L]| \le \Pr[T(\mathcal{A}) : find_r]$$

**Bounding $\Pr[T(\mathcal{A}) : find_r]$**

As when bounding $find_L$ earlier, we note that $find_r$ is the probability of a freshly sampled value already appearing in a set. For all adversary $\mathcal{A}$ that makes at most $q$ to $O_3$, $O_4$, $O_5$ and $O_6$, and at most $\sigma$ total oracle queries, we have

$$\Pr[T(\mathcal{A}) : find_r] \le \frac{1}{4} \frac{(\sigma + 1)^2}{2^n} + \frac{1}{2} \frac{q^2}{2^n}$$

The proof relies on the fact that, $\forall x, y, z$, if $0 \le x + y \le z$ then $xy \le \frac{z^2}{4}$, which allows us to clean complex bounds.

**Bounding $\Pr[T(\mathcal{A}) : find_L]$**

It now remains to bound the probability that $find_L$ occurs in $T(\mathcal{A})$. As shown in Figure 4.8, game $T(\mathcal{A})$ no longer uses the value of $r$, and that variable can therefore be leveraged to bound the probability of $find_L$.

Therefore, we can use the randomness of $r$ to bound the probability of $find_L$ in $T(\mathcal{A})$. The transformation from $S(\mathcal{A})$ to $T(\mathcal{A})$ have modified $find_L$, in the sense that every occurrence of $dom(\pi_i)$ is now replaced by $dom(\pi_i) \cup dom(\pi'_i)$, for $i \in \{1, 2, 3\}$. To simplify all this, $find_L$ is equivalent to a disjunction of six sub-events. Denoting $D_i := dom(\pi_i)$ and $D'_i := dom(\pi'_i)$, $find_L$ can be expressed, as it appears in $T(\mathcal{A})$ as follows.
$$ \text{find}_L \iff \bigvee \left\{ \begin{array}{ll} f_1(L^{\pi_1} \oplus r) & \in (D_1 \oplus D_2) \cup (D'_1 \oplus D'_2), \\ r \oplus f_1(L^{\pi_1} \oplus r) & \in (D_1 \oplus D'_2) \cup (D'_1 \oplus D_2), \\ f_2(L^{\pi_1} \oplus r) & \in (D_1 \oplus D_3) \cup (D'_1 \oplus D'_3), \\ r \oplus f_2(L^{\pi_1} \oplus r) & \in (D_1 \oplus D'_3) \cup (D'_1 \oplus D_3), \\ f_1(L^{\pi_1} \oplus r) \oplus f_2(L^{\pi_1} \oplus r) & \in (D_2 \oplus D_3) \cup (D'_2 \oplus D'_3), \\ r \oplus f_1(L^{\pi_1} \oplus r) \oplus f_2(L^{\pi_1} \oplus r) & \in (D_2 \oplus D'_3) \cup (D'_2 \oplus D_3) \end{array} \right\} $$

Recall that $f_1, f_2, x \mapsto x \oplus f_1(x), x \mapsto x \oplus f_2(x), x \mapsto f_1(x) \oplus f_2(x)$ and $x \mapsto x \oplus f_1(x) \oplus f_2(x)$ are bijective. Thus, for any adversary $\mathcal{A}$ that makes at most $\sigma$ total queries to its oracles, we can prove that

$$ \Pr[T(\mathcal{A}) : \text{find}_L] \le \frac{3(\sigma + 1)^2}{4} $$

This concludes the proof of Lemma 4.2.9, and we can now seek to apply it to the security of CMAC.

**Lemma 4.2.10 (Indistinguishability of CMAC and FCBC).** For any natural numbers $q, \sigma, n$, an adversary $\mathcal{A}$ making at most $q$ queries, of total size in the number of blocks of at most $\sigma$, has a low probability of distinguishing CMAC from FCBC, when CMAC is parameterized by a random permutation and FCBC is parameterized by three independent random permutations.

$$ \mathrm{Adv}_{\mathrm{CMAC}}^{\mathrm{prf}}(\mathcal{A}) \le \mathrm{Adv}_{\mathrm{FCBC}}^{\mathrm{prf}}(\mathcal{A}) + \frac{2(\sigma + 1)^2}{2^n} + \frac{0.5q^2}{2^n} \quad (4.4) $$

*Proof.* This is a direct application of the definition of MOMAC and Lemma 4.2.9. In CMAC, the assumptions involving bijections are reduced in GF$(2^n)$ to the fact that, for every $p \in \{x, x \oplus 1, x^2, x^2 \oplus 1, x^2 \oplus x, x^2 \oplus x \oplus 1\}$, the function $q \mapsto p \times q$ is bijective. $\square$

**Theorem 4.2.11 (Security of CMAC).** For any natural numbers $q, l, \sigma, n$, an adversary $\mathcal{A}$ making at most $q$ queries, each query of maximum size $\lceil n \rceil$ and of total size in the number of blocks of at most $\sigma$, has a low probability of distinguishing CMAC from a random function, when parameterized by a random permutation.

$$ \mathrm{Adv}_{\mathrm{CMAC}}^{\mathrm{prf}}(\mathcal{A}) \le \frac{2.5(\sigma + 1)^2 + 1.5q^2 + 2q^2l^2}{2^n} \quad (4.5) $$

*Proof.* This is a direct application of Theorem 4.2.3, Theorem 4.2.5 and Lemma 4.2.10. $\square$
# Part III

## Cryptographic Hash Function
<figure><img src="image_72.png" /></figure>
# Chapter 5

## Security of a Hash Function

A *hash function* is a mathematical algorithm that maps data of *arbitrary size* (called the message) to a *fixed-size* bitstring (called a *hash value*, *hash*, or *message digest*). A *crypto-graphic hash function* — also called a *one-way hash function* — is an efficient deterministic hash function that is almost infeasible to invert, i.e. given a hash *h*, finding a message whose hash value is *h* would be so expensive that it would take millions of years to compute.

Ideally, the only way to find a message that produces a given hash is to attempt a brute-force search of possible inputs and hope to find a match. One can use rainbow tables<fnref n="1" /> [Oechslin, 2003] to improve brute-force techniques, but for a secure hash function, it should still be too expensive in time and memory.

<figure><img src="image_73.png" /></figure>

**Example**

In a database that stores user passwords for authenticity, one can store them in plaintext. However any leak may reveal all the users' password, compromising later authentication. As a solution (simple and not sufficient), one can store the password hashes so that it should be difficult – nearly impossible – to anyone stealing the database to learn user passwords.

### 5.1 Security Definitions and Formalization

The ideal cryptographic hash function has the following main properties.

**Determinism:** The same message always results in the same hash.

**Efficiency:** The computation of a hash value for any given message is efficient.

**Preimage resistance:** It is infeasible to generate a message that yields a given hash value.

**Second preimage resistance:** It is infeasible to find another message that shares the same hash value as a given one.

**Collision resistance:** It is infeasible to find two different messages sharing the same hash.

**Pseudo-random:** A small change to a message should change the hash value so extensively that the new hash value appears uncorrelated with the old hash value.

I give the formalization of the three resistances in the next paragraphs. Then, using the definition of a random function from Section 2.3.2, I give the advantage of any adversary for each resistance against a random function, concluding that a random function is secure.

<footnote n="1">1. A rainbow table is a table that stores all computed hashes.</footnote>
<figure><img src="image_74.png" /></figure>

## EasyCrypt

In the formalization of the signature of a hash function, I use an option type to express the validity of a query, as it answers None when the query is prohibited.

```typescript
module type HashFunction = {
  proc init () : unit
  proc get (m : message) : hash option
}.
```

In the formalization of the security statement in the next chapter, the number of queries an adversary can make is bounded by a fixed value, here named bound.

```typescript
op bound : int.
axiom bound_gt0 : 0 < bound.
```

However, only the number of queries may not be enough to express more complex costs of queries, since some queries may be more costly than others in different models. Therefore, we generalize the function `increase_counter` that increases the counter instead of only increment it. This generalization is implemented using abstract operators in the general theory, and then, when the theory is used in a more defined model, one should clone this theory and instantiate the query cost function.

```typescript
op increase_counter : int → message → int.
```

The module `Bounder` encapsulates the validity of queries in terms of the accumulated cost of queries allowed. For each query, it tests if the increased counter stays below the bound. In this case it actually increases the counter and returns the hash value, otherwise it returns the default value `None`.

```typescript
module Bounder (F : HashFunction) : HashFunction = {
  var bounder : int
  proc init () : unit = { bounder ← 0; F.init(); }
  proc get(x : message) : hash option = {
    var y : hash option ← None;
    if (increase_counter bounder x ≤ bound) {
      bounder ← increase_counter bounder x;
      y ← F.get(x);
    }
    return y;
  }}.
```

## Preimage Advantage

<figure><img src="image_75.png" /></figure>

## EasyCrypt

```typescript
module Preimage (A : AdvPreimage, F : HashFunction) = {
  module O = Bounder(F)
  proc main (t : hash) : bool = {
    var m, t¹;
    O.init();
    m ← A(O).guess(t);
    t¹ ← O.get(m);
  }
}
```
```pascal
return t' = Some t;
}}.
```

The preimage advantage of any adversary $\mathcal{A}$ making at most bound queries against a hash function $h$ is defined for every hash value $t$ as:

$$ \mathrm{Adv}_h^{p1}(\mathcal{A}, t) := \Pr[\mathrm{Preimage}(\mathcal{A}, h).\mathrm{main}(t) : \mathrm{res}] $$

## Second Preimage Advantage

### EasyCrypt

```pascal
module SecondPreimage (A : AdvSecondPreimage, F : HashFunction) = {
  module O = Bounder(F)
  proc main (m1 : message) : bool = {
    var m2, t1, t2;
    O.init();
    m2 ← A(O).guess(m1);
    t1 ← O.get(m1);
    t2 ← O.get(m2);
    return m1 ≠ m2 ∧ ∃ h, t1 = Some h ∧ t2 = Some h;
  }}.
```

The second preimage advantage of any adversary $\mathcal{A}$ making at most bound queries against a hash function $h$ is defined for all message $m_1$ as:

$$ \mathrm{Adv}_h^{p2}(\mathcal{A}, m_1) := \Pr[\mathrm{SecondPreimage}(\mathcal{A}, h).\mathrm{main}(m_1) : \mathrm{res}] $$

## Collision Advantage

### EasyCrypt

```pascal
module Collision (A : AdvCollision, F : HashFunction) = {
  module O = Bounder(F)
  proc main () : bool = {
    var m1, m2, t1, t2;
    O.init();
    (m1,m2) ← A(O).guess();
    t1 ← O.get(m1);
    t2 ← O.get(m2);
    return m1 ≠ m2 ∧ ∃ h, t1 = Some h ∧ t2 = Some h;
  }}.
```

The collision advantage of any adversary $\mathcal{A}$ making at most bound queries against a hash function $h$ is defined as:

$$ \mathrm{Adv}_h^{\mathrm{coll}}(\mathcal{A}) := \Pr[\mathrm{Collision}(\mathcal{A}, h).\mathrm{main}() : \mathrm{res}] $$
## 5.2 Random Function Security

The ideal version of a hash function is a random function, already defined in Section 2.3.2. In this section, I only give the upper bound of each advantage against a random function and do not describe the EasyCrypt formal proofs as the techniques are already described in the previous chapters.

### EasyCrypt

In this section, the abstract function increase_counter is instanciated by the function that increases by 1 its first input, regardless of its second input.

clone Hash as MyHash with
op increase_counter ← fun (c : int) (_ : message) ⇒ c + 1.

Against a random function, an adversary has a low probability to find a preimage.

**Theorem 5.2.1 (Preimage resistance of a random function).** For any hash value $t \in S$, the preimage advantage of any adversary $\mathcal{A}$ that queries its oracle at most $\sigma$ times against a random function is bounded by:

$$ \mathrm{Adv}_{\mathrm{F}}^{\mathrm{p}1}(\mathcal{A}, t) \leq \frac{\sigma + 1}{|S|} $$

Against a random function, an adversary has a low probability to find a second preimage.

**Theorem 5.2.2 (Second preimage resistance of a random function).** For any message $m_1$, the second preimage advantage of any adversary $\mathcal{A}$ that queries its oracle at most $\sigma$ times against a random function is bounded by:

$$ \mathrm{Adv}_{\mathrm{F}}^{\mathrm{p}2}(\mathcal{A}, m_1) \leq \frac{\sigma + 1}{|S|} $$

Against a random function, an adversary has a low probability to find a collision.

**Theorem 5.2.3 (Collision resistance of a random function).** The collision advantage of any adversary $\mathcal{A}$ that queries its oracle at most $\sigma$ times against a random function is bounded by:

$$ \mathrm{Adv}_{\mathrm{F}}^{\mathrm{coll}}(\mathcal{A}) \leq \frac{\sigma^2 - \sigma + 2}{2|S|} $$

## 5.3 Indifferentiability, not indistinguishability

A hash function is by definition publicly known, as opposed to a MAC scheme that includes a secret key. Therefore, any hash function that is built upon a permutation should provide security (preimage, second preimage, and collision resistances) when the underlying permutation is publicly known. This is translated by giving to the adversary direct access to the permutation. Introduced by Maurer, Renner, and Holenstein in [Maurer et al., 2004], the notion of *indifferentiability* generalizes over the standard notion of *indistinguishability* by considering settings where the adversary has oracle access to both the construction and its underlying primitive.
It has been used as a way of reducing concerns in the design of block ciphers (with proofs for Feistel networks [Dachman-Soled et al., 2016, Dai and Steinberger, 2016b] and substitution-permutation networks [Cogliati et al., 2018]) and hash functions (with proofs for the Merkle-Damgård construction [Coron et al., 2005] and the SPONGE construction [Bertoni et al., 2008]). In each case, it formally captures the intuition that the construction does not introduce any structural vulnerabilities when the underlying primitive is seen as an ideal black-box permutation.

<figure><img src="image_76.png" /><figcaption>Figure 5.1 – Indifferentiability</figcaption></figure>

**Definition 5.3.1** (Indifferentiability [Maurer et al., 2004]). A construction C with oracle access to an ideal primitive F is said to be $(q_D, q_S, \epsilon)$-indifferentiable from an ideal functionality G if there exists a simulator P with oracle access to G such that for any distinguisher D that makes queries of total cost at most $q_D$, and $P[G]$ makes at most $q_S$ queries to G, when:

$$|\Pr[b \leftarrow D^{C[F],F}: b = 1] - \Pr[b \leftarrow D^{G,P[G]}: b = 1]| < \epsilon$$

<figure><img src="image_77.png" /></figure>

EasyCrypt

*type* state, message, thash.

*module type* Primitive = {

*proc* init () : unit

*proc* f (x : state) : state

*proc* fi (x : state) : state

}.

*module type* Functionality = {

*proc* init () : unit

*proc* f (x : message) : thash list

}.

*module type* Construction (F : Primitive) = Functionality.

*module type* Simulator (P : Functionality) = Primitive.

*module type* Adversary (Fun : Functionality) (Prim : Primitive) = {
  *proc* guess () : bool { Fun.f Prim.f Prim.fi } (* accessible oracles *)
}.

*module* Real (D : Adversary) (C : Construction) (F : Primitive) = {

*proc* game = A(C(F),F).guess

}

*module* Ideal (A : Adversary) (G : Functionality) (P : Simulator) = {

*proc* game = A(G,P(G)).guess
}

## 5.4 Security from Indifferentiability

When the adversary has access to the underlying permutation, it changes the security bounds of collision resistance and first- and second-preimage resistance in the sense that the query cost is not the number of queries the adversary calls the hash function. Instead the query cost is defined as the number of primitive calls incurred by the combined queries to the construction and to the primitive itself.

### EasyCrypt

In this case, the abstract function increase_counter is instanciated as follows, using an abstract operator pad, for which an instanciation is defined in Section 6.1.

type block, message.

op pad : message → block list.

clone Hash as MyHash with

op increase_counter ← fun (c : int) (l : message) ⇒ c + size (pad l).

**Theorem 5.4.1 (Preimage resistance from indifferentiability).** The advantage of any adversary $\mathcal{A}$ to succeed in producing a preimage for a construction $C(P)$ (over the primitive P) that is $(\sigma, \sigma, \epsilon)$-indifferentiable from a random oracle is bounded by:

$$ \mathrm{Adv}_{C(P)}^{p1}(\mathcal{A}) \leq \frac{\sigma + 1}{|S|} + \epsilon $$

**Theorem 5.4.2 (Second-preimage resistance from indifferentiability).** The advantage of any adversary $\mathcal{A}$ to succeed in producing a second-preimage for a construction $C(P)$ (over the primitive P) that is $(\sigma, \sigma, \epsilon)$-indifferentiable from a random oracle is bounded by:

$$ \mathrm{Adv}_{C(P)}^{p2}(\mathcal{A}) \leq \frac{\sigma + 1}{|S|} + \epsilon $$

**Theorem 5.4.3 (Collision resistance from Indifferentiability).** The advantage of any adversary $\mathcal{A}$ to succeed in producing a collision for a construction $C(P)$ (over the primitive P) that is $(\sigma, \sigma, \epsilon)$-indifferentiable from a random oracle is bounded by:

$$ \mathrm{Adv}_{C(P)}^{\mathrm{coll}}(\mathcal{A}) \leq \frac{\sigma^2 - \sigma + 2}{2|S|} + \epsilon $$

### Remark

The results in this chapter are part of my personal contributions and are proven generally (for all constructions and primitives).
# Chapter 6

## SHA3's Formal Security Proof
[Almeida et al., 2019b]

<figure><img src="image_78.png" /></figure>

**Remark**

This chapter's content has been published at CCS 2019 in [Almeida et al., 2019b].
I am using the text of our joint work with their agreement. My contributions will be
made clear when the description matches the boundaries of my personal contributions.

A stated goal of recent competitions for cryptographic standards is to gain trust from the broad cryptographic community through open and transparent processes. These processes generally involve open-source reference and optimized implementations for performance evaluation, rigorous security analysis for provable security evaluation, and, often, informal evaluation of security against side-channel attacks.

These artifacts contribute to building trust in candidates, and ultimately in the new
standard. However, the disconnect between implementation and security analyses is a major
cause of concern. Our paper [Almeida et al., 2019b] explores how formal approaches could
eliminate this disconnect and bring together implementation (most importantly, efficient
implementations) and software artifacts, in particular machine-checked proofs, supporting
security analyses. We put forward four desirable properties for formal approaches:

- *functional correctness*: efficient implementations should be proved equivalent to reference implementations and to algorithmic specifications of the standardized cryptographic construction that are both human-readable and interpreted by machines. Such specifications and implementations should be *proved* to have the same input/output behavior (or interactive behavior in protocols);

- *provable security*: rigorous security proofs should be provided both for algorithms and for implementations. For the highest level of assurance, security proofs should be machine-checked and establish guarantees for the (machine-readable) algorithmic specifications. Security for both efficient and reference implementations will follow from the functional correctness proofs, using the baseline adversarial models from provable security;

- *side-channel resistance*: implementations should be provably secure against side-channel attacks, in relevant ideal models. For instance, it is commonly required that implementations are secure in an abstract model of timing, where implementations leak secrets if they contain secret dependent memory-accesses or control-flow instructions, a notion known as "cryptographic constant-time". Combined with provable security,
it entails security in a stronger adversarial model where side-channel leakage is available to the adversary;

- *efficiency*: formal proofs should remain fully compatible with efficiency considerations. They should neither constrain in any way the code of the implementations (although constrained intermediate implementations could be used as proof artifacts) nor impact its performance.

We demonstrate through a relevant use case of the feasibility of formal approaches concerning the stated goals of functional correctness, provable security, side-channel resistance, and efficiency. Our use case is the SHA3 standard [Dworkin, 2015], the last member of the Secure Hash Algorithm family released by NIST in 2015. Our choice is guided by two main considerations. Firstly, the SHA3 standard will likely be used to protect real-world applications for many years to come. Secondly, its security proof is intricate and involves techniques that are not routinely addressed in machine-checked security proofs.

Concretely, our implementation is written in Jasmin (described in [Almeida et al., 2017], with another use case in [Almeida et al., 2019a]), a framework that targets high-assurance and high-speed implementations using “assembly in the head” (a mixture of high-level and low-level, platform-specific programming) and a formally verified and predictable compiler which empowers programmers to write highly efficient fine-tuned code. The generated (verified) x86-64 assembly code matches in performance the best available implementations for this primitive, including for example a current OpenSSL version. Machine-checked proofs of equivalence and provable security are developed in EasyCrypt, using the embedding developed in [Almeida et al., 2019a]. More precisely, as illustrated in Figure 6.1, we establish:

- *functional correctness*: the highly efficient implementations are proved functionally equivalent to a readable Jasmin reference implementation of the SHA3 standard;

- *provable security*: we prove that the SPONGE <fnref n="1" /> construction is indifferentiable from a random oracle when the underlying permutation is modeled as a random object. From this result we derive concrete bounds for the standard notions of collision-resistance and resistance against first- and second-preimage attacks in the random permutation model;

- *side-channel resistance*: we prove that the implementation only leaks the length of public data, in the abstract model of timing used to reason about “cryptographic constant-time”. This property is useful when the hash function is integrated into higher-level primitives, say key-derivation functions, when hashed inputs are secret.

Our results are established at different levels. Our provable security analysis is based on an EasyCrypt model of the SPONGE construction, which matches the (bit-oriented) specification in the SHA3 standard. At this level, we adopt the standard approach for cryptographic proofs of indifferentiability and treat the underlying permutation as an ideal object. In contrast, constant-time security is therefore established as close to the computational platform as possible. Our analysis of potential timing side-channels is carried out over highly optimized (byte- and word-oriented) Jasmin implementations of SHA3.

We then use automatic extraction and equivalence proofs in EasyCrypt to bridge these two levels of results. First, our optimized Jasmin implementations are proved equivalent to a readable reference implementation of the standard, which includes the SHA3 permutation. Finally, we also prove that the model of the SPONGE that proved theoretically secure is

<footnote n="1">1. The construction is described in more details in Section 6.1.</footnote>
<figure><img src="image_79.png" /><figcaption>Figure 6.1 – Our results. Full lines represent extraction to EasyCrypt and compilation to assembly by the Jasmin compiler. Dashed lines represent equivalence and security proofs, formalized in EasyCrypt.</figcaption></figure>

functionally equivalent to the Jasmin reference implementation of this construction when instantiated with the same permutation. This establishes a link between theoretical security and implementation security.

<figure><img src="image_80.png" /></figure>

**Remark**

All proof and implementation artifacts are available from https://gitlab.com/easycrypt/sha3. The README.md file contains further points to be relevant checking extraction and compilation tools and gives light instructions on how to use them to check the proofs and compile the code.

<figure><img src="image_81.png" /></figure>

**Remark**

My personal contribution is situated in the provable security level. It involves the in-differentiability proof and the proof that indifferentiability implies collision-resistance and resistance against first- and second-preimage attacks.

This manuscript will stop describing the Jasmin implementation, but anyone interested in this part are welcomed to read the original paper [Almeida et al., 2019b].

In section 6.1, I describe the SPONGE construction and the SHA3 functions. Then, in section 6.2 I present the security statement for which I explain in section 6.3 the structure of the security proof by introducing a general approach to the decomposition of indifferentiability games. In section 6.3.2, section 6.3.3 and section 6.3.4, I detail the formalization of the first, second and third layers of the indifferentiability proof.
## 6.1 The SPONGE construction

<figure><img src="image_82.png" /><figcaption>Figure 6.2 – Representation of SPONGE$_c[f, pad, r](m, l)$</figcaption></figure>

<figure><img src="image_83.png" /><figcaption>Figure 6.3 – Pseudocode for the SPONGE construction [?]</figcaption></figure>

The SHA3 standard defines a family of 4 hash functions and 2 extendable-output functions (XOFs). All functions rely on a generic construction, called the SPONGE, that is based on a fixed (unkeyed) permutation. The standard also defines modularly a permutation algorithm — KECCAK-p[1600, 24] — which operates over a 1600-bit-wide state and is defined as an approved usable in other standards. In the following, we use the notation KECCAK-p as shorthand for this permutation.

Representation and pseudocode for the SPONGE construction are respectively shown in Figure 6.2 and 6.3. It is parametrised by: i. the permutation $f$, ii. the padding algorithm pad, and iii. the rate (or block size) $r$. I write $c$ for the construction's capacity, defined as the permutation's bitwidth (1600 in the standard) minus $r$. The construction's internal state $s_a \| s_c$ has two parts: $s_a$ (r bits) and $s_c$ (c bits). On input of a bitstring $m$, the SPONGE