J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, Refinement Types for Secure Implementations, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, p.45, 2011.
DOI : 10.1109/csf.2008.27
URL : https://hal.archives-ouvertes.fr/hal-01294973

B. Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, 14th IEEE Computer Security Foundations Workshop (CSFW-14), pp.82-96, 2001.
DOI : 10.1109/csfw.2001.930138
URL : http://www.mpi-sb.mpg.de/~blanchet/publications/./BlanchetCSFW01.ps.gz

B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016.
DOI : 10.1561/3300000004
URL : https://hal.archives-ouvertes.fr/hal-01423760

B. Blanchet, M. Abadi, and C. Fournet, Automated verification of selected equivalences for security protocols, Journal of Logic and Algebraic Programming, vol.75, issue.1, pp.3-51, 2008.
DOI : 10.1016/j.jlap.2007.06.002
URL : https://doi.org/10.1016/j.jlap.2007.06.002

M. Bugliesi, S. Calzavara, F. Eigner, and M. Maffei, Resource-aware authorization policies for statically typed cryptographic protocols, 24th IEEE Computer Security Foundations Symposium, pp.83-98, 2011.
DOI : 10.1109/csf.2011.13

M. Bugliesi, S. Calzavara, F. Eigner, and M. Maffei, Logical foundations of secure resource management in protocol implementations, 2nd International Conference on Principles of Security and Trust, pp.105-125, 2013.
DOI : 10.1007/978-3-642-36830-1_6
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-36830-1_6.pdf

M. Bugliesi, S. Calzavara, F. Eigner, and M. Maffei, Affine Refinement Types for Secure Distributed Programming, ACM Transactions on Programming Languages and Systems, vol.37, issue.4, pp.1-11, 2015.
DOI : 10.1145/2743018
URL : https://iris.unive.it/bitstream/10278/3661939/1/toplas15.pdf

M. Bugliesi, R. Focardi, and M. Maffei, Authenticity by tagging and typing, ACM Workshop on Formal Methods in Security Engineering. pp. 1, 2004.
DOI : 10.1145/1029133.1029135

M. Bugliesi, R. Focardi, and M. Maffei, Analysis of typed analyses of authentication protocols, 18th IEEE Workshop on Computer Security Foundations, pp.112-125, 2005.

M. Bugliesi, R. Focardi, and M. Maffei, Dynamic types for authentication, Journal of Computer Security, vol.15, issue.6, pp.563-617, 2007.
DOI : 10.3233/jcs-2007-15602

R. Chadha, S. Ciobâc?-a, and S. Kremer, Automated verification of equivalence properties of cryptographic protocols, Programming Languages and Systems-Proceedings of the 21th
DOI : 10.1007/978-3-642-28869-2_6
URL : https://hal.archives-ouvertes.fr/inria-00632564

, European Symposium on Programming (ESOP'12), vol.7211, pp.108-127, 2012.

V. Cheval, Apte: an algorithm for proving trace equivalence, Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), vol.8413, pp.587-592, 2014.

V. Cheval, V. Cortier, and S. Delaune, Deciding equivalence-based properties using constraint solving, Theoretical Computer Science, vol.492, pp.1-39, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00881060

V. Cheval, . Cortier, . Véronique, and A. Plet, Lengths may break privacy-or how to check for equivalences with length, 25th International Conference on Computer Aided Verification (CAV'13), vol.8043, pp.708-723, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00881065

V. Cortier, S. Delaune, and A. Dallon, Sat-equiv: an efficient tool for equivalence properties, Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), 2017.
URL : https://hal.archives-ouvertes.fr/hal-01624274

