A. , M. And-fournet, and C. , Mobile values, new names, and secure communication, 28th ACM Symposium on Principles of Programming Languages (POPL'01, pp.104-115, 2001.

B. , M. And-laud, and P. , Computationally sound secrecy proofs by mechanized flow analysis, 13th ACM conference on Computer and Communications Security (CCS'06, pp.370-379, 2006.

B. , M. Canetti, R. And-krawczyk, and H. , Keying hash functions for message authentication, 16th Annual Cryptology Conference on Advances in Cryptology (CRYPTO'96, pp.1-15, 1996.

B. , M. And-rogaway, and P. , Random oracles are practical: A paradigm for designing efficient protocols, 1st ACM Conference on Computer and Communications Security (CCS'93, pp.62-73, 1993.

B. , K. Corin, R. Fournet, C. And-zalinescu, and E. , Computational security for cryptographic protocol implementations, 2009.

B. , K. Fournet, C. Gordon, A. D. And-tse, and S. , Verified interoperable implementations of security protocols, 19th IEEE Computer Security Foundations Workshop (CSFW'06, pp.139-152, 2006.

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.82-96, 2001.
DOI : 10.1109/CSFW.2001.930138

B. Blanchet, From Secrecy to Authenticity in Security Protocols, 9th International Static Analysis Symposium (SAS'02, pp.342-359, 2002.
DOI : 10.1007/3-540-45789-5_25

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

B. Blanchet, Computationally Sound Mechanized Proofs of Correspondence Assertions, 20th IEEE Computer Security Foundations Symposium (CSF'07), pp.97-111, 2007.
DOI : 10.1109/CSF.2007.16

B. Blanchet, A. D. Jaggard, A. Scedrov, and J. And-tsay, Computationally sound mechanized proofs for basic and public-key Kerberos, Proceedings of the 2008 ACM symposium on Information, computer and communications security , ASIACCS '08, pp.87-99, 2008.
DOI : 10.1145/1368310.1368326

B. Blanchet and D. And-pointcheval, Automated Security Proofs with Sequences of Games, 26th Annual International Cryptology Conference (CRYPTO'06, pp.537-554, 2006.
DOI : 10.1007/11818175_32

C. , S. And, and A. Datta, ASPIER: An automated framework for verifying security protocol implementations, 2008.

C. , R. And, and J. Den-hartog, A probabilistic hoare-style logic for game-based cryptographic proofs, 33rd International Colloquium on Automata, Languages and Programming, Part II (ICALP'06, pp.252-263, 2006.

D. , A. Derek, A. Mitchell, J. C. And-warinschi, and B. , Computationally sound compositional logic for key exchange protocols, 19th IEEE workshop on Computer Security Foundations (CSFW'06, pp.321-334, 2006.

D. , G. Curtero, F. Valero, V. And-pelayo, and F. , Automatic verification of the TLS handshake protocol, 19th ACM Symposium on Applied Computing, pp.789-794, 2004.

D. , T. Allen, and C. , The TLS protocol version 1, 1999.

D. , T. And-rescorla, E. Dierks, T. And-rescorla, and E. , The Transport Layer Security (TLS) Protocol Version 1.1, The Transport Layer Security (TLS) Protocol Version 1, 2006.

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

F. , P. Pointcheval, D. And-zimmer, and S. , HMAC is a randomness extractor and applications to TLS, ACM Symposium on Information, Computer and Communications Security (ASIACCS'08). ACM, pp.21-32, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00419158

F. , A. O. Karlton, P. And-kocher, and P. C. , The SSL protocol version 3.0, 1996.

G. , S. Manulis, M. Sadeghi, A. And-schwenk, and J. , Provably secure browser-based user-aware mutual authentication over TLS, ACM Symposium on Information, Computer and Communications Security (ASIACCS'08, pp.300-311, 2008.

G. , J. And-parrennes, and F. , Cryptographic protocol analysis on real C code, 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05, pp.363-379, 2005.

H. , C. Sundararajan, M. Datta, A. Derek, A. And-mitchell et al., A modular correctness proof of IEEE 802.11i and TLS, 12th ACM conference on Computer and Communications Security (CCS'05). ACM, pp.2-15, 2005.

J. , J. S. And-b, and J. Kaliski, On the security of RSA encryption in TLS, 22nd Annual International Cryptology Conference, pp.127-142, 2002.

J. Urjens and J. , Security Analysis of Crypto-based Java Programs using Automated Theorem Provers, 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06), pp.167-176, 2006.
DOI : 10.1109/ASE.2006.60

K. , A. And, and G. Lowe, Analysing TLS in the strand spaces model, 2008.

K. , V. Pokorny, O. And-rosa, and T. , Attacking RSA-based sessions in SSL/TLS, Cryptographic Hardware and Embedded Systems (CHES'03). Lecture Notes on Computer Science, pp.426-440, 2003.

M. , J. C. Shmatikov, V. And, and U. Stern, Finite-state analysis of SSL 3.0, 7th USENIX Security Symposium (SSYM'98). USENIX Association, pp.201-216, 1998.

M. , P. Smart, N. And-warinschi, and B. , A modular security analysis of the TLS handshake protocol, 14th Annual International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT'08, pp.55-73, 2008.

N. , R. Schroeder, and M. , Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.

O. , K. And-futatsugi, and K. , Equational approach to formal analysis of TLS, 25th IEEE International Conference on Distributed Computing Systems (ICSCS'05, pp.795-804, 2005.

P. , D. H. And-pointcheval, and D. , About the security of ciphers (semantic security and pseudo-random permutations), 11th International Workshop on Selected Areas in Cryptography, pp.182-197, 2004.

T. , I. And-laud, and P. , Application of dependency graphs to security protocol analysis, 3rd Symposium on Trustworthy Global Computing, pp.294-311, 2007.

W. , D. And, and B. Schneier, Analysis of the SSL 3.0 protocol, 2nd USENIX Workshop on Electronic Commerce (WOEC'96). USENIX Association, pp.29-40, 1996.

Y. , A. K. Paterson, K. G. And-mitchell, and C. J. , Padding oracle attacks on CBC-mode encryption with secret and random IVs, Fast Software Encryption, pp.299-319, 2005.