- Otherwise, by Fact 3, there is no configuration in $Tr'$ at a modified program point $\mu_k$, so $Tr$ has a matching trace in $C[G']$ that also satisfies $(\neg\varphi \lor D) \land \neg\text{NonUnique}_{G',D}$. (Note that $Tr$ may still be modified by **success simplify**: the matching trace in $C[G']$ may execute a modified program point $\mu_k$ after $Conf'$, but still the matching trace executes $e(\tilde{M})$, so satisfies $\neg\varphi$, and it does not execute any non-unique event of $G'$.)

We conclude that

$$
\begin{align*}
\mathrm{Adv}_G(C, \varphi, D) &= \Pr[C[G] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G,D}] \\
&\le \Pr[C[G] \le \left( \bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \land \bigwedge \mathcal{F}_k^{\mathrm{mod}} \right) \lor \left( \bigvee \mathcal{L}^+ \right)] \\
&\quad + \Pr[C[G'] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G',D}] \\
&\le p(C) + \mathrm{Adv}_{G'}(C, \varphi, D) \\
&\le p(C) + p'(C) \tag*{since $\mathrm{Bound}_{G'}(V, sp, D, p')$}
\end{align*}
$$

Hence, we have $\mathrm{Bound}_G(V, sp, D, p + p')$.

**Case 3:** $sp$ is 1-ses.secr$(x)$, Secrecy$(x)$, or bit secr$(x)$ with $C = C'[C_{sp}[]]$ and $x$ is defined only by new or by assignments of variables defined by new. Let $C'$ be any evaluation context acceptable for $C_{sp}[G]$ with public variables $V \setminus V_{sp}$ that does not contain $S, \bar{S}$, any event in $D$, nor any non-unique event of $G$.

$$
\begin{align*}
\mathrm{Adv}_G(C, sp, D) &= \Pr[C[G] : S \lor D] - \Pr[C[G] : \bar{S} \lor \mathrm{NonUnique}_{G,D}] \\
&= \Pr[C[G] : S] + \Pr[C[G] : D] - \Pr[C[G] : \bar{S}] - \Pr[C[G] : \mathrm{NonUnique}_{G,D}] \\
&\qquad \text{since these events are mutually exclusive} \\
&= \Pr[C[G] : S \land \neg sp] + \Pr[C[G] : D] \\
&\quad - \Pr[C[G] : \bar{S} \land \neg sp] - \Pr[C[G] : \mathrm{NonUnique}_{G,D}] \qquad \text{by Lemma 35} \\
&= \Pr[C[G] : (S \land \neg sp) \lor D] - \Pr[C[G] : \bar{S} \land \neg sp] - \Pr[C[G] : \mathrm{NonUnique}_{G,D}]
\end{align*}
$$

We have

* $\Pr[C[G'] : \mathrm{NonUnique}_{G',D}] \le \Pr[C[G] : \mathrm{NonUnique}_{G,D}]$,

* $\Pr[C[G'] : \bar{S} \land \neg sp] \le \Pr[C[G] : \bar{S} \land \neg sp]$

since a trace that executes a non-unique event or $\bar{S}$ in $G'$ cannot execute event adv loses, so it executed without change in $G$. Let us show that $\Pr[C[G] : (S \land \neg sp) \lor D] \le p(C) + \Pr[C[G'] : (S \land \neg sp) \lor D]$. Let $Tr$ be a full trace of $C[G]$ such that $Tr \vdash (S \land \neg sp) \lor D$. Let us show that $Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

Case 3.1: $Tr$ executes a non-unique event of $G$. Then $Tr \vdash e$ for some non-unique event $e$ in $G$ and in $D$. We conclude by Fact 2.

Case 3.2: $Tr \vdash e$ for some Shoup event $e$ in $D$. Then $Tr$ does not execute any non-unique event of $G$. We conclude by Fact 1 for the correspondence $\mathrm{event}(e) \Rightarrow$ false.

Case 3.3: $Tr \vdash S \land \neg sp$. Since $Tr \vdash \neg sp$, we have $Tr \vdash \neg\{\mathrm{prove}^{sp}(\mathrm{Tpp}(Tr))\}$, so we are in one of the following two cases:
* There exists $\mu \in \text{Tpp}(\text{Tr})$ such that $\text{Tr} \vdash \neg\{[\text{prove}^{\text{1-ses.secr.}}(x)(\mu)]\}$.

- If $\mu \in S_1$, then $\text{Tr} \vdash \bigvee \mathcal{L}^+$ since $\neg\{[\text{prove}^{\text{1-ses.secr.}}(x)(S_1)]\}$ is added to $\mathcal{L}^+$.

- If $\mu \in S_0 \setminus S_1$, then $(\theta I_\mu, \theta \mathcal{F}_\mu)$ is added to $\mathcal{L}^-$, where $\theta$ is a renaming of $I_\mu$ to fresh replication indices. Moreover, we have $\neg\{[\text{noleak}(z[\widetilde{M}'], \mathcal{I}, \mathcal{F})]\} \Rightarrow \exists \mathcal{I}, \wedge \mathcal{F}$, so $\neg\{[\text{prove}^{\text{1-ses.secr.}}(x)(\mu)]\} \Rightarrow \exists \theta I_\mu, \wedge \theta \mathcal{F}_\mu$ since $\text{defRand}_\mu(x)$ is defined. Therefore, $\text{Tr} \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \wedge \mathcal{F}_j$.

* In case $sp = \text{Secrecy}(x)$, there exist $\mu_1, \mu_2 \in \text{Tpp}(\text{Tr})$ such that $\text{Tr} \vdash \neg\{[\text{prove}^{\text{distinct}}(x)(\mu_1, \mu_2)]\}$. Let $z_1[\widetilde{M}_1] = \text{defRand}_{\mu_1}(x)$, $z_2[\widetilde{M}_2] = \text{defRand}_{\mu_2}(x)$, $\tilde{i}$ be the current replication indices at the definition of $x$, $\theta_1$ and $\theta_2$ be two distinct renamings of $\tilde{i}$ to fresh replication indices, $\tilde{i}_1 = \theta_1 \tilde{i}$, $\tilde{i}_2 = \theta_2 \tilde{i}$, and $\mathcal{F} = \theta_1 \mathcal{F}_{\mu_1} \cup \theta_2 \mathcal{F}_{\mu_2} \cup \{\theta_1 \widetilde{M}_1 = \theta_2 \widetilde{M}_2, \tilde{i}_1 \neq \tilde{i}_2\}$ Then $z_1 = z_2$ and $\text{Tr} \vdash \exists \tilde{i}_1, \exists \tilde{i}_2, \wedge \mathcal{F}$.

- If $\mathcal{F}$ yields a contradiction, then $\exists \tilde{i}_1, \exists \tilde{i}_2, \wedge \mathcal{F}$ is added to $\mathcal{L}^+$, so $\text{Tr} \vdash \bigvee \mathcal{L}^+$.

- Otherwise, $(\tilde{i}_1 \cup \tilde{i}_2, \mathcal{F})$ is added to $\mathcal{L}^-$, so $\text{Tr} \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \wedge \mathcal{F}_j$.

If $\text{Tr} \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \wedge \mathcal{F}_k^{\text{mod}}$, then $\text{Tr} \vdash (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \wedge \mathcal{F}_j \wedge \wedge \mathcal{F}_k^{\text{mod}}) \vee (\bigvee \mathcal{L}^+)$.

Otherwise, by Fact 3, there is no configuration in $\text{Tr}$ at a modified program point $\mu_k$, so $\text{Tr}$ has a matching trace in $C[G']$ that also satisfies $(S \wedge \neg sp) \vee D$.

Therefore, $\text{Pr}[C[G] : (S \wedge \neg sp) \vee D] \leq p(C) + \text{Pr}[C[G'] : (S \wedge \neg sp) \vee D]$, so

$$ \text{Adv}_G(C, sp, D) \leq p(C) + \text{Pr}[C[G'] : (S \wedge \neg sp) \vee D] - \text{Pr}[C[G'] : \bar{S} \wedge \neg sp] - \text{Pr}[C[G'] : \text{NonUnique}_{G',D}] $$

Moreover, by applying on $G'$ the same steps as on $G$ at the beginning of this proof, we have

$$ \text{Adv}_{G'}(C, sp, D) = \text{Pr}[C[G'] : (S \wedge \neg sp) \vee D] - \text{Pr}[C[G'] : \bar{S} \wedge \neg sp] - \text{Pr}[C[G'] : \text{NonUnique}_{G',D}] $$

so

$$ \text{Adv}_G(C, sp, D) \leq p(C) + \text{Adv}_{G'}(C, sp, D) \leq p(C) + p'(C) $$

since $\text{Bound}_{G'}(V, sp, D, p')$. Therefore, we have $\text{Bound}_G(V, sp, D, p + p')$. $\square$

## 5.2 crypto: Applying the Security Assumptions on Primitives

The crypto transformation applies security assumptions on primitives. The first version of this transformation was presented in [24, Section 3.2 and Appendix D].

# 6 Proof Strategy

The first version of the automatic proof strategy was presented in [24, Section 5].

# 7 Conclusion

The tool CryptoVerif produces proofs by sequences of games like those manually written by cryptographers. It generates the games, using an automatic proof strategy or guidance from the user, who specifies the transformations to perform. It supports a wide variety of cryptographic primitives specified by indistinguishability axioms. Many of these primitives are included in a library so that the user does not have to redefine them. It can prove secrecy, correspondence,
and indistinguishability properties. It has been applied to substantial case studies, including
Signal [47], TLS 1.3 [21], and WireGuard [53].

CryptoVerif still has limitations. In particular, the size of games tends to grow too fast, which
limits its ability to deal with large examples, especially because some game transformations
require the game to be expanded first by the **expand** transformation, which duplicates the code
from each test until the end of protocol. Planed improvements include allowing more game
transformations to work without previous application of **expand**; allowing internal oracle calls
in games, in order to share code between different parts of the game; using composition results in
order to make proofs more modular. Moreover, some game transformations could be generalized.
For instance, the transformation **merge branches merges branches of a test when they execute
the same code; the detection that several branches execute equivalent code could be made more
flexible, by allowing reorderings of instructions for instance. CryptoVerif only considers blackbox
adversaries: it does not support proofs that manipulate the code of the adversary, such as the
forking lemma [60].

**Acknowledgments** I warmly thank David Pointcheval for his advice and explanations of the computational proofs of protocols. This project would not have been possible without him. I also thank Jacques Stern for initiating this work and Charlie Jacomme for helpful discussions on this document. The design and implementation of CryptoVerif was partly done while I was at CNRS and at Ecole Normale Supérieure. This work was partly supported by the French National Research Agency (ANR) under the projects FormaCrypt (ARA SSIA 2005), ProSe (VERSO 2010, decision number 2010-VERS-004), TECAP (decision number ANR-17-CE39-0004-03) and received funding from the France 2030 program managed by the ANR under the reference ANR-22-PECY-0006 (PEPR Cybersecurity SVP).

References

[1] M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). *Journal of Cryptology*, 15(2):103–127, 2002.

[2] M. Abdalla, P.-A. Fouque, and D. Pointcheval. Password-based authenticated key exchange in the three-party setting. *IEE Proceedings Information Security*, 153(1):27–39, Mar. 2006.

[3] R. Affeldt, D. Nowak, and K. Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. In *9th International Workshop on Automated Verification of Critical Systems (AVoCS'09)*, volume 23 of *Electronic Communications of the EASST*. EASST, Sept. 2009.

[4] J. B. Almeida, M. Barbosa, G. Barthe, M. Campagna, E. Cohen, B. Grégoire, V. Pereira, B. Portela, P.-Y. Strub, and S. Tasiran. A machine-checked proof of security for AWS key management service. In *ACM SIGSAC Conference on Computer and Communications Security (CCS'19)*, pages 63–78, New York, NY, Nov. 2019. ACM Press.

[5] M. Backes, D. Hofheinz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In *ACM Conference on Computer and Communications Security (CCS'09)*, pages 66–78, New York, NY, Nov. 2009. ACM Press.

[6] M. Backes and P. Laud. Computationally sound secrecy proofs by mechanized flow analysis. In *13th ACM Conference on Computer and Communications Security (CCS'06)*, pages 370–379, New York, NY, Nov. 2006. ACM Press.
[7] M. Backes and B. Pfitzmann. Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In *17th IEEE Computer Security Foundations Workshop*, pages 204–218, Los Alamitos, CA, June 2004. IEEE Computer Society Press.

[8] M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In *10th ACM conference on Computer and communication security (CCS'03)*, pages 220–230, New York, NY, Oct. 2003. ACM Press.

[9] D. Baelde, S. Delaune, A. Koutsos, C. Jacomme, and S. Moreau. An interactive prover for protocol verification in the computational model. In *42nd IEEE Symposium on Security and Privacy (S&P'21)*, pages 537–554, Los Alamitos, CA, May 2021. IEEE Computer Society Press.

[10] G. Barthe, J. M. Crespo, Y. Lakhnech, and B. Schmidt. Mind the gap: Modular machine-checked proofs of one-round key exchange protocols. In E. Oswald and M. Fischlin, editors, *Advances in Cryptology - EUROCRYPT 2015*, volume 9057 of *Lecture Notes in Computer Science*, pages 689–718, Berlin, Heidelberg, Apr. 2015. Springer.

[11] G. Barthe, M. Daubignard, B. Kapron, and Y. Lakhnech. Computational indistinguishability logic. In *17th ACM Conference on Computer and Communications Security (CCS'10)*, pages 375–386, New York, NY, Oct. 2010. ACM Press.

[12] G. Barthe, B. Grégoire, S. Z. Béguelin, and Y. Lakhnech. Beyond provable security. Verifiable IND-CCA security of OAEP. In A. Kiayias, editor, *Topics in Cryptology - CT-RSA 2011*, volume 6558 of *Lecture Notes in Computer Science*, pages 180–196, Berlin, Heidelberg, Feb. 2011. Springer.

[13] G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin. Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt. In P. Degano, J. Guttman, and F. Martinelli, editors, *5th International Workshop on Formal Aspects in Security and Trust, FAST 2008*, volume 5491 of *Lecture Notes in Computer Science*, pages 1–19, Berlin, Heidelberg, 2009. Springer.

[14] G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin. Computer-aided security proofs for the working cryptographer. In P. Rogaway, editor, *Advances in Cryptology - CRYPTO 2011*, volume 6841 of *Lecture Notes in Computer Science*, pages 71–90, Berlin, Heidelberg, Aug. 2011. Springer.

[15] G. Barthe, B. Grégoire, and S. Zanella. Formal certification of code-based cryptographic proofs. In *36th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'09)*, pages 90–101, New York, NY, Jan. 2009. ACM Press.

[16] D. Basin, A. Lochbihler, and S. R. Sefidgar. CryptHOL: Game-based proofs in higher-order logic. *Journal of Cryptology*, 33:494–566, 2020.

[17] S. Z. Béguelin, G. Barthe, S. Heraud, B. Grégoire, and D. Hedin. A machine-checked formalization of sigma-protocols. In *23rd Computer Security Foundations Symposium (CSF'10)*, pages 246–260, Los Alamitos, CA, July 2010. IEEE Computer Society Press.

[18] S. Z. Béguelin, B. Grégoire, G. Barthe, and F. Olmedo. Formally certifying the security of digital signature schemes. In *30th IEEE Symposium on Security and Privacy, S&P 2009*, pages 237–250, Los Alamitos, CA, May 2009. IEEE Computer Society Press.
[19] M. Bellare and C. Namprempre. Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In T. Okamoto, editor, *Advances in Cryptology – ASIACRYPT’00*, volume 1976 of Lecture Notes in Computer Science, pages 531–545, Berlin, Heidelberg, Dec. 2000. Springer.

[20] M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. In S. Vaudenay, editor, *Advances in Cryptology – Eurocrypt 2006 Proceedings*, volume 4004 of Lecture Notes in Computer Science, pages 409–426, Berlin, Heidelberg, May 2006. Springer. Extended version available at http://eprint.iacr.org/2004/331.

[21] K. Bhargavan, B. Blanchet, and N. Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. In *IEEE Symposium on Security and Privacy (S&P’17)*, pages 483–503, Los Alamitos, CA, May 2017. IEEE Computer Society Press.

[22] B. Blanchet. Automatic proof of strong secrecy for security protocols. In *IEEE Symposium on Security and Privacy*, pages 86–100, May 2004.

[23] B. Blanchet. Computationally sound mechanized proofs of correspondence assertions. In *20th IEEE Computer Security Foundations Symposium (CSF’07)*, pages 97–111, Los Alamitos, CA, July 2007. IEEE Computer Society Press. Extended version available as ePrint Report 2007/128, http://eprint.iacr.org/2007/128.

[24] B. Blanchet. A computationally sound mechanized prover for security protocols. *IEEE Transactions on Dependable and Secure Computing*, 5(4):193–207, Oct.–Dec. 2008.

[25] B. Blanchet. Automatically verified mechanized proof of one-encryption key exchange. Cryptology ePrint Archive, Report 2012/173, Apr. 2012. Available at http://eprint.iacr.org/2012/173.

[26] B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. *Journal of Logic and Algebraic Programming*, 75(1):3–51, Feb.–Mar. 2008.

[27] I. Boureanu, C. C. Drăgan, F. Dupressoir, D. Gérault, and P. Lafourcade. Mechanised models and proofs for distance-bounding. In *34th IEEE Computer Security Foundations Symposium (CSF’21)*, Los Alamitos, CA, 2021. IEEE Computer Society Press.

[28] D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In *7th International Conference on Availability, Reliability and Security (ARES 2012)*, pages 65–74, Los Alamitos, CA, Aug. 2012. IEEE Computer Society Press.

[29] D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations and application to SSH. *Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)*, 4(1):4–31, Mar. 2013.

[30] R. Canetti. Universally composable security: A new paradigm for cryptographic protocols. In *42nd Symposium on Foundations of Computer Science (FOCS)*, pages 136–145, Los Alamitos, CA, Oct. 2001. IEEE Computer Society Press. An updated version is available at Cryptology ePrint Archive, http://eprint.iacr.org/2000/067.

[31] R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Linch, O. Pereira, and R. Segala. Time-bounded task-PIOAs: A framework for analyzing security protocols. In S. Dolev, editor, *20th Symposium on Distributed Computing (DISC)*, volume 4167 of Lecture Notes in Computer Science, pages 238–253, Berlin, Heidelberg, Sept. 2006. Springer.
[32] R. Canetti and J. Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004/334, 2004. Available at http://eprint.iacr.org/2004/334.

[33] H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. In *15th ACM conference on Computer and communications security (CCS'08)*, pages 109–118, New York, NY, Oct. 2008. ACM Press.

[34] V. Cortier, C. C. Drăgan, F. Dupressoir, B. Schmidt, P.-Y. Strub, and B. Warinschi. Machine-checked proofs of privacy for electronic voting protocols. In *IEEE Symposium on Security and Privacy (SP'17)*, pages 993–1008, Los Alamitos, CA, 2017. IEEE Computer Society Press.

[35] V. Cortier, H. Hördegen, and B. Warinschi. Explicit randomness is not necessary when modeling probabilistic encryption. In C. Dima, M. Minea, and F. Tiplea, editors, *Workshop on Information and Computer Security (ICS 2006)*, volume 186 of *Electronic Notes in Theoretical Computer Science*, pages 49–65. Elsevier, Sept. 2006.

[36] V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. *Journal of Automated Reasoning*, 46(3-4):225–259, Apr. 2011.

[37] V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In M. Sagiv, editor, *Proc. 14th European Symposium on Programming (ESOP'05)*, volume 3444 of *Lecture Notes in Computer Science*, pages 157–171, Berlin, Heidelberg, Apr. 2005. Springer.

[38] V. Cortier and B. Warinschi. A composable computational soundness notion. In *18th ACM Conference on Computer and Communications Security (CCS'11)*, pages 63–74, New York, NY, Oct. 2011. ACM Press.

[39] J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech. Towards automated proofs for asymmetric encryption schemes in the random oracle model. In *15th ACM conference on Computer and communications security (CCS'08)*, pages 371–380, New York, NY, Oct. 2008. ACM Press.

[40] J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech. Automated proofs for asymmetric encryption. In D. Dams, U. Hannemann, and M. Steffen, editors, *Concurrency, Compositionality, and Correctness*, volume 5930 of *Lecture Notes in Computer Science*, pages 300–321, Berlin, Heidelberg, 2010. Springer.

[41] J. Courant, C. Ene, and Y. Lakhnech. Computationally sound typing for non-interference: The case of deterministic encryption. In V. Arvind and S. Prasad, editors, *27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07)*, volume 4855 of *Lecture Notes in Computer Science*, pages 364–375, Berlin, Heidelberg, Dec. 2007. Springer.

[42] A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In L. Caires and L. Monteiro, editors, *ICALP 2005: the 32nd International Colloquium on Automata, Languages and Programming*, volume 3580 of *Lecture Notes in Computer Science*, pages 16–29, Berlin, Heidelberg, July 2005. Springer.
[43] A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi. Computationally sound compositional logic for key exchange protocols. In *19th IEEE Computer Security Foundations Workshop (CSFW'06)*, pages 321–334, Los Alamitos, CA, July 2006. IEEE Computer Society Press.

[44] J. Gancher, S. Gibson, P. Singh, S. Dharanikota, and B. Parno. OWL: Compositional verification of security protocols via an information-flow type system. In *2023 IEEE Symposium on Security and Privacy (S&P)*, pages 1114–1131, Los Alamitos, CA, May 2023. IEEE Computer Society Press.

[45] S. Goldwasser, S. Micali, and R. Rivest. A digital signature scheme secure against adaptive chosen-message attacks. *SIAM Journal of Computing*, 17(2):281–308, Apr. 1988.

[46] R. Janvier, Y. Lakhnech, and L. Mazaré. Completing the picture: Soundness of formal encryption in the presence of active adversaries. In M. Sagiv, editor, *Proc. 14th European Symposium on Programming (ESOP'05)*, volume 3444 of *Lecture Notes in Computer Science*, pages 172–185, Berlin, Heidelberg, Apr. 2005. Springer.

[47] N. Kobeissi, K. Bhargavan, and B. Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In *2nd IEEE European Symposium on Security and Privacy (EuroS&P'17)*, pages 435–450, Los Alamitos, CA, Apr. 2017. IEEE Computer Society Press.

[48] P. Laud. Handling encryption in an analysis for secure information flow. In P. Degano, editor, *Programming Languages and Systems, 12th European Symposium on Programming, ESOP'03*, volume 2618 of *Lecture Notes in Computer Science*, pages 159–173, Berlin, Heidelberg, Apr. 2003. Springer.

[49] P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In *IEEE Symposium on Security and Privacy*, pages 71–85, May 2004.

[50] P. Laud. Secrecy types for a simulatable cryptographic library. In *12th ACM Conference on Computer and Communications Security (CCS'05)*, pages 26–35, New York, NY, Nov. 2005. ACM Press.

[51] P. Laud and I. Tśahhirov. A user interface for a game-based protocol verification tool. In P. Degano and J. Guttman, editors, *6th International Workshop on Formal Aspects in Security and Trust (FAST2009)*, volume 5983 of *Lecture Notes in Computer Science*, pages 263–278, Berlin, Heidelberg, Nov. 2009. Springer.

[52] P. Laud and V. Vene. A type system for computationally secure information flow. In M. Liśkiewicz and R. Reischuk, editors, *15th International Symposium on Fundamentals of Computation Theory (FCT'05)*, volume 3623 of *Lecture Notes in Computer Science*, pages 365–377, Berlin, Heidelberg, Aug. 2005. Springer.

[53] B. Lipp, B. Blanchet, and K. Bhargavan. A mechanised cryptographic proof of the Wire-Guard virtual private network protocol. In *IEEE European Symposium on Security and Privacy (EuroS&P'19)*, pages 231–246, Stockholm, Sweden, June 2019. IEEE Computer Society.

[54] J. C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A probabilistic polynomial-time calculus for the analysis of cryptographic protocols. *Theoretical Computer Science*, 353(1–3):118–164, Mar. 2006.
[55] D. Nowak. A framework for game-based security proofs. In S. Qing, H. Imai, and G. Wang, editors, *Information and Communications Security, 9th International Conference, ICICS 2007*, volume 4861 of Lecture Notes in Computer Science, pages 319–333, Berlin, Heidelberg, Dec. 2007. Springer.

[56] D. Nowak. On formal verification of arithmetic-based cryptographic primitives. In P. J. Lee and J. H. Cheon, editors, *Information Security and Cryptology - ICISC 2008, 11th International Conference*, volume 5461 of Lecture Notes in Computer Science, pages 368–382, Berlin, Heidelberg, Dec. 2008. Springer.

[57] D. Nowak and Y. Zhang. A calculus for game-based security proofs. In *Provable Security, Fourth International Conference, ProvSec 2010*, volume 6402 of Lecture Notes in Computer Science, pages 35–52, Berlin, Heidelberg, Oct. 2010. Springer.

[58] T. Okamoto and D. Pointcheval. The gap-problems: a new class of problems for the security of cryptographic schemes. In K. Kim, editor, *International Workshop on Practice and Theory in Public Key Cryptography (PKC'2001)*, volume 1992 of Lecture Notes in Computer Science, pages 104–118, Berlin, Heidelberg, Feb. 2001. Springer.

[59] A. Petcher and G. Morrisett. The foundational cryptography framework. In R. Focardi and A. C. Myers, editors, *4th International Conference on Principles of Security and Trust (POST'15)*, volume 9036 of Lecture Notes in Computer Science, pages 53–72, Berlin, Heidelberg, Apr. 2015. Springer.

[60] D. Pointcheval and J. Stern. Security proofs for signature schemes. In U. Maurer, editor, *Advances in Cryptology — EUROCRYPT '96*, volume 1070 of Lecture Notes in Computer Science, pages 387–398, Berlin, Heidelberg, May 1996. Springer.

[61] V. Shoup. A proposal for an ISO standard for public-key encryption, Dec. 2001. ISO/IEC JTC 1/SC27.

[62] V. Shoup. OAEP reconsidered. *Journal of Cryptology*, 15(4):223–249, Sept. 2002.

[63] V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332, Nov. 2004. Available at http://eprint.iacr.org/2004/332.

[64] G. Smith and R. Alpízar. Secure information flow with random assignment and encryption. In *4th ACM Workshop on Formal Methods in Security Engineering (FMSE'06)*, pages 33–43, Nov. 2006.

[65] C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, and M. Waidner. Cryptographically sound theorem proving. In *19th IEEE Computer Security Foundations Workshop (CSFW-19)*, pages 153–166, Los Alamitos, CA, July 2006. IEEE Computer Society Press.

[66] C. Sprenger and D. Basin. Cryptographically-sound protocol-model abstractions. In *23rd Annual IEEE Symposium on Logic in Computer Science*, pages 3–17, Los Alamitos, CA, June 2008. IEEE Computer Society Press.

[67] I. Tšahhirov and P. Laud. Application of dependency graphs to security protocol analysis. In G. Barthe and C. Fournet, editors, *3rd Symposium on Trustworthy Global Computing (TGC'07)*, volume 4912 of Lecture Notes in Computer Science, pages 294–311, Berlin, Heidelberg, Nov. 2007. Springer.
[68] T. Y. C. Woo and S. S. Lam. Authentication for distributed systems. In D. Denning and P. Denning, editors, *Internet Besieged: Countering Cyberspace Scofflaws*, pages 319-355. ACM Press and Addison-Wesley, Oct. 1997.
Inria

RESEARCH CENTRE
PARIS

2 rue Simone Iff - CS 42112
75589 Paris Cedex 12

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399