T. Acar, M. Belenkiy, M. Bellare, and D. Cash, Cryptographic Agility and Its Relation to Circular Encryption, EUROCRYPT, pp.403-422, 2010.
DOI : 10.1007/978-3-642-13190-5_21

A. Askarov, D. Zhang, and A. C. Myers, Predictive black-box mitigation of timing channels, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.297-307, 2010.
DOI : 10.1145/1866307.1866341

M. Avalle, A. Pironti, D. Pozza, and R. Sisto, JavaSPI, International Journal of Secure Software Engineering, vol.2, issue.4, pp.34-48, 2011.
DOI : 10.4018/jsse.2011100103

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

M. Backes, C. Hritcu, M. Maffei, and T. Tarrach, Type-checking implementations of protocols based on zero-knowledge proofs, FCS, 2009.

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

M. Backes, C. Hrit¸cuhrit¸cu, and M. Maffei, Union and Intersection Types for Secure Protocol Implementations, TOSCA'11, pp.1-28
DOI : 10.1007/978-3-642-27375-9_1
URL : https://hal.archives-ouvertes.fr/hal-01102192

M. Bellare, A. Desai, E. Jokipii, and P. Rogaway, A concrete security treatment of symmetric encryption, Proceedings 38th Annual Symposium on Foundations of Computer Science, pp.394-403, 1997.
DOI : 10.1109/SFCS.1997.646128

J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, Refinement types for secure implementations, ACM TOPLAS, vol.33, issue.2, p.8, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01294973

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, POPL, pp.445-456, 2010.

K. Bhargavan, C. Fournet, R. Corin, and E. , Verified Cryptographic Implementations for TLS, ACM Transactions on Information and System Security, vol.15, issue.1, pp.1-32, 2012.
DOI : 10.1145/2133375.2133378
URL : https://hal.archives-ouvertes.fr/hal-00863381

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, A computationally sound mechanized prover for security protocols, IEEE S&P, pp.140-154, 2006.

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

B. Brumley, M. Barbosa, D. Page, and F. Vercauteren, Practical Realisation and Elimination of an ECC-Related Software Bug Attack, CT-RSA, 2011.
DOI : 10.1007/11761679_2

D. Brumley and D. Boneh, Remote timing attacks are practical, USENIX Security, pp.1-14, 2003.
DOI : 10.1016/j.comnet.2005.01.010

B. Canvel, A. P. Hiltgen, S. Vaudenay, and M. Vuagnoux, Password Interception in a SSL/TLS Channel, CRYPTO, pp.583-599, 2003.
DOI : 10.1007/978-3-540-45146-4_34

S. Chaki and A. 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

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, 2008.
DOI : 10.1007/978-3-540-78800-3_24

G. Díaz, F. Curtero, V. Valero, and F. Pelayo, Automatic verification of the TLS handshake protocol, Proceedings of the 2004 ACM symposium on Applied computing , SAC '04, pp.789-794, 2004.
DOI : 10.1145/967900.968063

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.1. RFC 4346, 2006.

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.2. RFC 5246, 2008.

K. P. Dyer, S. E. Coull, T. Ristenpart, and T. Shrimpton, Peeka-boo , I still see you: Why efficient traffic analysis countermeasures fail, IEEE S&P, pp.332-346, 2012.

P. Fouque, D. Pointcheval, and S. Zimmer, HMAC is a randomness extractor and applications to TLS, Proceedings of the 2008 ACM symposium on Information, computer and communications security , ASIACCS '08, pp.21-32, 2008.
DOI : 10.1145/1368310.1368317
URL : https://hal.archives-ouvertes.fr/inria-00419158

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, pp.341-350, 2011.
DOI : 10.1145/2046707.2046746
URL : https://hal.archives-ouvertes.fr/inria-00614372

A. Freier, P. Karlton, and P. Kocher, The secure sockets layer (SSL) protocol version 3, pp.0-1996, 2011.
DOI : 10.17487/rfc6101

S. Gajek, M. Manulis, O. Pereira, A. Sadeghi, and J. Schwenk, Universally Composable Security Analysis of TLS, ProvSec, pp.313-327, 2008.
DOI : 10.1007/11555827_28

M. Georgiev, S. Iyengar, S. Jana, R. Anubhai, D. Boneh et al., The most dangerous code in the world, Proceedings of the 2012 ACM conference on Computer and communications security, CCS '12, pp.38-49, 2012.
DOI : 10.1145/2382196.2382204

