M. Abadi and B. Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM, vol.52, issue.1, pp.102-146, 2005.
DOI : 10.1145/1044731.1044735

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

T. Acar, C. Fournet, and D. Shumow, DKM: Design and verification of a crypto-agile distributed key manager, 2011.

M. Aizatulin, A. D. Gordon, and J. Jürjens, Extracting and verifying cryptographic models from C protocol code by symbolic execution, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, 2011.
DOI : 10.1145/2046707.2046745

M. Albrecht, K. Paterson, and G. Watson, Plaintext Recovery Attacks against SSH, 2009 30th IEEE Symposium on Security and Privacy, pp.16-26, 2009.
DOI : 10.1109/SP.2009.5

M. Backes, M. Maffei, and D. Unruh, Computationally sound verification of source code, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.387-398, 2010.
DOI : 10.1145/1866307.1866351

M. Backes, C. Hrit¸cuhrit¸cu, and M. Maffei, Union and Intersection Types for Secure Protocol Implementations, TOSCA, 2011.
DOI : 10.1007/978-3-642-27375-9_1

URL : https://hal.archives-ouvertes.fr/hal-01102192

I. Baltopoulos and A. D. Gordon, Secure compilation of a multi-tier web language, Proceedings of the 4th international workshop on Types in language design and implementation, TLDI '09, pp.27-38, 2009.
DOI : 10.1145/1481861.1481866

I. Baltopoulos, J. Borgström, and A. D. Gordon, Maintaining Database Integrity with Refinement Types, 2011.
DOI : 10.1017/S0956796806006216

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

M. Bellare, R. Canetti, and H. Krawczyk, Keying Hash Functions for Message Authentication, LNCS, vol.1109, pp.1-15, 1996.
DOI : 10.1007/3-540-68697-5_1

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, pp.123-135, 2008.
DOI : 10.1145/1368310.1368330

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, Verified interoperable implementations of security protocols, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, pp.1-561, 2008.
DOI : 10.1145/1452044.1452049

K. Bhargavan, R. Corin, P. Deniélou, C. Fournet, and J. J. Leifer, Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, pp.124-140, 2009.
DOI : 10.1109/CSF.2009.26

K. Bhargavan, R. Corin, P. Deniélou, C. Fournet, and J. J. Leifer, Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, pp.124-140, 2009.
DOI : 10.1109/CSF.2009.26

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, ACM Symposium on Principles of Programming Languages (POPL'10), pp.445-456, 2010.

D. Bleichenbacher, Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS #1, Advances in Cryptology -CRYPTO '98, pp.1-12, 1998.
DOI : 10.1007/BFb0055716

J. Borgström, A. D. Gordon, and R. Pucella, Roles, stacks, histories: A triple for Hoare, Journal of Functional Programming, vol.29, issue.02, pp.159-207, 2011.
DOI : 10.1145/1057387.1057392

I. Cervesato, A. D. Jaggard, A. Scedrov, J. Tsay, and C. Walstad, Breaking and fixing public-key Kerberos, Information and Computation, vol.206, pp.2-4402, 2008.

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

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, TPHOLs, pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15

R. Corin and F. A. Manzano, Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations, ESSoS, pp.58-72, 2011.
DOI : 10.1007/978-3-642-19125-1_5

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-208, 1983.
DOI : 10.1109/TIT.1983.1056650

F. Dupressoir, A. Gordon, J. Jürjens, and D. Naumann, Guiding a general-purpose C verifier to prove cryptographic protocols, 24th IEEE Computer Security Foundations Symposium, 2011.

C. Fournet, M. Kohlweiss, and P. Strub, Modular code-based cryptographic verification, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, p.7, 2011.
DOI : 10.1145/2046707.2046746

URL : https://hal.archives-ouvertes.fr/inria-00614372

S. Goldwasser, R. Micali, and . Rivest, A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks, SIAM Journal on Computing, vol.17, issue.2, pp.281-308, 1988.
DOI : 10.1137/0217017

A. D. Gordon and C. Fournet, Principles and applications of refinement types Logics and Languages for Reliability and Security, 2010.

J. Goubault-larrecq and F. Parrennes, Cryptographic Protocol Analysis on Real C Code, VMCAI, pp.363-379, 2005.
DOI : 10.1007/978-3-540-30579-8_24

N. Guts, C. Fournet, and F. Z. Nardelli, Reliable Evidence: Auditability by Typing, 14th European Symposium on Research in Computer Security (ESORICS'09), pp.168-183, 2009.
DOI : 10.1016/S0140-3664(02)00049-X

H. Krawczyk, M. Bellare, and R. Canetti, HMAC: Keyed-hashing for message authentication, 1997.
DOI : 10.17487/rfc2104

. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, TACAS, volume 1055 of Lecture Notes in Computer Science, pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43

. Milner, Communicating and Mobile Systems: the ?-Calculus, 1999.

R. Needham and M. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.
DOI : 10.1145/359657.359659

A. Pironti and J. Jürjens, Formally-Based Black-Box Monitoring of Security Protocols, ESSoS, pp.79-95, 2010.
DOI : 10.1007/978-3-642-11747-3_7

N. Swamy, J. Chen, and R. Chugh, Enforcing Stateful Authorization and Information Flow Policies in Fine, ESOP, pp.529-549, 2010.
DOI : 10.1007/978-3-642-11957-6_28

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with value-dependent types, International Conference on Functional Programming, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00939188

S. Vaudenay, S. , I. , and W. , Security Flaws Induced by CBC Padding ??? Applications to SSL, IPSEC, WTLS..., Advances in Cryptology -EUROCRYPT 2002, pp.534-545, 2002.
DOI : 10.1007/3-540-46035-7_35