# π First Proof

In this chapter, we will have a look at a first proof using CryptoVerif. You will be guided to gather an understanding of how to work with CryptoVerif.

We will consider the Enc-then-MAC construction. Our goal is to show that Enc-then-MAC is IND-CPA-secure, assuming the symmetric encryption is IND-CPA-secure and the MAC is SUF-CMA-secure.

## Enc-then-MAC

The Enc-then-MAC construction works as follows.

- Encrypt the plaintext, resulting in a ciphertext.
- Compute the MAC over this ciphertext.
- Concatenate the ciphertext and this MAC.

You can see a visualization of this construction on the right-hand side.

## Input file

In this section, we will build the input file for the proof together. CryptoVerif takes this file and tries to prove the queries we defined using the sequence of games technique.

βΉοΈ Note that we will not strictly walk through every line of code from top to bottom. We will skip some lines for didactic reasons and explain them at the appropriate places.

### Cryptographic assumptions

We start with the cryptographic assumptions we make for the cryptographic primitives used. In our case, this is that the symmetric encryption is IND-CPA-secure and the MAC is SUF-CMA-secure.

CryptoVerif provides a library containing many cryptographic assumptions you can use (see *docs/manual.pdf*, Chapter 6). It is also possible to create your own assumptions.

You can see the code snippets for telling CryptoVerif that *enc* is IND-CPA-secure and *mac* is SUF-CMA-secure in the following.

The macros *IND_CPA_sym_enc* and *SUF_CMA_det_mac* defined in default library *default.ocvl* are expanded. For a better understanding, we will discuss the technical side with the example of the *IND_CPA_sym_enc* macro.

First, let us inspect the meaning of the parameters of this macro:

- type of keys,
- type of plaintexts,
- type of ciphertexts,
- encryption function,
- decryption function,
- function to inject the type bitstring into the type bitstringbot. The decryption returns either a bitstring (plaintext) or bottom (when the decryption fails). The type bitstringbot contains all bitstrings and bottom. bitstringbot is the return type of the decryption function.
- function from bitstring to bitstring, modeling the leakage of the encryption. We usually interpret this as the leakage of the length of the plaintext.
- probability of breaking the IND-CPA property

The functions *enc*, *dec*, *injbot* and *Z* are declared by the macro. It is important that they are not declared anywhere else. They can only be used after the macro has been expanded.

The types of keys, plaintexts, ciphertexts, and the probability *Penc* must be declared before expanding the macro.

As you can see in the code snippet, the probability *Penc* is declared right before expanding the macro.

The types of plaintexts and ciphertexts are *bitstring*, a predefined type.

The type of keys is declared at the top of the input file, depicted in the following code snippet. There are also the type declarations for parameters for the macro *SUF_CMA_det_mac*.

The types are annotated with the label **[fixed]** meaning that, for example, an encryption key is a bitstring of fixed length. Note that CryptoVerif does not need to know the specific length. Similar as it does not need to know the specific implementation of the symmetric encryption scheme or the MAC.

Note that it is possible to make an exact specification of the length to CryptoVerif.

Now we want to gain a better understanding of how CryptoVerif is doing game transformations. Once again, we will take the IND-CPA assumption as an example.

Letβs have a look at a code snippet from the macro *IND_CPA_sym_enc* in the default library *default.ocvl* depicted below.

This equivalence defines how the IND-CPA game hop looks like. CryptoVerif will look for code segments matching with the upper block (lines 136-138) and will replace them with the lower block (lines 140-142) to perform this game hop. If it does so, the probability stated in line 139 will be added to the bound of the adversary advantage.

Letβs compare the upper block (lines 136-138) with the lower block (lines 140-142) to see why this equivalence is suitable for the IND-CPA assumption.

We start with a uniformly random sampled encryption key *k* (line 136+140). The lines 137-138 and lines 141-142 are representing the encryption oracle using replication of the oracle *Oenc*. Oracles are defined by the usage of ":=".

βΉοΈ Replication of oracles are used to indicate that an oracle can be executed multiple times. In the code snippet above, the oracle

Oencis replicatedNtimes. The variableNis no concrete value, but a parameter that will appear as such in the adversary advantage.

Both oracles *Oenc* take a cleartext *x* as input, but they differ in their output.

In the upper block, the oracle returns the encryption of the cleartext *x* under the key *k* and the encryption seed *r* (line 138). This matches a regular encryption of cleartexts.

In the lower block, the oracle does not encrypt the cleartext *x* but the leakage of the encryption *Z(x)* (line 142). For simplicity, we will interpret the leakage of the encryption as the leakage of the lenght of the cleartext. We assume that *Z(x)* will return a bitstring with the same lenght as *x* consisting only of zeros.

This transformation matches the IND-CPA assumption quite well, as the ciphertexts cannot be used to gather any additional information about the cleartexts.

βοΈ It is important that the requirements stated by this equivalence are strictly matched to perform this transformation.

