# ❓ Motivation

## What is CryptoVerif?

CryptoVerif
is a tool for proving cryptographic protocols in the computational model. It formalizes the
“sequence of games”
proving technique (often also called “game hopping”). CryptoVerif computes a bound on the advantage of an adversary. Input files are written in a specialized probabilistic process calculus language inspired by the applied
pi-calculus.

CryptoVerif has an automatic mode, as well as an interactive mode.

## Why you should learn about it

CryptoVerif can be used to prove secrecy, authentication, and indistinguishability properties of cryptographic protocols. You can use it, for example, to verify your handwritten proof, and check for any human-made mistakes.

Note that CryptoVerif cannot find attacks, **but** the output of a failed proof may help you to derive a concrete attack on a protocol you may even have considered to be secure before.

### Author

This tutorial was made by Marc Hafner as a Master's project at the Chair for Network and Data Security, Ruhr-University Bochum.

Advisors: Benjamin Lipp, Marcus Brinkmann

Special thanks to Benjamin for his support, helping me understand CryptoVerif better after each meeting.

# 🔧 Installation

ℹ️ This tutorial only shows how to install CryptoVerif and its requirements on

Ubuntu.

It is also possible to run CryptoVerif under other Linux distributions, MacOS, and Windows.

For more information, take a look at theREADMEfile in the downloaded CryptoVerif folder.

## Download CryptoVerif

CryptoVerif can be downloaded here.

- Click on the “Source” download link,
- Scroll to the very bottom of the page and accept the terms,
- Accept again in the popup window,
- Download
*cryptoverif2.06.tar.gz*to a location of your choosing.

## Install OCaml (4.03 or higher)

CryptoVerif requires OCaml version 4.03 or higher to be installed. The easiest way to install OCaml is to use its package manager opam. The following three commands are meant to be executed as root, or with `sudo`

(source):

```
add-apt-repository ppa:avsm/ppa
apt update
apt install opam
```

For CryptoVerif to work, it is important to install the OCaml compiler as well. This is taken care of by the following two commands, execute them as normal user (source).
After the execution of the first command, you may be asked if you want to modify the file `~/.profile`

. You can answer with the default "N".
When asked if you want to add a hook, you can answer with the default "y".

```
opam init
eval $(opam env)
```

Check if the installation was successful with the following command.

```
ocaml -version
```

## Install CryptoVerif

First, you need to decompress the previously downloaded *cryptoverif2.06.tar.gz*.

```
tar -xzf cryptoverif.2.06.tar.gz
```

Build the programs using the following commands.

```
cd cryptoverif2.06
./build
```

Further, CryptoVerif requires the OCaml cryptographic library *cryptokit* to be installed.

```
opam install cryptokit
```

## Test for successful installation

Let’s try to run CryptoVerif on an example protocol. You need to be in the directory *cryptoverif2.06* where the executable *cryptoverif* is located, before executing the following command.

```
./cryptoverif examples/basic/pfdh.cv
```

The end of the result should look like this:

ℹ️ Having problems with the installation? Take a look at the

READMEfile in the downloaded CryptoVerif folder.

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

# 💡 Challenges

## Enc-and-MAC

In the first challenge, we will consider the
Enc-and-MAC
construction. The assumptions on the cryptographic primitives are the same as in the chapter **First Proof**: The symmetric encryption is IND-CPA-secure and the MAC is SUF-CMA-secure.

**Try** to prove that Enc-and-MAC is IND-CPA-secure using CryptoVerif. As you may already know, that **cannot be proven** as attacks exist.

In this challenge, you should inspect CryptoVerif’s output and understand why the sequence of games failed.

Note that CryptoVerif **cannot find attacks**. However, you should use CryptoVerif’s output to derive a concrete attack on the Enc-and-MAC construction.

The Enc-and-MAC construction works as follows.

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

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

**❓ Don’t know how to proceed? Click here.**

The input file is almost the same as

enc-then-MAC-IND-CPA.ocvdiscussed in the chapterFirst Proof.

For this task, you need torewrite the definitionoffull_encto match Enc-and-MAC instead of Enc-then-MAC.

**Show solution**

Solution: Definition Enc-and-MACTo rewrite the definition of the Enc-then-MAC encryption to the Enc-and-MAC encryption, you need to change what the MAC will be computed over. For Enc-and-MAC, we compute the MAC over the plaintext

m.

Explanation: How the proof failsIn the IND-CPA proof for Enc-then-MAC presented in the chapter

First Proof, we saw that CryptoVerif was able to merge the branches depending on the value ofb. This was possible as the expressions were semantically the same in both branches.

For the Enc-and-MAC construction, this is not possible. When you have a look at the highlighted parts in the CryptoVerif output below, you will see that in the upper branch, the MAC is computed over the plaintextm1and in the lower branch over the plaintextm2. This prevents merging those branches. At this point, CryptoVerif does not find another way to prove the secrecy ofb.## Now we want to use the output of the failed CryptoVerif proof to derive an attack against the Enc-and-MAC construction. As shown before, the proof failed because the branches of the if statement could not be merged. This was because the MACs were computed over the different plaintexts m1 and m2. When we try to derive an attack against the Enc-and-MAC construction, we will start at this part.

