[. Adão, G. Bana, J. Herzog, and A. Scedrov, Soundness of Formal Encryption in the Presence of Key-Cycles, Proc. 10th European Symposium on Research in Computer Security (ESORICS'05), pp.374-396, 2005.
DOI : 10.1007/11555827_22

[. Adão, G. Bana, and A. Scedrov, Computational and Information-Theoretic Soundness and Completeness of Formal Encryption, 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp.170-184, 2005.
DOI : 10.1109/CSFW.2005.13

[. Abadi, M. Baudet, and B. Warinschi, Guessing Attacks and the Computational Soundness of Static Equivalence
DOI : 10.1007/11690634_27

[. Abadi, R. Corin, and C. Fournet, Computational Secrecy by Typing for the Pi Calculus, Programming Languages and Systems, 4th Asian Symposium, pp.253-269, 2006.
DOI : 10.1007/11924661_16

P. Adão and C. Fournet, Cryptographically Sound Implementations for Communicating Processes, Automata, Languages and Programming, 33rd International Colloquium, pp.83-94, 2006.
DOI : 10.1007/11787006_8

[. Abadi and A. D. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.36-47, 1997.
DOI : 10.1145/266420.266432

[. Askarov, D. Hedin, and A. Sabelfeld, Cryptographically-masked flows Reconciling two views of cryptography (the computational soundness of formal encryption), Proc. 13th International Static Analysis Symposium (SAS'06) Proc. 1st IFIP International Conference on Theoretical Computer Science (IFIP?TCS'00), volume 1872 of LNCS, pp.353-369, 2000.

[. Abadi and P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption

M. Aw05a, B. Abadi, and . Warinschi, Password-based encryption analyzed, Proc. 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), pp.664-676, 2005.

M. Aw05b, B. Abadi, and . Warinschi, Security analysis of cryptographically controlled access to xml documents, Proc. 24th ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems (PODS'05), pp.108-117, 2005.

[. Abadi and B. Warinschi, Security analysis of cryptographically controlled access to XML documents, Journal of the ACM, vol.55, issue.2, pp.1-29, 2008.
DOI : 10.1145/1346330.1346331

I. Backes, A. D. Cervesato, A. Jaggard, J. Scedrov, and . Tsay, Cryptographically sound security proofs for basic and public-key kerberos, Proc. 11th European Symposium on Research in Computer Security(ESORICS'06), pp.362-383, 2006.

[. Baudet, V. Cortier, and S. Kremer, Computationally sound implementations of equational theories against passive adversaries, Proc. 32nd International Colloquium on Automata , Languages and Programming (ICALP'05), pp.652-663, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00426620

[. Baudet, V. Cortier, and S. Kremer, Computationally sound implementations of equational theories against passive adversaries, Information and Computation, vol.207, issue.4, pp.496-520, 2009.
DOI : 10.1016/j.ic.2008.12.005
URL : https://hal.archives-ouvertes.fr/inria-00426620

[. Barthe, J. Cederquist, and S. Tarento, A machinechecked formalization of the generic model and the random oracle model, Proc. 2nd International Joint Conference on Automated Reasoning, pp.385-399, 2004.

M. Backes and M. Duermuth, A Cryptographically Sound Dolev-Yao Style Security Proof of an Electronic Payment System, 18th IEEE Computer Security Foundations Workshop (CSFW'05)
DOI : 10.1109/CSFW.2005.5

[. Backes, M. Dürmuth, and R. Küsters, On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography, Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp.108-120, 2007.
DOI : 10.1007/978-3-540-77050-3_9

I. Boneh, S. Halevi, M. Hamburg, and R. Ostrovsky, Circular-Secure Encryption from Decision Diffie-Hellman, Advances in Cryptology -CRYPTO 2008, pp.108-125, 2008.
DOI : 10.1007/978-3-540-85174-5_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.121.4099

[. Backes, C. Jacobi, and B. Pfitzmann, Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation, International Symposium of Formal Methods Europe, pp.310-329, 2002.
DOI : 10.1007/3-540-45614-7_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.7064

[. 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

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

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, A computationally sound mechanized prover for security protocols, IEEE Symposium on Security and Privacy, pp.140-154, 2006.

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, 2007.
DOI : 10.1109/sp.2006.1

Y. Bresson, L. Lakhnech, B. Mazaré, and . Warinschi, A Generalization of DDH with Applications to Protocol Analysis and Computational Soundness, Advances in Cryptology -CRYPTO 2007, pp.482-499
DOI : 10.1007/978-3-540-74143-5_27

M. Backes, S. Moedersheim, B. Pfitzmann, and L. Vigano, Symbolic and cryptographic analysis of the secure wsreliablemessaging scenario, Proc. 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06), 2006.

G. Bana, P. Mohassel, and T. Stegers, Computational Soundness of Formal Indistinguishability and Static Equivalence, Proc. 11th Asian Computing Science Conference, pp.182-196, 2006.
DOI : 10.3233/JCS-2004-12105

[. Backes, M. Maffei, and D. Unruh, Zeroknowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol, Proceedings of 29th IEEE Symposium on Security and Privacy, 2008.

M. Backes and B. Pfitzmann, A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol

M. Backes and B. Pfitzmann, A Cryptographically Sound Security Proof of the Needham???Schroeder???Lowe Public-Key Protocol, IEEE Journal on Selected Areas in Communications, vol.22, issue.10, pp.2075-2086, 2004.
DOI : 10.1109/JSAC.2004.836016

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, Limits of the Cryptographic Realization of Dolev-Yao-Style XOR, Proc. 10th European Symposium on Research in Computer Security (ESORICS'05), pp.336-354, 2005.
DOI : 10.1007/11555827_11

M. Backes and B. Pfitzmann, Relating symbolic and computational secrecy, Transactions on Dependable and Secure Computing, pp.109-123, 2005.
DOI : 10.1109/sp.2005.17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.8373

M. Backes and B. Pfitzmann, On the Cryptographic Key Secrecy of the Strengthened Yahalom Protocol, Proc. 21st IFIP International Information Security Conference (SEC'06), 2006.
DOI : 10.1007/0-387-33406-8_20

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

[. Backes, B. Pfitzmann, and A. Scedrov, Keydependent message security under active attacks -BRSIM/UCsoundness of symbolic encryption with key cycles, Journal of Computer SecurityJCS), 2008.

[. 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, 2003.
DOI : 10.1145/948109.948140

[. Backes, B. Pfitzmann, and M. Waidner, Symmetric Authentication within a Simulatable Cryptographic Library, Proc. 8th European Symposium on Research in Computer Security (ESORICS'03), pp.271-290, 2003.
DOI : 10.1007/978-3-540-39650-5_16

[. Backes, B. Pfitzmann, and M. Waidner, Limits of the reactive simulatability/uc of Dolev-Yao models with hashes, Proceedings of 11th European Symposium on Research in Computer Security(ESORICS), pp.404-423

[. Backes, B. Pfitzmann, and M. Waidner, The reactive simulatability (RSIM) framework for asynchronous systems, Information and Computation, vol.205, issue.12, pp.1685-1720, 2007.
DOI : 10.1016/j.ic.2007.05.002

[. Black, P. Rogaway, and T. Shrimpton, Encryptionscheme security in the presence of key-dependent messages, In Selected Areas in Cryptography LNCS, vol.2595, pp.62-75, 2002.

M. Backes and D. Unruh, Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers, 2008 21st IEEE Computer Security Foundations Symposium, pp.255-269, 2008.
DOI : 10.1109/CSF.2008.20

[. Canetti, Universally composable security: A new paradigm for cryptographic protocols (extended abstract), Proc. 42nd IEEE Symposium on Foundations of Computer Science (FOCS'01), pp.136-147, 2001.

L. Canetti, D. Cheung, M. Kaynar, N. Liskov, O. Lynch et al., Time-bounded taskpioas: A framework for analyzing security protocols, Proceedings of the 20th International Symposium on Distributed Computing, pp.238-253, 2006.

M. Courant, P. Daubignard, Y. Lafourcade-cristian-ene, and . Lahknech, 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, 2008.
DOI : 10.1145/1455770.1455817

C. Courant, Y. Ene, and . Lakhnech, Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption, Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), pp.364-375, 2007.
DOI : 10.1007/978-3-540-77050-3_30

[. Canetti and J. Herzog, Universally composable symbolic analysis of mutual authentication and key-exchange protocols (extended abstract), Proc. 3rd Theory of Cryptography Conference, pp.380-403, 2006.

[. Cortier, H. Hördegen, and B. Warinschi, Explicit Randomness is not Necessary when Modeling Probabilistic Encryption, Workshop on Information and Computer Security, 2006.
DOI : 10.1016/j.entcs.2006.11.044
URL : https://hal.archives-ouvertes.fr/inria-00078825

[. Cortier, S. Kremer, R. Küsters, and B. Warinschi, Computationally Sound Symbolic Secrecy in the Presence of Hash Functions, Proceedings of the 26th Conference on Fundations of Software Technology and Theoretical Computer Science (FSTTCS'06), pp.176-187, 2006.
DOI : 10.1007/11944836_18
URL : https://hal.archives-ouvertes.fr/inria-00108386

V. Hubert-comon-lundh and . Cortier, Computational soundness of observational equivalence, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, 2008.
DOI : 10.1145/1455770.1455786

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

V. Cortier, Z. Eugen, and . Alinescu, Deciding Key Cycles for Security Protocols, Proc. of the 13th Int. Conference on Logic for Programming, pp.317-331, 2006.
DOI : 10.1007/11916277_22
URL : https://hal.archives-ouvertes.fr/inria-00181625

A. Datta, J. C. Derek, V. Mitchell, M. Shmatikov, and . Turuani, Probabilistic Polynomial-Time Semantics for a Protocol Security Logic, Proc. of 32nd International Colloquium on Automata, Languages and Programming, pp.16-29, 2005.
DOI : 10.1007/11523468_2
URL : https://hal.archives-ouvertes.fr/inria-00103654

[. Datta, A. Derek, J. C. Mitchell, and A. Roy, Protocol composition logic (PCL) In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, Electronic Notes in Theoretical Computer Science, 2007.

[. 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

[. Delaune, S. Kremer, and M. D. Ryan, Coercionresistance and receipt-freeness in electronic voting, Computer Security Foundations Workshop (CSFW'06), pp.28-39, 2006.

I. Fournet and T. Rezk, Cryptographically sound implementations for typed information-flow security, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pp.323-335, 2008.

[. Galindo, F. D. Garcia, and P. Van-rossum, Computational Soundness of Non-Malleable Commitments, Proc. 4th Information Security Practice and Experience Conference (ISPEC'08), 2008.
DOI : 10.1007/978-3-540-79104-1_26

[. Goldwasser, S. Micali, and R. L. 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

J. Groth and R. Ostrovsky, Cryptography in the multi-string model, Appears in Advances in Cryptology -CRYPTO 2007, pp.323-341, 2007.

[. Gupta and V. Shmatikov, Towards computationally sound symbolic analysis of key exchange protocols, Proceedings of the 2005 ACM workshop on Formal methods in security engineering , FMSE '05, pp.23-32, 2005.
DOI : 10.1145/1103576.1103580

[. Gupta and V. Shmatikov, Key confirmation and adaptive corruptions in the protocol security logic, Proc. of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), pp.113-142, 2006.

D. Flavio, P. Garcia, and . Van-rossum, Sound computational interpretation of symbolic hashes in the standard model, Proc. International Workshop on Security 2006 (IWSEC'06), pp.33-47, 2006.

D. Flavio, P. Garcia, and . Van-rossum, Sound and complete computational interpretation of symbolic hashes in the standard model, Theoretical Computer Science, vol.394, pp.112-133, 2008.

J. Herzog, A computational interpretation of Dolev???Yao adversaries, Proceedings of the 3rd IFIP WG1.7 Workshop on Issues in the Theory of Security, 2003.
DOI : 10.1016/j.tcs.2005.03.003

J. Herzog, A computational interpretation of Dolev???Yao adversaries, Theoretical Computer Science, vol.340, issue.1, pp.57-81, 2005.
DOI : 10.1016/j.tcs.2005.03.003

O. Horvitz and V. D. Gligor, Weak Key Authenticity and the Computational Completeness of Formal Encryption, Advances in Cryptology -CRYPTO 2003, pp.530-547
DOI : 10.1007/978-3-540-45146-4_31

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

[. Janvier, Y. Lakhnech, and L. Mazaré, Computational Soundness of Symbolic Analysis for Protocols Using Hash Functions, Proceedings of the Workshop on Information and Computer Security (ICS'06), 2006.
DOI : 10.1016/j.entcs.2007.01.066

[. Küsters, A. Datta, J. C. Mitchell, and A. Ramanathan, On the Relationships between Notions of??Simulation-Based Security, Journal of Cryptology, vol.353, issue.1???3, pp.145-153, 2008.
DOI : 10.1007/s00145-008-9019-9

S. Kremer and L. Mazaré, Adaptive Soundness of Static Equivalence, Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07), pp.610-625, 2007.
DOI : 10.1007/978-3-540-74835-9_40

S. Kremer and L. Mazaré, Computationally sound analysis of protocols using bilinear pairings, Journal of Computer Security, vol.18, issue.6, 2009.
DOI : 10.3233/JCS-2009-0388

R. Küsters and M. Tuengerthal, Joint state theorems for publickey encryption and digital signature functionalities with local computations, Computer Security Foundations (CSF'08), 2008.

[. Laud, Semantics and Program Analysis of Computationally Secure Information Flow, Proc. 10th European Symposium on Programming (ESOP'01), volume 2028 of LNCS, pp.77-91
DOI : 10.1007/3-540-45309-1_6

P. Laud, Encryption cycles and two views of cryptography, Nordic Workshop on Secure IT Systems (NORDSEC'02), 2002.

P. Laud, Handling Encryption in an Analysis for Secure Information Flow, Proc. 12th European Symposium on Programming, pp.159-173, 2003.
DOI : 10.1007/3-540-36575-3_12

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

P. Laud, On the computational soundness of cryptographically masked flows, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pp.337-348, 2008.

[. Laud and R. Corin, Sound Computational Interpretation of Formal Encryption with Composed Keys, Proc. 6th International Conference on Information Security and Cryptology (ICISC'03), volume 2971 of LNCS, pp.55-66, 2004.
DOI : 10.1007/978-3-540-24691-6_5

I. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov, A probabilistic poly-time framework for protocol analysis, Proceedings of the 5th ACM conference on Computer and communications security , CCS '98
DOI : 10.1145/288090.288117

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

[. Laud and I. Tsahhirov, Digital signature in automatic analyses for confidentiality against active adversaries, Nordic Workshop on Secure IT Systems (NORDSEC'05), pp.29-41, 2005.

[. Laud and V. Vene, A Type System for Computationally Secure Information Flow, Proc. 15th International Symposium on Fundamentals of Computation Theory (FCT'05), pp.365-377, 2005.
DOI : 10.1007/11537311_32

[. Mazaré, Computationally sound analysis of protocols using bilinear pairings, Proc. 7th International Workshop on Issues in the Theory of Security (WITS'07), pp.6-21, 2007.

D. Micciancio and S. Panjwani, Adaptive Security of Symbolic Encryption, Proc. 2nd Theory of Cryptography Conference (TCC'05), pp.169-187, 2005.
DOI : 10.1007/978-3-540-30576-7_10

J. C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague, A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols, Proc. 17th Annual Conference on the Mathematical Foundations of Programming Semantics, 2001.
DOI : 10.1016/S1571-0661(04)80968-X

G. Miklau and D. Suciu, Controlling Access to Published Data Using Cryptography, VLDB '2003: Proceedings of the 29th international conference on Very large data bases, pp.898-909, 2003.
DOI : 10.1016/B978-012722442-8/50084-7

D. Micciancio and B. Warinschi, Completeness theorems for the abadi-rogaway logic of encrypted expressions, Proceedings of the 2nd IFIP WG1.7 Workshop on Issues in the Theory of Security (WITS'02), 2002.

D. Micciancio and B. Warinschi, Completeness theorems for the Abadi???Rogaway language of encrypted expressions1, Journal of Computer Security, vol.12, issue.1, pp.99-129, 2004.
DOI : 10.3233/JCS-2004-12105

D. Micciancio and B. Warinschi, Soundness of Formal Encryption in the Presence of Active Adversaries, Proc. 1st Theory of Cryptography Conference, pp.133-151, 2004.
DOI : 10.1007/978-3-540-24638-1_8

[. Roy, A. Datta, A. Derek, and J. C. Mitchell, Inductive Proofs of Computational Secrecy, Proceedings of the 12th European Symposium on Research in Computer Security (ES- ORICS'07), pp.219-234, 2007.
DOI : 10.1007/978-3-540-74835-9_15

A. Roy, A. Datta, and J. C. Mitchell, Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols, Revised Selected Papers from the 3rd Symposium on Trustworthy Global Computing, 2008.
DOI : 10.1007/978-3-540-78663-4_21

[. Ramanathan, J. C. Mitchell, A. Scedrov, and V. Teague, Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols, Proc. 7th International Conference on Foundations of Software Science and Computation Structures, pp.468-483
DOI : 10.1007/978-3-540-24727-2_33

[. Ramanathan, J. C. Mitchell, A. Scedrov, and V. Teague, A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols, Theoretical Computer Science, vol.353, pp.118-164, 2006.

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-44, 2006.
DOI : 10.1145/1180337.1180341

C. Sprenger and D. Basin, Cryptographically-sound protocol-model abstractions, Logic in Computer Science (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

C. Sprenger and D. Basin, Cryptographically-sound protocol-model abstractions, Computer Security Foundations (CSF 08), pp.115-129, 2008.
DOI : 10.1109/csf.2008.19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.323.6473

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

[. Tarento, Machine-Checked Security Proofs of Cryptographic Signature Schemes, Proc. 10th European Symposium on Research in Computer Security (ESORICS'05), pp.140-158, 2005.
DOI : 10.1007/11555827_9

[. Warinschi, A computational analysis of the Needham???Schroeder???(Lowe) protocol, Journal of Computer Security, vol.13, issue.3, pp.565-591, 2005.
DOI : 10.3233/JCS-2005-13307