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