📝 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.