M. Aizatulin, A. D. Gordon, and J. Jürjens, Computational verification of C protocol implementations by symbolic execution, Proceedings of the 2012 ACM conference on Computer and communications security, CCS '12, pp.712-723, 2012.
DOI : 10.1145/2382196.2382271

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

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII, pp.146-166, 2014.
DOI : 10.1145/1594834.1480894
URL : https://hal.archives-ouvertes.fr/hal-01114366

G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy et al., Probabilistic relational verification for cryptographic implementations, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.193-206, 2014.
DOI : 10.1145/2535838.2535847
URL : https://hal.archives-ouvertes.fr/hal-00935743

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computeraided security proofs for the working cryptographer, Advances in Cryptology ? CRYPTO 2011, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

G. Barthe, B. Grégoire, and S. Zanella, Formal certification of code-based cryptographic proofs, 36th ACM SIGPLAN -SIGACT Symposium on Principles of Programming Languages (POPL'09)

S. Z. Béguelin, B. Grégoire, G. Barthe, and F. Olmedo, Formally certifying the security of digital signature schemes, 30th IEEE Symposium on Security and Privacy, pp.237-250, 2009.

M. Bellare, New proofs for NMAC and HMAC: Security without collision-resistance, CRYPTO'06, pp.602-619, 2006.
DOI : 10.1007/11818175_36
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.59

M. Bellare, J. Kilian, and P. Rogaway, The Security of the Cipher Block Chaining Message Authentication Code, Journal of Computer and System Sciences, vol.61, issue.3, pp.362-399, 2000.
DOI : 10.1006/jcss.1999.1694

M. Bellare and P. Rogaway, Random oracles are practical, Proceedings of the 1st ACM conference on Computer and communications security , CCS '93, pp.62-73, 1993.
DOI : 10.1145/168588.168596

J. Bengtson, K. Bhargavan, C. Fournet, A. Gordon, and S. Maffeis, Refinement types for secure implementations, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, 2011.
DOI : 10.1109/csf.2008.27
URL : https://hal.archives-ouvertes.fr/hal-01294973

K. Bhargavan, B. Blanchet, and N. Kobeissi, Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate, 2017 IEEE Symposium on Security and Privacy (SP), 2017.
DOI : 10.1109/SP.2017.26
URL : https://hal.archives-ouvertes.fr/hal-01575920

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

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with Verified Cryptographic Security, 2013 IEEE Symposium on Security and Privacy, pp.445-462, 2013.
DOI : 10.1109/SP.2013.37
URL : https://hal.archives-ouvertes.fr/hal-00863373

B. Blanchet, Proverif users

B. Blanchet, A. D. Jaggard, A. Scedrov, and J. 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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.216.7091

D. Boneh, E. Shen, and B. Waters, Strongly unforgeable signatures based on computational Diffie-Hellman, " in Public Key Cryptography -PKC, pp.229-240, 2006.
DOI : 10.1007/11745853_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.363.2693

D. Cadé and B. Blanchet, From computationally-proved protocol specifications to implementations and application to SSH, Ubiquitous Computing, and Dependable Applications (JoWUA), pp.4-31, 2013.

L. Chen and Q. Tang, Bilateral unknown key-share attacks in key agreement protocols, Journal of Universal Computer Science, vol.14, issue.3, pp.416-440, 2008.

C. J. Cremers, Unbounded verification, falsification, and characterization of security protocols by pattern refinement, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08
DOI : 10.1145/1455770.1455787

I. B. Damgård, A Design Principle for Hash Functions, Advances in Cryptology?CRYPTO89 Proceedings, ser. LNCS, G. Brassard, pp.416-427, 1989.
DOI : 10.1007/0-387-34805-0_39

W. Diffie, P. C. Van-oorschot, and M. J. Wiener, Authentication and authenticated key exchanges, Designs, Codes and Cryptography, pp.107-125, 1992.
DOI : 10.1007/BF00124891
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.216.6107

D. Dolev and A. C. 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

T. Frosch, C. Mainka, C. Bader, F. Bergsma, J. Schwenk et al., How Secure is TextSecure?, 2016 IEEE European Symposium on Security and Privacy (EuroS&P), pp.457-472, 2016.
DOI : 10.1109/EuroSP.2016.41
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.689.6003

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, pp.281-308, 1988.
DOI : 10.1137/0217017
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.8353

N. Kobeissi, K. Bhargavan, and B. Blanchet, Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach, 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pp.435-450, 2017.
DOI : 10.1109/EuroSP.2017.38

G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, " in Tools and Algorithms for the Construction and Analysis of Systems, ser, LNCS, vol.1055, pp.147-166, 1996.

M. Luby and C. Rackoff, How to Construct Pseudorandom Permutations from Pseudorandom Functions, SIAM Journal on Computing, vol.17, issue.2, pp.373-386, 1988.
DOI : 10.1137/0217022

R. M. Needham and M. D. 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

T. Okamoto and D. Pointcheval, The Gap-Problems: A New Class of Problems for the Security of Cryptographic Schemes, International Workshop on Practice and Theory in Public Key Cryptography (PKC'2001), pp.104-118, 1992.
DOI : 10.1007/3-540-44586-2_8

A. Pironti, P. Strub, and K. Bhargavan, Identifying website users by TLS traffic analysis: New attacks and effective countermeasures, INRIA Paris Rocquencourt, Tech. Rep, vol.8067, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00732449

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties, 2012 IEEE 25th Computer Security Foundations Symposium, pp.78-94, 2012.
DOI : 10.1109/CSF.2012.25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.8368

J. Tsay and S. F. Mjølsnes, A Vulnerability in the UMTS and LTE Authentication and Key Agreement Protocols, Computer Network Security (MMM-ACNS'12), ser, pp.65-76, 2012.
DOI : 10.1007/978-3-642-33704-8_6

P. Wuille, Dealing with malleability, " https://github.com/bitcoin/bips/ blob/master/bip-0062.mediawiki, 2014.

A. C. Yao, Theory and application of trapdoor functions, 23rd Annual Symposium on Foundations of Computer Science (sfcs 1982)
DOI : 10.1109/SFCS.1982.45