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

8. Arinc-specification, Datalink security, part 1 ? ACARS message security Available for sale at http://aviation-ia, 2007.

A. Armando, The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Computer Aided Verification, 17th International Conference, CAV 2005, 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.1007/978-3-642-22792-9_5

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, Computer-Aided 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), pp.90-101, 2009.
DOI : 10.1145/1480881.1480894

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.330.771

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, LNCS, vol.4117, issue.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.1145/1890028.1890031

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, IEEE Symposium on Security and Privacy (S&P'17)
DOI : 10.1007/11841197_6

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.61.3389

K. Bhargavan, R. Corin, C. Fournet, and E. Z?linescu, 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 Available at http://prosecco.inria.fr/personal/ bblanche/proverif/proverif-users

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions Extended version available as ePrint Report, 20th IEEE Computer Security Foundations Symposium (CSF'07), pp.97-111, 2007.

B. Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008.
DOI : 10.1109/TDSC.2007.1005

B. Blanchet, Automatic verification of correspondences for security protocols*, Journal of Computer Security, vol.17, issue.4, pp.363-434, 2009.
DOI : 10.3233/JCS-2009-0339

B. Blanchet, Automatically Verified Mechanized Proof of One-Encryption Key Exchange, 2012 IEEE 25th Computer Security Foundations Symposium, pp.325-339, 2012.
DOI : 10.1109/CSF.2012.8

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

B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends in Privacy and Security, pp.1-135, 2016.
DOI : 10.1561/3300000004

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

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, Public Key Cryptography -PKC 2006, 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, Journal of Wireless Mobile Networks, 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.

J. Coron, Y. Dodis, C. Malinaud, and P. Puniya, Merkle-Damg??rd Revisited: How to Construct a Hash Function, Advances in Cryptology?CRYPTO 2005, pp.430-448, 2005.
DOI : 10.1007/11535218_26

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.365.1590

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, pp.119-128, 2008.
DOI : 10.1145/1455770.1455787

I. B. Damgård, A Design Principle for Hash Functions, Advances in Cryptology?CRYPTO'89 Proceedings, 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, IT, issue.12, pp.29198-208, 1983.

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, 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pp.435-450, 2017.

G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.1055, pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6385

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

N. Sp, 38A: Recommendation for block cipher modes of operation, methods and techniques, 2001.

N. Fips, The keyed-hash message authentication code (HMAC) Available at http://csrc.nist.gov/publications/fips/fips198/fips-198a.pdf, 2008.

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 Available at https, 2012.

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), 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), pp.80-91, 1982.
DOI : 10.1109/SFCS.1982.45