Solution: Derive attack on Enc-and-MACOur goal is to show that the Enc-and-MAC construction is not necessarily IND-CPA-secure when the encryption scheme is assumed to be IND-CPA-secure and the MAC is considered SUF-CMA-secure. We know that the fact that the MAC is computed over the plaintext instead of the ciphertext is probably connected to the reason why the proof fails.

As we want to derive an attack against the IND-CPA security, we aim for revealing any information about the plaintext. The most simple way of doing so is by revealing the whole plaintext. Combine this with the fact that SUF-CMA security of a MAC does not make any statements about confidentiality. You can define a MAC namedMACusing a SUF-CMA secure MAC namedMAC'as follows.It is easy to prove that the newly constructed MAC is still SUF-CMA-secure. For further information, you can have a look at Krawczyk's work (Chapter 4). Instantiating the Enc-and-MAC construction with the newly constructed MAC, it is quite obvious that it cannot be IND-CPA-secure. The message encrypted is always appended to the MAC and is directly revealed in the Enc-and-MAC ciphertext. This way, the adversary can say which plaintext has been encrypted with probability 1.

💡 Feel free to experiment with CryptoVerif if you want to. For example, you can use CryptoVerif to prove that the newly constructed MAC revealing the message is still SUF-CMA-secure.

## Enc-then-MAC IND-CCA2

In the second challenge, we will consider the
Enc-then-MAC
construction again. The assumptions on the cryptographic primitives are the same as in the chapter **First Proof**: The symmetric encryption is IND-CPA-secure and the MAC is SUF-CMA-secure.

Your goal is to prove that Enc-then-MAC is then
IND-CCA2-secure using CryptoVerif.

You can orientate yourself on the input file
*enc-then-MAC-IND-CPA.ocv*
presented in the chapter **First Proof**. You may require to have a look at hints 4 and 5 as they contain CryptoVerif syntax not captured in this tutorial beforehand.

**❓ Need any hints? Click here.**

💡 Hint 1Consider the

differencesbetween theIND-CPAgame and theIND-CCA2game. What is new?

💡 Hint 2The IND-CCA2 game requires a decryption oracle.

Did you tell CryptoVerif how theEnc-then-MAC decryptionlooks like?

Solution: Decryption Enc-then-MAC

💡 Hint 3The IND-CCA2 game requires a decryption oracle.

Did you add thedecryption oracle? You can orientate yourself on the encryption oracle presented in the chapterFirst Proof.

Note that you should not implement the decryption oracle as a left-or-right oracle.

💡 Hint 4Did you remember to

excludehow any adversary cantrivially winthe IND-CCA2 game?

You may use tables in CryptoVerif to do so. Check the syntax of tables in CryptoVerif below.

CryptoVerif Syntax: Tables

💡 Hint 5In the IND-CCA2 game, the adversary can access the encryption oracle and the decryption oracle. The adversary can choose the order he makes requests to the oracles, but in CryptoVerif only one oracle can be called at a time.

Check the syntax of parallel composition of oracles in CryptoVerif below.

CryptoVerif Syntax: Parallel composition of oracles

**Show solution**

Solution: Decryption Enc-then-MACThe Enc-then-MAC decryption function

full_dechas three parameters. It requires the ciphertextcof typebitstring, the encryption keykof typekey, and the MAC keymkof typemkey.

First, it separates the ciphertextcof the Enc-then-MAC encryption back into the actual encryption ciphertextc1and the MACmac1. If the ciphertextcwas of incorrect format and therefore could not be split intoc1andmac1, the function returns bottom.

Then, it is checked whether the MACmac1is valid. This is done by calling the verification functionverify, providing the ciphertextc1, the MAC keymk, and the MACmac1as parameters. If the verification succeeds, the decryption of the ciphertextc1under the decryption key (same as the encryption key)kis returned. If the verification fails, the function returns bottom.

Solution: Enc and Dec oracle (exclude trivial win)The encryption oracle

QencLRis almost the same as in the IND-CPA proof presented in the chapterFirst Proof. As we need to give an adversary access to a decryption oracle, we require preventing that an adversary can win the IND-CCA2 game trivially. That is, excluding that an adversary can send a ciphertext produced by the encryption oracle directly to the decryption oracle.

We do this by keeping track of the returned ciphertexts in a table. First, we create a table calledciphertexts, which can contain elements of the typebitstring. Inside the oracleOencwe will insert the generated ciphertextc0into the table.The decryption oracle

