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