If we assume that inside a game the encryption seedris chosen randomly outside the replication and is reused for each encryption, then CryptoVerif is not allowed to perform this transformation, as the requirements including the correct distribution for each variable are not matched.

### Definition Enc-then-MAC

Further, we need to define how Enc-then-MAC works.

For the definition of the Enc-then-MAC construction, we will need a function for concatenation. We are not interested in the concrete implementation of this function.

Therefore, we only declare the function using the keyword **fun**.

The keyword **letfun** is used when defining a function, i.e., giving a concrete implementation. We will use this one for the definition of the Enc-then-MAC encryption.

The declaration of the concatenation function is shown in the following.

The function *concat* takes parameters of type *bitstring* and *macs*, and returns a variable of type *bitstring*. The annotation **[data]** indicates that this function is injective and its inverse can be computed efficiently.

Now that we talked about the concatenation function, we have everything we need to move on to the Enc-then-MAC construction. The definition of the Enc-then-MAC encryption is depicted in the following.

As we want to define the exact behaviour for the Enc-then-MAC encryption, we use **letfun** for the definition of the function *full_enc*.

The function has three parameters that are needed.

First, there is the plaintext *m* of type *bitstring*. In this model, we consider plain- and ciphertexts as bitstrings. This means we consider cryptographic primitives (e.g., encryption) as mappings from bitstrings to bitstrings.

Further, there are the encryption key *k* of type *key*, and the MAC key *mk* of type *mkey*.

We will use the encryption function *enc* declared inside the macro *IND_CPA_sym_enc* to compute the encryption of the plaintext *m* under the encryption key *k*. This ciphertext is then stored in variable *c1*.

Next, we concatenate the ciphertext *c1* with the MAC of the ciphertext *c1* under the MAC key *mk*. This concatenation is the result of our Enc-then-MAC encryption function *full_enc*.

Note the difference between the usage of β;β and β.β in CryptoVerif.

Sequential execution is denoted by β;β. In the above code snippet, you can see this in the line where *c1* is set to the ciphertext. The semicolon indicates that there is a line of code following, which should be executed afterwards.

The line with the concationation is the last expression belonging to *full_enc*. This block of code is ended with β.β.

### Initial game to prove (including oracles)

Now we want to construct the initial game CryptoVerif should try to prove using the sequence of games. In our example, this is the IND-CPA game. Note that for many games, there are oracles the adversary has access to. Here, an encryption oracle from the IND-CPA game is required. We will start with this oracle before proceeding with the initial game.

The code of the encryption oracle is depicted below.

First, let's talk about the keyword **let** used for this oracle. With this, the subprocess *QencLR* is defined. The code in this subprocess will be inlined inside the main process we will see later on. It is not required to do it this way. You can also put the whole code inside the main process where you need it. Using this approach, you can structure your code for a lot better readability.

The encryption oracle is implemented as a left-or-right oracle. That means that the oracle receives two plaintexts in each query made by the adversary and always encrypts the left plaintext or always encrypts the right plaintext, depending on the value of the secret bit *b0*.

Note the relation between IND-CPA security and LoR-CPA security (cf. [
Bellare et al., Theorem 3]).

The oracle *Oenc* we want to define should be callable by the adversary multiple times. We model this by oracle replication. The oracle can be called *qEnc* times. *qEnc* is just a parameter defined at the top of the input file and is not an actual number. The parameter is put into the bound of the adversary advantage at a corresponding game hop.

The adversary can make calls to the oracle. This models the interaction between the adversary and the game.

The oracle *Oenc* takes two plaintexts *m1* and *m2* as input. As distinguishing ciphertexts of plaintexts with different leakage in the encryption is easy, the oracle should only respond with the ciphertext if the leakage of the received plaintexts is the same.

Remember: Interpreting the leakage of the encryption as the length of the plaintext, this means that *m1* and *m2* should have the same length. This property is also referred to in many definitions of the IND-CPA assumption.

βΉοΈ

If-branches cannot be mergedin CryptoVerif. This means that expressions that should be executed after the conditioned expression have to be put inside the matchBranchandthe noMatchBranch.

The value of *m0* is set to *m1* or *m2*, depending on the bit *b0*. Then, we return the Enc-then-MAC encryption of *m0* under the encryption key *k* and the MAC key *mk*.

As *b0* is fixed for the left-or-right oracle, this means that we always encrypt *m1* or always encrypt *m2*.

In our initial game, we want to prove the secrecy of the bit *b*. We use the query depicted in the following to tell CryptoVerif what should be proven.

The initial game is displayed in the following code snippet.

In CryptoVerif the initial game is the main process. This is indicated by the keyword **process**. There can be only one main process.

Inside this process, we define the oracle *OStart*. Here you will recognize how this oracle represents the initial game, to be more specific, the IND-CPA game.

