M. Abadi and P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), First IFIP International Conference on Theoretical Computer Science, pp.3-22, 2000.

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, pp.331-340, 2011.
DOI : 10.1145/2046707.2046745

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
DOI : 10.1145/2382196.2382271

M. R. Albrecht, K. G. Paterson, and G. J. Watson, Plaintext Recovery Attacks against SSH, 2009 30th IEEE Symposium on Security and Privacy, pp.16-26, 2009.
DOI : 10.1109/SP.2009.5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.216.9854

M. Avalle, A. Pironti, R. Sisto, and D. Pozza, The JavaSPI framework for security protocol implementation, ARES'11, pp.746-751, 2011.

M. Backes, D. Hofheinz, and D. Unruh, CoSP, Proceedings of the 16th ACM conference on Computer and communications security, CCS '09, pp.66-78, 2009.
DOI : 10.1145/1653662.1653672

G. Barthe, B. Grégoire, and S. Zanella, Formal certification of code-based cryptographic proofs, POPL'09, pp.90-101, 2009.

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

M. Bellare, T. Kohno, and C. Namprempre, Authenticated encryption in SSH, Proceedings of the 9th ACM conference on Computer and communications security , CCS '02, pp.1-11, 2002.
DOI : 10.1145/586110.586112

M. Bellare, T. Kohno, and C. Namprempre, The secure shell (SSH) transport layer encryption modes, 2006.
DOI : 10.17487/rfc4344

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

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, and A. Gordon, Modular verification of security protocol code by typing, POPL'10, pp.445-456, 2010.

K. Bhargavan, C. Fournet, A. Gordon, and S. Tse, Verified interoperable implementations of security protocols, ACM TOPLAS, vol.31, issue.1, 2008.

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 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, Using Horn clauses for analyzing security protocols, Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pp.86-111, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01110425

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

D. Cadé and B. Blanchet, From Computationally-proved Protocol Specifications to Implementations, 2012 Seventh International Conference on Availability, Reliability and Security, pp.65-74, 2012.
DOI : 10.1109/ARES.2012.63

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.

D. Cadé and B. Blanchet, Proved Generation of Implementations from Computationally Secure Protocol Specifications, 2nd Conference on Principles of Security and Trust, pp.63-82, 2013.
DOI : 10.1007/978-3-642-36830-1_4

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.151.293

H. Comon-lundh and V. Cortier, Computational soundness of observational equivalence, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, pp.109-118, 2008.
DOI : 10.1145/1455770.1455786
URL : https://hal.archives-ouvertes.fr/inria-00323199

V. Cortier, H. Hördegen, and B. Warinschi, Explicit Randomness is not Necessary when Modeling Probabilistic Encryption, ICS'06, pp.49-65, 2006.
DOI : 10.1016/j.entcs.2006.11.044
URL : https://hal.archives-ouvertes.fr/inria-00078825

V. Cortier and B. Warinschi, Computationally Sound, Automated Proofs for Security Protocols, ESOP'05, pp.157-171, 2005.
DOI : 10.1007/978-3-540-31987-0_12
URL : https://hal.archives-ouvertes.fr/inria-00000556

J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech, Automated proofs for asymmetric encryption, Concurrency, Compositionality, and Correctness, pp.300-321, 2010.
DOI : 10.1007/978-3-642-11512-7_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2052

J. F. Cas and . Cremers, Scyther -Semantics and Verification of Security Protocols, 2006.

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.

F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann, Guiding a general-purpose C verifier to prove cryptographic protocols, CSF'11, pp.3-17, 2011.

C. Fournet, M. Kohlweiss, and P. Strub, Modular codebased cryptographic verification, CCS'11, pp.341-350, 2011.
DOI : 10.1145/2046707.2046746
URL : https://hal.archives-ouvertes.fr/inria-00614372

J. Goubault-larrecq and F. Parrennes, Cryptographic Protocol Analysis on Real C Code, VMCAI'05, pp.363-379, 2005.
DOI : 10.1007/978-3-540-30579-8_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.2108

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

T. Kivinen and M. Kojo, More modular exponential (MODP) Diffie-Hellman groups for Internet Key Exchange (IKE), RFC, vol.3526, 2003.
DOI : 10.17487/rfc3526

G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, TACAS'96, pp.147-166
DOI : 10.1007/3-540-61042-1_43

A. J. Menezes, P. C. Van-oorschot, and S. A. Vanstone, Handbook of Applied Cryptography, 1996.
DOI : 10.1201/9781439821916

G. Milicia, ?-spaces: Programming security protocols, NWPT'02, 2002.

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

O. Nicholas and . Shea, Using Elyjah to analyse Java implementations of cryptographic protocols, FCS-ARSPA-WITS'08, 2008.

S. Owens, A Sound Semantics for OCaml light, LNCS, vol.4960, issue.08, pp.1-15, 2008.
DOI : 10.1007/978-3-540-78739-6_1

G. Kenneth, G. J. Paterson, and . Watson, Plaintext-dependent decryption: A formal security treatment of SSH-CTR, Eurocrypt, pp.345-361095, 2010.

A. Pironti and R. Sisto, An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation, 2007 IEEE Symposium on Computers and Communications, pp.839-844, 2007.
DOI : 10.1109/ISCC.2007.4381508

A. Pironti and R. Sisto, Provably correct Java implementations of Spi Calculus security protocols specifications, Computers & Security, vol.29, issue.3, pp.302-314, 2010.
DOI : 10.1016/j.cose.2009.08.001

E. Poll and A. Schubert, Verifying an implementation of SSH, WITS'07, 2007.

D. Pozza, R. Sisto, and L. Durante, Spi2Java: automatic cryptographic protocol Java code generation from SPI calculus, 18th International Conference on Advanced Information Networking and Applications, 2004. AINA 2004., pp.400-405, 2004.
DOI : 10.1109/AINA.2004.1283943
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.563.2347

D. Song, A. Perrig, and D. Phan, AGVI ??? Automatic Generation, Verification, and Implementation of Security Protocols, CAV'01, pp.241-245, 2001.
DOI : 10.1007/3-540-44585-4_21

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

B. Warinschi, A computational analysis of the Needham-Schroeder(Lowe ) protocol, 16th Computer Security Foundations Workshop (CSFW'03), pp.248-262, 2003.

T. Ylönen, RFC 4251: The Secure Shell (SSH) Protocol Architecture, 2006.

T. Ylönen and . Rfc, The Secure Shell (SSH) Authentication Protocol, 2006.
DOI : 10.17487/rfc4252

T. Ylönen, RFC 4253: The Secure Shell (SSH) Transport Layer Protocol, 2006.

T. Ylönen and . Rfc, The Secure Shell (SSH) Connection Protocol, 2006.
DOI : 10.17487/rfc4254