M. Abadi and P. Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)*, Journal of Cryptology, vol.15, issue.2, pp.103-127, 2002.
DOI : 10.1007/s00145-001-0014-7

M. Abdalla, P. Fouque, and D. Pointcheval, Password-based authenticated key exchange in the threeparty setting, IEE Proceedings Information Security, pp.27-39, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00918401

P. Adão, G. Bana, J. Herzog, and A. Scedrov, Soundness of formal encryption in the presence of keycycles, ESORICS 2005, pp.374-396, 2005.

R. Affeldt, D. Nowak, and K. Yamada, Certifying assembly with formal cryptographic proofs: the case of BBS, AVoCS'09, 2009.

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

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

M. Backes and P. Laud, Computationally sound secrecy proofs by mechanized flow analysis, Proceedings of the 13th ACM conference on Computer and communications security , CCS '06, pp.370-379, 2006.
DOI : 10.1145/1180405.1180450
URL : https://hal.archives-ouvertes.fr/inria-00080498

M. Backes, M. Maffei, and D. Unruh, Computationally sound verification of source code, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.387-398, 2010.
DOI : 10.1145/1866307.1866351

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 and B. Pfitzmann, Relating Symbolic and Cryptographic Secrecy, IEEE Transactions on Dependable and Secure Computing, vol.2, issue.2, pp.109-123, 2005.
DOI : 10.1109/TDSC.2005.25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.8373

M. Backes, B. Pfitzmann, and M. Waidner, A composable cryptographic library with nested operations, Proceedings of the 10th ACM conference on Computer and communication security , CCS '03, pp.220-230, 2003.
DOI : 10.1145/948109.948140

G. Barthe, M. Daubignard, B. Kapron, and Y. Lakhnech, Computational indistinguishability logic, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.375-386, 2010.
DOI : 10.1145/1866307.1866350
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.174.7136

G. Barthe, B. Grégoire, S. Z. Béguelin, and Y. Lakhnech, Beyond Provable Security Verifiable IND-CCA Security of OAEP, CT-RSA 2011, pp.180-196, 2011.
DOI : 10.1109/SP.2009.17
URL : https://hal.archives-ouvertes.fr/hal-01112084

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, 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, POPL'09, pp.90-101, 2009.

S. Z. Béguelin, G. Barthe, S. Heraud, B. Grégoire, and D. Hedin, A machine-checked formalization of sigma-protocols, CSF'10, pp.246-260, 2010.

M. Bellare and C. Namprempre, Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, Advances in Cryptology ? ASIACRYPT'00, pp.531-545, 1976.

M. Bellare and P. Rogaway, The security of triple encryption and a framework for code-based gameplaying proofs, LNCS, vol.4004331, pp.409-426, 2004.

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

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, Automatic proof of strong secrecy for security protocols, IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, pp.86-100, 2004.
DOI : 10.1109/SECPRI.2004.1301317

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions Extended version available as ePrint Report, CSF'07, pp.97-111, 2007.

B. Blanchet, A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing, vol.5401, issue.4, pp.193-207, 2005.
DOI : 10.1109/sp.2006.1

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

B. Blanchet and D. Pointcheval, Automated Security Proofs with Sequences of Games, CRYPTO 2006, pp.537-554, 2006.
DOI : 10.1007/11818175_32

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

R. Canetti, Universally composable security: A new paradigm for cryptographic protocols An updated version is available at Cryptology ePrint Archive, FOCS'01, pp.136-145067, 2000.

R. Canetti and J. Herzog, Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols, TCC'06, pp.380-403, 2004.
DOI : 10.1007/11681878_20

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 2006, 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, Towards automated proofs for asymmetric encryption schemes in the random oracle model, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, pp.371-380, 2008.
DOI : 10.1145/1455770.1455817

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. Courant, C. Ene, and Y. Lakhnech, Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption, FSTTCS'07, pp.364-375, 2007.
DOI : 10.1007/978-3-540-77050-3_30

A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani, Probabilistic Polynomial-Time Semantics for a Protocol Security Logic, ICALP'05, pp.16-29, 2005.
DOI : 10.1007/11523468_2
URL : https://hal.archives-ouvertes.fr/inria-00103654

A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols, 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.321-334, 2006.
DOI : 10.1109/CSFW.2006.9

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.

S. Halevi, A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report, vol.181, p.181, 2005.

R. Janvier, Y. Lakhnech, and L. Mazaré, Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries, ESOP'05, pp.172-185, 2005.
DOI : 10.1007/978-3-540-31987-0_13

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

P. Laud, Handling Encryption in an Analysis for Secure Information Flow, ESOP'03, pp.159-173, 2003.
DOI : 10.1007/3-540-36575-3_12

P. Laud, Symmetric encryption in automatic analyses for confidentiality against active adversaries, IEEE Symposium on Security and Privacy, pp.71-85, 2004.

P. Laud, Secrecy types for a simulatable cryptographic library, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, pp.26-35, 2005.
DOI : 10.1145/1102120.1102126

P. Laud and I. T?ahhirov, A User Interface for a Game-Based Protocol Verification Tool, FAST2009, pp.263-278, 2009.
DOI : 10.1007/978-3-642-12459-4_19

P. Laud and V. Vene, A Type System for Computationally Secure Information Flow, FCT'05, pp.365-377, 2005.
DOI : 10.1007/11537311_32

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

D. Micciancio and B. Warinschi, Soundness of Formal Encryption in the Presence of Active Adversaries, TCC'04, pp.133-151, 2004.
DOI : 10.1007/978-3-540-24638-1_8

J. C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague, A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols, Electronic Notes in Theoretical Computer Science, vol.45, pp.1-3118, 2006.
DOI : 10.1016/S1571-0661(04)80968-X

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

D. Nowak, A Framework for Game-Based Security Proofs, LNCS, vol.4861, pp.319-333, 2007.
DOI : 10.1007/978-3-540-77048-0_25

D. Nowak, On Formal Verification of Arithmetic-Based Cryptographic Primitives, LNCS, vol.28, issue.2, pp.368-382, 2008.
DOI : 10.1109/SFCS.1982.45

V. Shoup, Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report, vol.332332, 2004.

G. Smith and R. Alpízar, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security , FMSE '06, pp.33-43, 2006.
DOI : 10.1145/1180337.1180341

C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, and M. Waidner, Cryptographically Sound Theorem Proving, 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.153-166, 2006.
DOI : 10.1109/CSFW.2006.10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.4064

I. T?ahhirov and P. Laud, Application of Dependency Graphs to Security Protocol Analysis, TGC'07, pp.294-311, 2007.
DOI : 10.1007/978-3-540-78663-4_20

T. Y. Woo and S. S. Lam, A semantic model for authentication protocols, Proceedings 1993 IEEE Computer Society Symposium on Research in Security and Privacy, pp.178-194, 1993.
DOI : 10.1109/RISP.1993.287633