V. Cortier, N. Grimm, J. Lallemand, and M. Maffei, A Type System for Privacy Properties, 24th ACM Conference on Computer and Communications Security (CCS'17), pp.409-423, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01626109

V. Cortier, N. Grimm, J. Lallemand, and M. Maffei, Equivalence Properties by Typing in Cryptographic Branching Protocols, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01900079

V. Cortier and B. Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security, vol.21, issue.1, pp.89-148, 2013.
URL : https://hal.archives-ouvertes.fr/inria-00638556

C. Cremers, The Scyther Tool: Verification, falsification, and analysis of security protocols, Computer Aided Verification, 20th International Conference, vol.5123, pp.414-418, 2008.

J. Dawson and A. Tiu, Automating open bisimulation checking for the spi-calculus, IEEE Computer Security Foundations Symposium (CSF 2010), 2010.

S. Delaune, S. Kremer, and M. D. Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security, vol.17, issue.4, pp.435-487, 2009.

F. Eigner and M. Maffei, Differential privacy by typing in security protocols, 26th IEEE Computer Security Foundations Symposium, pp.272-286, 2013.

S. Escobar, C. Meadows, and J. Meseguer, A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties, Theoretical Computer Science, vol.367, issue.1-2, pp.162-202, 2006.

R. Focardi and M. Maffei, Types for Security Protocols, Formal Models and Techniques for Analyzing Security Protocols, vol.5, pp.143-181, 2011.

A. D. Gordon and A. Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, vol.11, issue.4, pp.451-519, 2003.

S. Meier, B. Schmidt, C. Cremers, and D. Basin, The TAMARIN Prover for the Symbolic Analysis of Security Protocols, Computer Aided Verification, 25th International Conference, CAV 2013, vol.8044, pp.696-701, 2013.

P. Roenne, , 2016.

S. Santiago, S. Escobar, C. A. Meadows, and J. Meseguer, c)),-R(? ? LL ? ? l (c ?,? )) ?? = ? and R(? ? LL ? ? r (c ?,? )) ?? = ?,-? l (c ?,? ) and ? r (c ?,? ) restricted to vars(R) are ground, there exists a recipe R without destructors, ?= R (? ? LL ? ? l (c ?,? )),-R(? ? LL ? ? r, pp.162-177, 2014.

, All these case are similar, we write the proof generically for R = f (R 1 , R 2 ). By the induction hypothesis, there exist R 1 , R 2 such that ? for all i ? {1, 2}, vars(R i ) ? vars(R i ), ? for all i ? {1, 2}, R i (? ? LL ? ? l (c ?,? )) ?= R i (? ? LL ? ? l (c ?,? )), ? for all i ? {1, We prove the property by induction on R.-If R = x ? AX or R = a ? C ? FN then the claim holds with R = R, vol.2

. Let-r-=-f, ?= f (R 1 (? ? LL ? ? l (c ?,? )) ?, R 2 (? ? LL ? ? l (c ?,? )) ?), the second point implies that R(? ? LL ? ? l (c ?,? )) ?= R (? ? LL ? ? l (c ?,? )). Similarly, R(? ? LL ? ? r (c ?,? )) ?= R (? ? LL ? ? r (c ?,? )), and the claim holds.-If R = dec(S, K) for some recipes S, K, then since R(? ? LL ? ? l (c ?,? )) ?? = ?, we have K(? ? LL ? ? l (c ?,? )) ?= k for some k ? K, The first point imply that R satisfies the conditions on variables. Since R(? ? LL ? ? l

, where N = R(? ? LL ? ? r (c ?,? )) ?. In addition, by Lemma 37, there exists c such that ? ? ? LL ?? l (c ?,? ) ? ? ? LL ?? r (c ?,? ) : LL ? c. Thus by Lemma 23, there exists c such that ? K(? ? LL ? ? l (c ?,? )) ?? K(? ? LL ? ? r (c ?,? )) ?: LL ? c , which is to say ? k ? k : LL ? c. Hence by Lemma 20 and by well-formedness of ? , k = k and ? (k, k) <: key LL (T ) for some type T. Since S(? ? LL ? ? l (c ?,? )) ?= enc(M, k) = ?, and vars(S) ? vars(R), by the induction hypothesis, Similarly, there exists k ? K such that K(? ? LL ?? r (c ?,? )) ?= k and S(? ? LL ?? r (c ?,? )) ?= enc(N, k )

S. =-x-for-some-variable-x-?-ax-,-or-s-=-enc(s-,-k-)-for-some, S. , and K. , Moreover, S being a subterm of S itd also satisfies the conditions on the domains, and thus the property holds with R = S .-If R = adec(S, K) for some recipes S, K: this case is similar to the symmetric case.-If R = checksign(S, K) for some recipes S, K: then since R(? ? LL ? ? l (c ?,? )) ?? = ?, we have K(? ? LL ? ? l (c ?,? )) ?= vk(k) for, M. Hence R(? ? LL ? ? l (c ?,? )) ?= M = S (? ? LL ? ? l (c ?,? )), and similarly for ? r (c ?,? )

, Similarly, there exists k ? K such that K(? ? LL ? ? r (c ?,? )) ?= vk(k ) and S(? ? LL ? ? r (c ?,? )) ?= sign(N, k ), where N = R(? ? LL ? ? r

. Since-s(?-?-ll-?-?-l, ?= sign(M, k) = ?, by the induction hypothesis, there exists S such that vars(S ) ? vars(S), S (? ? LL ? ? l (c ?,? )) = S(? ? LL ? ? l (c ?,? )) ?= sign(M, k), and S (? ? LL ? ? r (c ?,? )) = S(? ? LL ? ? r

S. , K. )-for-some, S. , and K. , ? In the first case, we therefore have sign(M, k) ? sign(N, k ) ? c ?,?. In addition, by Lemma 37, there exists c ? c ?,? such that ? ? ? LL ? ? l (c ?,? ) ? ? ? LL ? ? r (c ?,? ) : LL ? c. Thus there exists c ? c such that ? sign(M, k) ? sign(N, k ) : LL ? c. Hence by Lemma 18, there exists c ? c ? c such that ? M ? N : LL ? c. Moreover M , N are ground, since by assumption ? l (c ?,? ) and ? r (c ?,? ) restricted to vars(R) are ground. Therefore, by Lemma 26, ? )) = sign(M, k), it is clear from the definition of ? that either S = x for some x ? AX , or S = sign

S. and K. , Since S (? ? LL ? ? l (c ?,? )) = sign(M, k), we have S (? ? LL ? ? l (c ?,? )) = M. Hence R(? ? LL ? ? l (c ?,? )) ?= M = S (? ? LL ? ? l (c ?,? )), and similarly for ? r (c ?,? ). Moreover, S being a subterm of S it also satisfies the conditions on the domains, and thus the property holds with R = S .-If R = ? 1 (S) for some recipe S then since R(? ? LL ? ? l (c ?,? )) ?? = ?

, M 1 , M 2 , where M 1 = R(? ? LL ? ? l (c ?,? )) ?, and M 2 is a message

S. Similarly and . (?-?-ll-?-?-r, ?= N 1 , N 2 , where N 1 = R(? ? LL ? ? r (c ?,? )) ?, and N 2 is a message

. Since-s(?-?-ll-?-?-l, ?= M 1 , M 2 = ?, by the induction hypothesis, there exists S such that vars(S ) ? vars(S), S (? ? LL ?? l (c ?,? )) = S(? ? LL ?? l, ?= M, k, and S (? ? LL ?? r

=. , it is clear from the definition of ? that either S = x for some x ? AX , or S = S 1 , S 2 for some S 1 , S 2. The first case is impossible, since by Lemma 35, step2 ? (c ?,? ) = true, and thus c ?,? does not contain pairs, Since S (? ? LL ? ? l (c ?,? )) = M 1 , M 2 , we have S 1 (? ? LL ? ? l (c ?,? )) = M 1. Hence R(? ? LL ? ? l (c ?,? )) ?= M 1 = S 1 (? ? LL ? ? l (c ?,? )), and similarly for ? r (c ?,? ). Moreover

, For all term t and substitution ? containing only messages

, We then have t 1 ? ?? = ? and t 2 ? ?? = ?, and t? ?= f (t 1 ? ?, t 2 ? ?), which, by the induction hypothesis, is equal to f (t 1 ? ?, t 2 ? ?), i.e. to f (t 1 , t 2 ) ? ?. The case where f is enc, aenc or sign is similar, the base case where t is a variable x, by definition of ?, since ?(x) is a messages, ?(x) ?= ?(x) and the claim holds

. ??-?-?.-?c-?.-?-n-,k-?-?-?-:-?-x-?-c-?, R) ? dom(? ? LL ? ? l (c)),-? l (c ?,? ) and ? r (c ?,? ) restricted to vars(R) are ground, for all x ? dom(? ? LL ? ? l (c)), if R(? ? LL ? ? l (c ?,? )) = (? ? LL ? ? l (c ?,? ))(x) then R is a variable y ? dom, Lemma 40. For all ground ?, ? , for all recipe R such that

, Similarly, if R(? ? LL ? ? r (c ?,? ) = (? ? LL ? ? r (c ?,? ))(x) then R is a variable y ? dom(? ? LL ? ? r (c)) or

, We distinguish several cases for R.-If R = a ? C ? FN : the claim clearly holds.-If R = x ? AX then the claim trivially holds.-If R = enc(S, K) or sign(S, K) for some recipes S, K: these two cases are similar, we only detail the encryption case. (? ? LL ? ? l (c ?,? ))(x) is then an encrypted message, We only detail the proof for ? l (c ?,? ), as the proof for ? r (c ?,? ) is similar, vol.35

, By definition of ? ? LL , this implies that ? (k, k) <: key LL (T ) for some T. Since ? is well-formed, this contradicts ? (k, k ) <: key HH (T ): this case is impossible.-If R = aenc(S, K) or h(S) for some recipes S, K: these two cases are similar, we only detail the encryption case. (? ? LL ? ? l (c ?,? ))(x) is then an asymmetrically encrypted message. By Lemma 35, we know that step2 ? (c ?,? ) = true. Hence S(? ? LL ? ? l (c ?,? )) contains directly under pairs a nonce n such that ? (n) = ? HH,a n , or a key k ? K such that ? (k, k ) = key HH (T ) for some T , k. This is only possible if there exists a recipe S such that S (? ? LL ? ? l (c ?,? )) = n (resp. k). Since S can only contain names from FN (and no keys), this implies that there exists a variable z such that (? ? LL ? ? l (? c ?,? ))(z) = n (resp. k). As step2 ? (c) = true, z can only be in dom(? ? LL ). Thus, by definition of ? ? LL , ? (n) = ? LL, This is only possible if there exists a variable z such that K = z and (? ? LL ? ? l (? c ?,? ))(z) = k. Since step2 ? (c) = true, z can only be in dom(? ? LL )

R. and S. Such-that-??-?-?.-?c-?-?-c-?,?.-?-n-,k-?-?-?, ? X ? c ? ,-vars(R) ? vars(S) ? dom(? ? LL ? ? l (c)),-? l (c ?,? ) and ? r (c ?,? ) restricted to vars(R) ? vars(S) are ground, we have (R(? ? LL ?? l (c ?,? ))) ?= (S(? ? LL ?? l (c ?,? ))) ? ?? (R(? ? LL ?? r (c ?,? ))) ?=, Lemma 41. For all ground ?, ? , for all recipes

. ??-=-?, We then assume that (R(? ? LL ? ? l (c ?,? ))) ?= (S(? ? LL ? ? l (c ?,? ))) ?. Let us first note that (R(? ? LL ? ? l (c ?,? ))) ?? = ? ?? (R(? ? LL ? ? r (c ?,? ))) ?? = ?. This follows from Lemmas 37 and 23. Similarly, we have S(? ? LL ? ? l

. ??-=-?, ? )) ?= ?. By assumption, in that case we also have S(? ? LL ? ? l (c ?,? )) ?= ?, and thus S(? ? LL ? ? r (c ?,? )) ?= ?, and the claim holds. Let us now assume that R(? ? LL ? ? l (c ?,? )) ?? = ?, i.e., by assumption, that S(? ? LL ? ? l (c ?,? )) ?? = ?, We then have R(? ? LL ? ? r (c ?,? )) ?? = ? and S(? ? LL ? ? r

, there exist recipes R , S without destructors such that-vars(R ) ? vars(S ) ? dom(? ? LL ? ? l (c ?,? )),-R(? ? LL ? ? l (c ?,? )) ?= R (? ? LL ? ? l (c ?,? )),-R(? ? LL ? ? r (c ?,? )) ?= R (? ? LL ? ? r, vol.38

S. (?-?-ll-?-?-l, ?= S (? ? LL ? ? l (c ?,? )),-S(? ? LL ? ? r (c ?,? )) ?= S (? ? LL ? ? r

, By the assumption, we have R (? ? LL ? ? l (c ?,? )) = S (? ? LL ? ? l

S. ?-c-?-f-n, we can distinguish four cases for R and S .-If they have the same head symbol, either this symbol is a nonce or constant and the claim is trivial, or it is a variable, and we handle this case later, or it is a constructor. We write the proof for this last case generically for R = f (R ) and S = f (S ), We show that R (? ? LL ? ? r (c ?,? )) = S (? ? LL ? ? r (c ?,? )) by induction on the recipes

, Indeed: ? if x, y ? dom(? ? LL ), this follows from the definition of ? ? LL. ? if x ? dom(? ? LL ) and y ? dom(? l (? c ?,? )): then by definition of ? ? LL , R (? ? LL ? ? l (c ?,? )) = ? ? LL (x) is a nonce, key, public key, or verification key. Hence ? l (c ?,? )(y) is also a nonce, key, public key or verification key. This is not possible, as by Lemma 35, step2 ? (c ?,? ) = true. ? if x, y ? dom, By step3 ? (c), we have M ? = N ?. Note that ? and ? have disjoint domains. Let x ? dom(?) ? (vars(M ) ? vars(N )). Then µ(x) = n for some n ? N. Thus ?(x) = µ(x)? = n. Since, by assumption, ?? ? ?. ?c ?. ? N ,K ? ? ? : ? X ? c ? , there exists c x such that ? N ,K n ? ? (x) : LL ? c x. Hence by Lemma, vol.20

. Therefore,

, we have R(? ? LL ? ? r (c ?,? )) ?= S(? ? LL ? ? r

?. Such-that-?c-?-?-c-?,?.-?-n-,k-?-?-?-:-?-x-?-c-?-,-?-n and K. , Lemma 42

. Proof, This is a direct consequence of Lemma 41, by unfolding the definition of static equivalence. Lemma 43. c is consistent in ?

. Proof, By Lemma 34, it suffices to show that c is consistent in ?. This is a direct consequence of Lemma 42, by unfolding the definition of consistency