S. Goldwasser, S. Micali, and R. L. 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

C. He, M. Sundararajan, A. Datta, A. Derek, and J. C. Mitchell, A modular correctness proof of IEEE 802.11i and TLS, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, pp.2-15, 2005.
DOI : 10.1145/1102120.1102124

T. Jager, F. Kohlar, S. Schäge, and J. Schwenk, On the Security of TLS-DHE in the Standard Model, CRYPTO, pp.273-293, 2012.
DOI : 10.1007/978-3-642-32009-5_17

J. Jonsson and J. B. Kaliski, On the Security of RSA Encryption in TLS, CRYPTO, pp.127-142, 2002.
DOI : 10.1007/3-540-45708-9_9

J. Jürjens, 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

A. Kamil and G. Lowe, Analysing TLS in the strand spaces model, Journal of Computer Security, vol.19, issue.5, 2008.
DOI : 10.3233/JCS-2011-0429

J. Kelsey, Compression and Information Leakage of Plaintext, Fast Software Encryption, pp.95-102, 2002.
DOI : 10.1007/3-540-45661-9_21

V. Klima, O. Pokorny, and T. Rosa, Attacking RSA-Based Sessions in SSL/TLS, CHES, pp.426-440, 2003.
DOI : 10.1007/978-3-540-45238-6_33

H. Krawczyk, The Order of Encryption and Authentication for Protecting Communications (or: How Secure Is SSL?), CRYPTO'01, 2001.
DOI : 10.1007/3-540-44647-8_19

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

R. Küsters, T. Truderung, and J. Graf, A Framework for the Cryptographic Verification of Java-Like Programs, 2012 IEEE 25th Computer Security Foundations Symposium, pp.198-212, 2012.
DOI : 10.1109/CSF.2012.9

A. Langley, Unfortunate current practices for HTTP over TLS, 2011.

N. M. Langley, A. , and B. Moeller, Transport Layer Security (TLS) False Start, 2010.
DOI : 10.17487/RFC7918

J. Lawall, B. Laurie, R. R. Hansen, N. Palix, and G. Muller, Finding Error Handling Bugs in OpenSSL Using Coccinelle, 2010 European Dependable Computing Conference, 2010.
DOI : 10.1109/EDCC.2010.31
URL : https://hal.archives-ouvertes.fr/hal-00940375

N. Mavrogiannopoulos and S. Josefsson, GnuTLS documentation on record padding, 2011.

N. Mavrogiannopoulos, F. Vercauteren, V. Velichkov, and B. Preneel, A cross-protocol attack on the TLS protocol, Proceedings of the 2012 ACM conference on Computer and communications security, CCS '12, pp.62-72, 2012.
DOI : 10.1145/2382196.2382206

B. Moeller, Security of CBC ciphersuites in SSL/TLS: Problems and countermeasures, 2004.

P. Morrissey, N. Smart, and B. Warinschi, A Modular Security Analysis of the TLS Handshake Protocol, ASIACRYPT'08, pp.55-73, 2008.
DOI : 10.1145/322510.322530

K. Ogata and K. Futatsugi, Equational Approach to Formal Analysis of TLS, 25th IEEE International Conference on Distributed Computing Systems (ICDCS'05), pp.795-804, 2005.
DOI : 10.1109/ICDCS.2005.32

K. G. Paterson, T. Ristenpart, and T. Shrimpton, Tag Size Does Matter: Attacks and Proofs for the TLS Record Protocol, ASIACRYPT 2011, pp.372-389, 2011.
DOI : 10.1007/978-3-642-25385-0_20

L. C. Paulson, Inductive analysis of the Internet protocol TLS, ACM Transactions on Information and System Security, vol.2, issue.3, pp.332-351, 1999.
DOI : 10.1145/322510.322530

M. Ray, Authentication gap in TLS renegotiation, 2009.

E. Rescorla, M. Ray, S. Dispensa, and N. Oskov, TLS renegotiation indication extension, 2010.

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with value-dependent types, ICFP, pp.266-278, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00939188

S. Turner and T. Polk, Prohibiting secure sockets layer (SSL) version 2.0. RFC 6176, 2011.

S. Vaudenay, S. , I. , and W. , Security flaws induced by CBC padding applications to, pp.534-546, 2002.

A. K. Yau, K. G. Paterson, and C. J. Mitchell, Padding Oracle Attacks on CBC-Mode Encryption with Secret and Random IVs, FSE, pp.299-319, 2005.
DOI : 10.1007/11502760_20