The bit *b* is sampled as a random boolean value, being either 0 or 1. Further, the keys are sampled randomly from their corresponding keyspaces. The encryption key *k* is uniformly random of type *key*. The MAC key *mk* is uniformly random of type *mkey*.

At this point the initial game is set up, and we want to give control to the adversary. We do this using the keyword **return**. The adversary can now choose which oracle he wants to call.

With the keyword **run**, a subprocess is inlined. Therefore, we inline the previously defined subprocess *QencLR* with the random bit *b*, the random encryption key *k*, and the random MAC key *mk* as parameters. This subprocess contains the encryption oracle that can be called by the adversary against the IND-CPA game.

In the very last line there is no β.β as the file ends here.

## Execute

The input file is now ready, and we can execute CryptoVerif to let it try proof our query.

You can find the input file *enc-then-MAC-IND-CPA.ocv*
here.

When in the same directory as the executable *cryptoverif* you can run CryptoVerif on our created input file using the following command. (The presented input file already exists in the folder *examples/basic*.)

```
./cryptoverif examples/basic/enc-then-MAC-IND-CPA.ocv
```

## Output

Let's have a look at the output of CryptoVerif and see how it proved the Enc-then-MAC construction IND-CPA-secure under the given cryptographic assumptions.

CryptoVerif proves the secrecy of bit *b* in eight games. We will not talk about every game hop. When you take a look at the first game hops, you will see that many game hops are of syntactic nature. Note that the first game is already inlined. Examples for syntactic game hops are expanding if statements or renaming variables.

We will take a closer look at the game hop, where the assumption that the encryption scheme is IND-CPA-secure is used. You can expand the IND-CPA game hop below.

**Show IND-CPA game hop**

In Game 4, the game before the IND-CPA game hop, you can see that besides some syntactic changes not much has changed compared to the initial game. The previous syntactic game hops are necessary to fulfill the requirements to apply the IND-CPA equivalence. We talked about this equivalence in detail in the section **Cryptographic Assumptions**.

Depending on the value of bit *b* either the plaintext *m1* or *m2* is encrypted using the Enc-then-MAC encryption. For this game hop, we will focus only on the part of the Enc-then-MAC construction where the plaintext *m1* or *m2* is encrypted using the encryption scheme *enc*. The plaintexts for this encryption are highlighted in the output of CryptoVerif.

As we told CryptoVerif that the encryption scheme is IND-CPA-secure by expanding the corresponding macro, the defined equivalence can be applied here. As we have previously seen, the plaintext to be encrypted is replaced by the leakage of the encryption of this plaintext. Having a look at the highlighted parts in Game 5, you can see that this equivalence has been applied. Note that the equivalence has been applied twice, once for each branch of the if statement. This equivalence models the IND-CPA assumption.

We will now take a look at the last game hop and understand why the secrecy of bit *b* can be proven in the last game. You can expand the last game hop (Merging game hop) below.

**Show Merging game hop**

In the last game hop, the branches of the if statement depending on the value of bit *b* are merged. This is possible as both branches are semantically equal.

First, in both branches, a seed is sampled uniformly at random. The ciphertexts *c1* are generated using the same encryption function, the same encryption key, and a uniformly random sampled seed. We have to take a look at the plaintexts that are used for the encryption. In the upper branch *Z(m1)* is encrypted, while in the lower branch *Z(m2)* is encrypted. Because of the condition `if Z(m1) = Z(m2) then`

, both values are the same. The return statements are also the same in both branches. Therefore, the branches can be merged.

The bit *b* was only used in the if statement whose branches we merged with the last game hop. Therefore, it has now become trivial that the secrecy of bit *b* can be proven, as it is not used anywhere in the game anymore.

In the following, you can see that CryptoVerif proved the secrecy of bit *b* in game 8. You can also see the bound of the adversary advantage. In the last line, it is stated that all queries have been proven. Therefore, the proof done by CryptoVerif is finished.

Only the games discussed before in detail are affecting the advantage of the adversary. For simplicity, we will use the term "advantage in game X" when describing the "advantage regarding the secrecy of bit *b* in game X".

First, you can see that the advantage in game 1 is bounded by twice the probability defined by the IND-CPA equivalence (*Penc*) plus the advantage in game 8. The factor of two is because the equivalence has been applied twice in the IND-CPA game hop. Second, the advantage in game 8 is bounded by zero as the secrecy of bit *b* in game 8 is trivial as explained before.

These advantages are put together to form the final result advantage.

The advantage depends on some parameters like the length of the plaintexts and the time. CryptoVerif also defines the result time as the time of the relevant operations used.

### TeX output

CryptoVerif also allows writing its output to a TeX file. You can see an example in the following.

```
mkdir tex
./cryptoverif -tex ./tex/enc-then-MAC-IND-CPA examples/basic/enc-then-MAC-IND-CPA.ocv
```

You can view the PDF with a TeX editor of your choice (e.g.
TeXstudio).

Alternatively, you can simply use an
Online LaTeX Editor
to display the PDF without any installation required.