M. Abadi, M. Baudet, and B. Warinschi, Guessing Attacks and the Computational Soundness of Static Equivalence, Foundations of Software Science and Computation Structure (FoSSaCS'06), pp.398-412, 2006.
DOI : 10.1007/11690634_27

M. Abadi and V. Cortier, Deciding Knowledge in Security Protocols under (Many More) Equational Theories, 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp.62-76, 2005.
DOI : 10.1109/CSFW.2005.14
URL : https://hal.archives-ouvertes.fr/inria-00000554

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Principles of Program-ming Languages (POPL'01), pp.104-115, 2001.
DOI : 10.1145/373243.360213
URL : https://hal.archives-ouvertes.fr/hal-01423924

M. Abadi and A. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, 1999.
DOI : 10.1145/266420.266432

M. Abadi and P. Rogaway, Reconciling two views of cryptography: the computational soundness of formal encryption, Int. Conf. on Theoretical Computer Science, 2000.

M. Abdalla and B. Warinschi, On the Minimal Assumptions of Group Signature Schemes, 6th International Conference on Information and Communication Security, pp.1-13, 2004.
DOI : 10.1007/978-3-540-30191-2_1

P. Adão and C. Fournet, Cryptographically Sound Implementations for Communicating Processes, International Colloquium on Algorithms, Languages and Programming (ICALP'06), 2006.
DOI : 10.1007/11787006_8

A. Armando, The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Computer Aided Verification, pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

M. Backes, M. Dürmuth, and R. Küsters, On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2007.
DOI : 10.1007/978-3-540-77050-3_9

M. Backes and B. Pfitzmann, Symmetric encryption in a simulatable Dolev-Yao style cryptographic library, Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004., 2004.
DOI : 10.1109/CSFW.2004.1310742

M. Backes and B. Pfitzmann, Relating cryptographic und symbolic key secrecy, Symp. on Security and Privacy (SSP'05), pp.171-182, 2005.
DOI : 10.1109/sp.2005.17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.8373

M. Backes, B. Pfitzmann, and M. Waidner, A com-posable cryptographic library with nested operations, 10th ACM Concerence on Computer and Communications Security (CCS'03), 2003.

M. Backes, B. Pfitzmann, and M. Waidner, The reactive simulatability (RSIM) framework for asynchronous systems, Information and Computation, vol.205, issue.12, pp.1685-1720, 2007.
DOI : 10.1016/j.ic.2007.05.002

G. Bana, Soundness and completeness of formal logics of symmetric encryption, Cryptology ePrint Archive Report, vol.101, 2005.

M. Baudet, V. Cortier, and S. Kremer, Computationally sound implementations of equational theories against passive adversaries, Int. Colloquium on Automata, Languages and Programming (ICALP'05), 2005.
URL : https://hal.archives-ouvertes.fr/inria-00426620

M. Bellare and C. Namprempre, Authenticated encryption: relations among notions and analysis of the generic composition paradigm, Advances in Cryptology, pp.531-545, 1976.

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930138
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.5150

B. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.3-51, 2008.
DOI : 10.1109/LICS.2005.8

M. Burrows, M. Abadi, and R. Needham, A logic of authentication, 1989.

R. Canetti, Universal composable security: a new paradigm for cryptographic protocols, Symposium on Foundations of Computer Science, 2001.

R. Canetti and J. Herzog, Universally composable symbolic analysis of cryptographic protocols, Theory of Cryptography Conference (TCC'06), 2006.

R. Canetti and T. Rabin, Universal Composition with Joint State, Cryptology ePrint Archive, vol.47, 2002.
DOI : 10.1007/978-3-540-45146-4_16

V. Cortier, S. Kremer, R. Küsters, and B. Warinschi, Computationally Sound Symbolic Secrecy in the Presence of Hash Functions, Fundations of Software Technology and Theoretical Computer Science (FSTTCS'06), pp.176-187, 2006.
DOI : 10.1007/11944836_18
URL : https://hal.archives-ouvertes.fr/inria-00108386

V. Cortier and B. Warinschi, Computationally Sound, Automated Proofs for Security Protocols, European Symposium on Programming (ESOP'05), pp.157-171, 2005.
DOI : 10.1007/978-3-540-31987-0_12
URL : https://hal.archives-ouvertes.fr/inria-00000556

S. Delaune, S. Kremer, and M. D. Ryan, Coercion-Resistance and Receipt-Freeness in Electronic Voting, 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.28-39, 2006.
DOI : 10.1109/CSFW.2006.8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.218.4709

S. Delaune, S. Kremer, and M. D. Ryan, Symbolic bisimulation for the applied pi-calculus, Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp.133-145, 2007.

R. Janvier, Y. Lakhnech, and L. Mazaré, Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries, European Symposium on Programming (ESOP'05), pp.172-185, 2005.
DOI : 10.1007/978-3-540-31987-0_13

R. Janvier, Y. Lakhnech, and L. Mazare, (de)compositions of cryptographic schemes and their applications to protocols, Cryptology ePrint Archive, 2005.

R. Janvier, Y. Lakhnech, and L. Mazaré, Computational Soundness of Symbolic Analysis for Protocols Using Hash Functions, Workshop on Information and Computer Security (ICS'06), 2006.
DOI : 10.1016/j.entcs.2007.01.066

A. Juels, M. Luby, and R. Ostrovsky, Security of blind digital signatures, advances in cryptology, pp.150-164, 1997.
DOI : 10.1007/BFb0052233

S. Kremer and L. Mazaré, Adaptive Soundness of Static Equivalence, European Symposium on Research in Computer Security (ESORICS'07), pp.610-625, 2007.
DOI : 10.1007/978-3-540-74835-9_40

R. Küsters and M. Tuengerthal, Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation, 2008 21st IEEE Computer Security Foundations Symposium, 2008.
DOI : 10.1109/CSF.2008.18

P. Laud, Symmetric encryption in automatic analyses for confidentiality against active adversaries, Symp. on Security and Privacy, pp.71-85, 2004.

D. Micciancio and B. Warinschi, Completeness theorems for the Abadi-Rogaway language of encrypted expressions, Journal of Computer Security, 2004.

D. Micciancio and B. Warinschi, Soundness of formal encryption in presence of an active attacker, Theory of Cryptography Conference, 2004.

J. Mitchell, A. Ramanathan, and V. Teague, A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols, Theoretical Computer Science, vol.353, issue.1-3, pp.118-164, 2006.
DOI : 10.1016/j.tcs.2005.10.044

I. Centre-de-recherche, ?. Nancy, and L. Est, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès

I. Centre-de-recherche, ?. Bordeaux, and . Ouest, Domaine Universitaire -351, cours de la Libération -33405 Talence Cedex Centre de recherche INRIA Grenoble ? Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier Centre de recherche INRIA Lille ? Nord Europe : Parc Scientifique de la Haute Borne -40, avenue Halley -59650 Villeneuve d'Ascq Centre de recherche INRIA Paris ? Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex Centre de recherche INRIA Rennes ? Bretagne Atlantique : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex Centre de recherche INRIA Saclay ? Île-de-France, des Vignes : 4, rue Jacques Monod -91893 Orsay Cedex Centre de recherche INRIA, pp.93-06902, 2004.