M. Abadi, Secrecy by typing in security protocols, JACM, vol.46, issue.5, 1999.

M. Abadi and B. Blanchet, Analyzing security protocols with secrecy types and logic programs, JACM, vol.52, issue.1, 2005.
DOI : 10.1145/1044731.1044735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.3131

M. Abadi and P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), J. Crypt, vol.15, issue.2, 2002.

M. Backes, B. Pfitzmann, and M. Waidner, Symmetric authentication in a simulatable Dolev???Yao-style cryptographic library, International Journal of Information Security, vol.6, issue.3, 2005.
DOI : 10.1007/s10207-004-0056-6

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

M. Backes, M. Dürmuth, D. Hofheinz, and R. Küsters, Conditional reactive simulatability, Int. J. Inf. Sec, vol.7, issue.2, 2008.
DOI : 10.1007/s10207-007-0046-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.1707

M. Backes, D. Hofheiz, and D. Unruh, CoSP, Proceedings of the 16th ACM conference on Computer and communications security, CCS '09, 2009.
DOI : 10.1145/1653662.1653672

M. Backes, M. Maffei, and D. Unruh, Computational sound verification of source code, ACM CCS 09, 2010.

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Formal Certification of ElGamal Encryption, 2008.
DOI : 10.1007/978-3-642-01465-9_1

G. Barthe, B. Gregoire, S. Heraud, and S. Zanella-béguelin, Computer-Aided Security Proofs for the Working Cryptographer, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

M. Bellare and C. Namprempre, Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, J. Crypt, vol.21, 2008.

M. Bellare and P. Rogaway, Introduction to modern cryptography, UCSD CSE 207 Course Notes, 2005.

M. Bellare and P. Rogaway, The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, EURO- CRYPT 2006, 2006.
DOI : 10.1007/11761679_25

M. Bellare, R. Canetti, and H. Krawczyk, Keying hash functions for message authentication Refinement types for secure implementations, CRYPTO'96, pp.2008-118, 1996.

K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu, Cryptographically verified implementations for TLS, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, 2008.
DOI : 10.1145/1455770.1455828

K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy, Verified implementations of the information card federated identity-management protocol, Proceedings of the 2008 ACM symposium on Information, computer and communications security , ASIACCS '08, 2008.
DOI : 10.1145/1368310.1368330

K. Bhargavan, R. Corin, P. Dénielou, C. Fournet, and J. Leifer, Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, 2009.
DOI : 10.1109/CSF.2009.26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.187

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, 2010.

B. Blanchet, A computationally sound mechanized prover for security protocols, IEEE Symposium on Security and Privacy, 2006.

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), 2008.
DOI : 10.1109/LICS.2005.8

R. Canetti, Universally composable security: a new paradigm for cryptographic protocols, Proceedings 2001 IEEE International Conference on Cluster Computing, 2001.
DOI : 10.1109/SFCS.2001.959888

S. Chaki and A. Datta, ASPIER: An Automated Framework for Verifying Security Protocol Implementations, 2009 22nd IEEE Computer Security Foundations Symposium, 2009.
DOI : 10.1109/CSF.2009.20

N. A. Danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, POPL, 2008.

A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani, Probabilistic Polynomial-Time Semantics for a Protocol Security Logic, ICALP 2005, 2005.
DOI : 10.1007/11523468_2
URL : https://hal.archives-ouvertes.fr/inria-00103654

A. Datta, A. Derek, J. C. Mitchell, and A. Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science, vol.172, 2007.
DOI : 10.1016/j.entcs.2007.02.012
URL : http://doi.org/10.1016/j.entcs.2007.02.012

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, IT?, vol.29, issue.2, 1983.

F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann, Guiding a general-purpose C verifier to prove cryptographic protocols, CSF 2011, 2011.
DOI : 10.1109/csf.2011.8
URL : http://arxiv.org/abs/1312.6532

N. A. Durgin, J. C. Mitchell, and D. Pavlovic, A compositional logic for proving security properties of protocols*, Journal of Computer Security, vol.11, issue.4, 2003.
DOI : 10.3233/JCS-2003-11407

C. Fournet, K. Bhargavan, and A. Gordon, Cryptographic verification of protocol implementations by typechecking, FOSAD, 2011.

S. Goldwasser, S. Micali, and R. Rivest, A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks, SIAM Journal on Computing, vol.17, issue.2, 1988.
DOI : 10.1137/0217017
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.8353

J. Goubault-larrecq and F. Parrennes, Cryptographic Protocol Analysis on Real C Code, VMCAI'05, 2005.
DOI : 10.1007/978-3-540-30579-8_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.2108

S. Halevi, A plausible approach to computer-aided cryptographic proofs, Cryptology ePrint Archive Report, vol.181, 2005.

D. Hofheinz, D. Unruh, and J. Müller-quade, Polynomial runtime and composability. Cryptology ePrint Archive, Report, p.23, 2009.

B. M. Kapron and S. A. Cook, A new Characterization of Type-2 Feasibility, SIAM Journal on Computing, vol.25, issue.1, p.25, 1996.
DOI : 10.1137/S0097539794263452

H. Krawczyk, M. Bellare, and R. Canetti, HMAC: Keyed-hashing for message authentication, 1997.
DOI : 10.17487/rfc2104
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.383.2086

R. Küsters, Simulation-Based Security with Inexhaustible Interactive Turing Machines, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006.
DOI : 10.1109/CSFW.2006.30

R. Küsters and M. Tuengerthal, Universally Composable Symmetric Encryption, 2009 22nd IEEE Computer Security Foundations Symposium, 2009.
DOI : 10.1109/CSF.2009.18

P. Laud, Semantics and Program Analysis of Computationally Secure Information Flow, 2001.
DOI : 10.1007/3-540-45309-1_6

P. Laud, Secrecy types for a simulatable cryptographic library, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, 2005.
DOI : 10.1145/1102120.1102126

P. Laud, On the computational soundness of cryptographicallymasked flows, POPL, 2008.

J. H. Morris and J. , Protection in programming languages, Communications of the ACM, vol.16, issue.1, 1973.
DOI : 10.1145/361932.361937

C. Rackoff and D. R. Simon, Non-Interactive Zero-Knowledge Proof of Knowledge and Chosen Ciphertext Attack, CRYPTO'91, 1991.
DOI : 10.1007/3-540-46766-1_35

J. C. Reynolds, Types, abstraction and parametric polymorphism, IFIP Congress, 1983.

A. Roy, A. Datta, A. Derek, and J. C. Mitchell, Inductive trace properties for computational security, Journal of Computer Security, vol.18, issue.6, 2010.
DOI : 10.3233/JCS-2009-389
URL : http://doi.org/10.3233/jcs-2009-389