Qdechas two parameters. It requires the encryption keykof typekeyand the MAC keymkof typemkey. Similar to the encryption oracle, we use oracle replication for the decryption oracle as well. The oracleOdectakes a ciphertextcas input. Note that the decryption oracle is not a left-or-right oracle, so we do not have inputs likec1andc2. We check whether the ciphertextc, queried by the adversary, is inside the tableciphertextsand has therefore been returned by the encryption oracle earlier. If this is the case, the function returns bottom. Otherwise, the Enc-then-MAC decryption is returned.The parameters

qEncandqDecused for the oracle replication are declared at the top of the input file.

Solution: Initial GameThe initial game is almost the same as the initial game for the IND-CPA game presented in the chapter

First Proof. The only difference is that the adversary has access to a decryption oracle additionally. We achieve this by running both oracles in parallel composition (check Hint 5).

Take a look at the last game and convince yourself that the secrecy of *b* can be proven in Game 14.

**Show last game**

# 📝 Self-Study

In this chapter, you are welcome to have a look at how CryptoVerif proves the authenticated key exchange protocol *signed Diffie-Hellman* secure in a multi-user, multi-session environment.

We will not have an in-depth look at every line of the input file as in the chapter **First Proof**. You will recognize many similar structures. We will have a look at some code snippets, discussing the most important differences.

One interesting aspect, for example, is how CryptoVerif excludes *malicious accepts*.

Further, in this proof, you can see how CryptoVerif can be guided through the proof (interactive mode).

You can find the input file *signedDH.ocv*
here.

## Secrecy of session key

The queries to prove secrecy of the session key *keyA* and *keyB* have the same syntax as we have seen before to prove the secrecy of bit *b*.

The difference here is that the values of *keyA* and *keyB* depend on the messages the communicating parties have sent each other (key agreement).

We only want to prove secrecy in case the two honest parties *A* and *B* interacted. There is a problem where another party besides *B* can communicate with party *A* and trivially know the agreed key. Because of this, you can see a little trick in the following code snippet. The value of the agreed key is stored in *kA* at first. Only if the other party is *B* then the value of *keyA* is set to *kA*. Otherwise, *kA* will be directly leaked.

## Events

In CryptoVerif we can also use events. You can see the declaration of the events *endA*, *beginB*, and *endB* in the following. They also have parameters of the given types associated to them.

In the following, you can see in the highlighted part how it looks when an event is recorded. In this example, this is the event *endA*. We will use these events later on to prove that a *malicious accept* is not possible.

From the code depicted above, you can also understand that the messages of a protocol exchanged between the communicating parties are defined as oracles in CryptoVerif.

## Exclude malicious accept

Now we want CryptoVerif to prove that a *malicious accept* is not possible. For this we write queries using the events *endA*, *beginB*, and *endB* shown in the previous section.

In the upper query we want to prove that for each event *endA* there exists one distinct event *beginB* with the same parameters. This should be proven even if the shared secrets *keyA* and *keyB* are leaked. We indicate this using the keyword **public_vars**.

To be more precise, when this query is proven it means that party *A* can authenticate party *B*, even if any shared secrets leaks.

The lower query is the other way around. We want to show that *B* can authenticate *A*, even if any shared secret is leaked. For each event *endB* there exists one distinct event *endA* with the same parameters.

## Interactive mode

It is possible to run CryptoVerif in interactive mode. This might be necessary for complex protocols. In the interactive mode, you can guide CryptoVerif through the proof. In this section, we will have a look at how to use the interactive mode.

We need to add a *proof* environment to the input file as depicted above. With the keyword **out_game** we can specify a filename and save the current game inside. To make the proof interactive, we use the keyword **interactive**. Note that this way CryptoVerif will ask in the console for the next command instead of continuing with the rest of the *proof* environment. If you delete the **interactive** keyword, CryptoVerif would follow this given proof structure. You can take this part which is ignored to know what commands you should type in the console in CryptoVerif's interactive mode.

You can apply a cryptographic assumption on a function using a command like **crypto assumption(function)**. This will apply the defined equivalence (compare *ind_cpa(enc)* in the chapter **First Proof**). In our example, we will apply the ROM assumption on the hashfunction *hash* first. The second cryptographic assumption we apply is the UF-CMA assumption on the signature function *sign*. The protocol uses this signature function multiple times, and therefore we also want to apply the assumption multiple times. We need to indicate this by adding a star at the end of the command.

In interactive mode, you can type the command **success** at any time and CryptoVerif will try to prove the queries. When you type the command **success** after applying the two assumptions mentioned before, you can see that the queries for excluding *malicious accepts* can already be proven at this point. The remaining queries for the secrecy of *keyA* and *keyB* remain unproven. Use the command **simplify** to simplify the current game. At this point, this would remove the events from the current game as they are no longer needed.

Next, apply the CDH assumption on the function *exp*. After this you can use the command **success** again, and you will see that now all queries have been proven.

During interactive mode, the command **quit** can be used to leave interactive mode. Then, CryptoVerif continues with the next commands in the proof environment.

ℹ️ Note that CryptoVerif is also able to prove the Signed DH protocol in automatic mode.