B. Chor and R. L. Rivest, A knapsack-type public key cryptosystem based on arithmetic in finite fields, CRYPTO'84, ser. LNCS, pp.54-65, 1985.
DOI : 10.1109/18.21214

H. W. Lenstra-jr, On the Chor?Rivest knapsack cryptosystem, Journal of Cryptology, vol.3, issue.3, pp.149-155, 1991.
DOI : 10.1007/BF00196908

S. Vaudenay, Cryptanalysis of the Chor-Rivest cryptosystem, CRYPTO'98, ser. LNCS, pp.243-256, 1998.

M. Bellare and P. Rogaway, The Exact Security of Digital Signatures-How to Sign with RSA and Rabin, EURO- CRYPT'96, ser. LNCS, pp.399-416, 1996.
DOI : 10.1007/3-540-68339-9_34

K. Ohta and T. Okamoto, On concrete security treatment of signatures derived from identification, CRYPTO'98, ser, pp.354-369, 1998.
DOI : 10.1007/BFb0055741

M. Bellare and P. Rogaway, Optimal asymmetric encryption, EUROCRYPT'94, ser. LNCS, pp.92-111, 1994.
DOI : 10.1007/BFb0053428

V. Shoup, OAEP Reconsidered, Journal of Cryptology, vol.15, issue.4, pp.223-249, 2002.
DOI : 10.1007/s00145-002-0133-9

E. Fujisaki, T. Okamoto, D. Pointcheval, and J. Stern, RSA-OAEP Is Secure under the RSA Assumption, Journal of Cryptology, vol.17, issue.2, pp.81-104, 2004.
DOI : 10.1007/s00145-002-0204-y

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

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

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

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

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

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

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

V. Cortier and B. Warinschi, A composable computational soundness notion, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, pp.63-74, 2011.
DOI : 10.1145/2046707.2046717
URL : https://hal.archives-ouvertes.fr/inria-00638552

V. Cortier, S. Kremer, and B. Warinschi, A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems, Journal of Automated Reasoning, vol.13, issue.1, pp.3-4, 2011.
DOI : 10.1007/s10817-010-9187-9
URL : https://hal.archives-ouvertes.fr/inria-00525776

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

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

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

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

C. Sprenger and D. Basin, Cryptographically-sound protocol-model abstractions, LICS'08, pp.3-17, 2008.
DOI : 10.1109/csf.2008.19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.323.6473

R. Canetti, Universally composable security: a new paradigm for cryptographic protocols, Proceedings 2001 IEEE International Conference on Cluster Computing, pp.136-145, 2001.
DOI : 10.1109/SFCS.2001.959888

R. Canetti and J. Herzog, Universally composable symbolic analysis of cryptographic protocols (the case of encryptionbased mutual authentication and key exchange), Cryptology ePrint Archive, 2004.

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

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-3, 2006.
DOI : 10.1016/S1571-0661(04)80968-X

D. Nowak and Y. Zhang, A Calculus for Game-Based Security Proofs, ProvSec 2010, ser, pp.35-52, 2010.
DOI : 10.1007/978-3-642-02273-9_29

A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani, Probabilistic Polynomial-Time Semantics for a Protocol Security Logic, ICALP'05, ser. LNCS, 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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.5001

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

R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Linch et al., Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols, DISC'06, ser. LNCS, pp.238-253, 2006.
DOI : 10.1007/11864219_17

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 V. Vene, A Type System for Computationally Secure Information Flow, FCT'05, ser, pp.365-377, 2005.
DOI : 10.1007/11537311_32

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

J. Courant, C. Ene, and Y. Lakhnech, Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption, FSTTCS'07, ser. LNCS, pp.364-375, 2007.
DOI : 10.1007/978-3-540-77050-3_30

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

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

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

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt, FAST 2008, ser. LNCS, pp.1-19, 2009.

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.

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

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

M. Bellare and P. Rogaway, The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, EUROCRYPT 2006, ser. LNCS, pp.409-426, 2006.
DOI : 10.1007/11761679_25

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, CRYPTO 2011, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

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

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

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

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

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

P. Laud and I. T?ahhirov, A user interface for a gamebased protocol verification tool, FAST2009, ser, pp.263-278, 2009.

E. Bresson, O. Chevassut, and D. Pointcheval, Security proofs for an efficient password-based key exchange, Proceedings of the 10th ACM conference on Computer and communication security , CCS '03, pp.241-250, 2003.
DOI : 10.1145/948109.948142

S. M. Bellovin and M. Merritt, Encrypted key exchange: password-based protocols secure against dictionary attacks, Proceedings 1992 IEEE Computer Society Symposium on Research in Security and Privacy, pp.72-84, 1992.
DOI : 10.1109/RISP.1992.213269
URL : http://academiccommons.columbia.edu/download/fedora_content/download/ac:127104/CONTENT/neke.pdf

B. Blanchet, Automatically Verified Mechanized Proof of One-Encryption Key Exchange, 2012 IEEE 25th Computer Security Foundations Symposium, p.2012
DOI : 10.1109/CSF.2012.8
URL : https://hal.archives-ouvertes.fr/hal-00863386

M. Bellare and P. Rogaway, The AuthA protocol for password-based authenticated key exchange, 1363.

M. Bellare, D. Pointcheval, and P. Rogaway, Authenticated Key Exchange Secure against Dictionary Attacks, EURO- CRYPT 2000, ser. LNCS, pp.139-155, 2000.
DOI : 10.1007/3-540-45539-6_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.5384

J. Coron, Security Proof for Partial-Domain Hash Signature Schemes, CRYPTO 2002, ser, pp.613-626, 2002.
DOI : 10.1007/3-540-45708-9_39
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.6371

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

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

M. Abdalla, P. Fouque, and D. Pointcheval, Password-based authenticated key exchange in the three-party setting, IEE Proceedings - Information Security, vol.153, issue.1, pp.27-39, 2006.
DOI : 10.1049/ip-ifs:20055073
URL : https://hal.archives-ouvertes.fr/hal-00918401