article

A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

Authors:

Véronique Cortier,

Bogdan WarinschiAuthors Info & Claims

Journal of Automated Reasoning, Volume 46, Issue 3-4

Pages 225 - 259

https://doi.org/10.1007/s10817-010-9187-9

Published: 01 April 2011 Publication History

Abstract

Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers with respect to the more detailed computational models have been quite unclear. For more than 20 years the two approaches have coexisted but evolved mostly independently. Recently, significant research efforts attempt to develop paradigms for cryptographic systems analysis that combines the best of both worlds. There are two broad directions that have been followed. Computational soundness aims to establish sufficient conditions under which results obtained using symbolic models imply security under computational models. The direct approach aims to apply the principles and the techniques developed in the context of symbolic models directly to computational ones. In this paper we survey existing results along both of these directions. Our goal is to provide a rather complete summary that could act as a quick reference for researchers who want to contribute to the field, want to make use of existing results, or just want to get a better picture of what results already exist.

References

[1]

Ad&#227;o, P., Bana, G., Herzog, J., Scedrov, A.: Soundness of formal encryption in the presence of key-cycles. In: Proc. 10th European Symposium on Research in Computer Security (ESORICS'05). LNCS, vol. 3679, pp. 374-396 (2005).

Digital Library

[2]

Ad&#227;o, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. In: Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp. 170-184 (2005).

Digital Library

[3]

Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. In: Proc. 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06). LNCS, vol. 3921 (2006).

Digital Library

[4]

Abadi, M., Corin, R., Fournet, C.: Computational secrecy by typing for the pi calculus. In: Programming Languages and Systems, 4th Asian Symposium, (APLAS'06), vol. 4279 of LNCS, pp. 253-269. Springer (2006).

Digital Library

[5]

Ad&#227;o, P., Fournet, C.: Cryptographically sound implementations for communicating processes. In: Automata, Languages and Programming, 33rd International Colloquium (ICALP'06). LNCS, vol. 4052, pp. 83-94. Springer, Heidelberg (2006).

Digital Library

[6]

Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. In: Proc. of the 4th ACM Conference on Computer and Communications Security (CCS'97), pp. 36-47. ACM, New York (1997).

Digital Library

[7]

Askarov, A., Hedin, D., Sabelfeld A.: Cryptographically-masked flows. In: Proc. 13th International Static Analysis Symposium (SAS'06). LNCS, vol. 4134, pp. 353-369 (2006).

Digital Library

[8]

Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). In: Proc. 1st IFIP International Conference on Theoretical Computer Science (IFIP-TCS'00). LNCS, vol. 1872, pp. 3-22 (2000).

Digital Library

[9]

Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 15(2), 103-127 (2002).

Digital Library

[10]

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

Digital Library

[11]

Abadi, M., Warinschi, B.: Security analysis of cryptographically controlled access to xml documents. In: Proc. 24th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS'05), pp. 108-117. ACM, New York (2005).

Digital Library

[12]

Abadi, M., Warinschi, B.: Security analysis of cryptographically controlled access to xml documents. J. ACM 55(2), 1-29 (2008).

Digital Library

[13]

Backes, M.: A cryptographically sound Dolev-Yao style security proof of the Otway-Rees protocol. In: Proc. 9th European Symposium on Research in Computer Security (ESORICS'04). LNCS, vol. 3193, pp. 89-108 (2004).

[14]

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

Digital Library

[15]

Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Proc. 32nd International Colloquium on Automata, Languages and Programming (ICALP'05). LNCS, vol. 3580, pp. 652-663. Springer, Heidelberg (2005).

Digital Library

[16]

Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. Inf. Comput. 207(4), 496-520 (2009).

Digital Library

[17]

Barthe, G., Cederquist, J., Tarento, S.: A machine-checked formalization of the generic model and the random oracle model. In: Proc. 2nd International Joint Conference on Automated Reasoning (IJCAR'04). Lecture Notes in Artificial Intelligence, vol. 3097, pp. 385-399. Springer, Heidelberg (2004).

[18]

Backes, M., Duermuth, M.: A cryptographically sound Dolev-Yao style security proof of an electronic payment system. In: Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp. 78-93 (2005).

Digital Library

[19]

Backes, M., D&#252;rmuth, M., K&#252;sters, R.: On simulatability soundness and mapping soundness of symbolic cryptography. In: Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07). LNCS, vol. 4855, pp. 108-120. Springer, New Delhi (2007).

Digital Library

[20]

Boneh, D., Halevi, S., Hamburg, M., Ostrovsky, R.: Circular-secure encryption from decision Diffie-Hellman. In: Advances in Cryptology - CRYPTO 2008. LNCS, vol. 5157, pp. 108-125. Springer, Heidelberg (2008).

Digital Library

[21]

Backes, M., Jacobi, C., Pfitzmann, B.: Deriving cryptographically sound implementations using composition and formally verified bisimulation. In: International Symposium of Formal Methods Europe. LNCS, vol. 2381, pp. 310-329 (2002).

Digital Library

[22]

Blanchet, B., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Computationally sound mechanized proofs for basic and public-key kerberos. In: ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pp. 87-99. ACM, Tokyo (2008).

Digital Library

[23]

Backes, M., Laud, P.: Computationally sound secrecy proofs by mechanized flow analysis. In: Proc. 13th ACM Conference on Computer and Communications Security (CCS'06), pp. 370-379. Alexandria, VA, USA (2006).

Digital Library

[24]

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. of the 14th Computer Security Foundations Workshop (CSFW'01), pp. 82-96. IEEE Computer Society Press (2001).

Digital Library

[25]

Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140-154. IEEE Computer Society Press, Oakland (2006).

Digital Library

[26]

Blanchet, B.: Computationally sound mechanized proofs of correspondence assertions. In: 20th IEEE Computer Security Foundations Symposium (CSF'07), pp. 97-111. IEEE, Venice, Italy (2007).

Digital Library

[27]

Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing (2007).

Digital Library

[28]

Bresson, E., Lakhnech, Y., Mazar&#233;, L., Warinschi, B.: A generalization of ddh with applications to protocol analysis and computational soundness. In: Advances in Cryptology--CRYPTO 2007. LNCS, vol. 4622, pp. 482-499. Springer, Heidelberg (2007).

Digital Library

[29]

Backes, M., Moedersheim, S., Pfitzmann B., Vigano, L.: Symbolic and cryptographic analysis of the secure ws-reliablemessaging scenario. In: Proc. 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06). LNCS, vol. 3921 (2006).

Digital Library

[30]

Bana, G., Mohassel, P., Stegers, T.: The computational soundness of formal indistinguishability and static equivalence. In: Proc. 11th Asian Computing Science Conference (ASIAN'06). LNCS, vol. 4435, pp. 182-196. Springer, Heidelberg (2006).

Digital Library

[31]

Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: Proceedings of 29th IEEE Symposium on Security and Privacy (2008).

Digital Library

[32]

Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. In: Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST-TCS'03). LNCS, vol. 2914, pp. 1-12 (2003).

[33]

Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. J. Sel. Area. Comm. 22(10), 2075-2086 (2004).

Digital Library

[34]

Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE Computer Science Foundations Workshop (CSFW'04), pp. 204-218 (2004).

Digital Library

[35]

Backes, M., Pfitzmann B.: Limits of the cryptographic realization of Dolev-Yao-style xor. In: Proc. 10th European Symposium on Research in Computer Security (ESORICS'05). LNCS, vol. 3679, pp. 336-354 (2005).

Digital Library

[36]

Backes, M., Pfitzmann, B.: Relating symbolic and computational secrecy. Transactions on Dependable and Secure Computing 2(2), 109-123 (2005).

Digital Library

[37]

Backes, M., Pfitzmann, B.: On the cryptographic key secrecy of the strengthened yahalom protocol. In: Proc. 21st IFIP International Information Security Conference (SEC'06) (2006).

[38]

Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: CRYPTO'06. Lecture Notes on Computer Science, vol. 4117, pp. 537-554. Springer, Santa Barbara (2006).

Digital Library

[39]

Backes, M., Pfitzmann, B., Scedrov, A.: Key-dependent message security under active attacks-- BRSIM/UC-soundness of symbolic encryption with key cycles. J. Comput. Secur. 16, 497-530 (2008).

Digital Library

[40]

Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proc. 10th ACM Conference on Computer and Communications Security (CCS'03) (2003).

Digital Library

[41]

Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within simulatable cryptographic library. In: Proc. 8th European Symposium on Research in Computer Security (ESORICS'03). LNCS, pp. 271-290 (2003).

[42]

Backes, M., Pfitzmann, B., Waidner, M.: Limits of the reactive simulatability/uc of Dolev-Yao models with hashes. In: Proceedings of 11th European Symposium on Research in Computer Security (ESORICS). LNCS, vol. 4189, pp. 404-423. Springer, Heidelberg (2006) (Preprint on IACR ePrint 2006/068).

Digital Library

[43]

Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability framework. Inf. Comput. 205(12), 1685-1720 (2007).

Digital Library

[44]

Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685-1720 (2007).

Digital Library

[45]

Black, J., Rogaway, P., Shrimpton, T.: Encryption-scheme security in the presence of key-dependent messages. In: Selected Areas in Cryptography 2002 (SAC '02). LNCS, vol. 2595, pp. 62-75. Springer, St. John's (2002).

Digital Library

[46]

Backes, M., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs against active attackers. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pp. 255-269. IEEE Computer Society, Pittsburgh (2008).

Digital Library

[47]

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

Digital Library

[48]

Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, O., Segala, R.: Time-bounded task-pioas: a framework for analyzing security protocols. In: Proceedings of the 20th International Symposium on Distributed Computing, pp. 238-253 (2006).

Digital Library

[49]

Courant, J., Daubignard, M., Cristian Ene, P.L., Lahknech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: Proc. 15th ACM Conference on Computer and Communications Security, (CCS'08). Alexandria, USA (2008).

Digital Library

[50]

Courant, J., Ene, C., Lakhnech, Y.: Computationally sound typing for non-interference: the case of deterministic encryption. In: Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07). LNCS, vol. 4855, pp. 364-375. Springer, New Delhi (2007).

Digital Library

[51]

Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols (extended abstract). In: Proc. 3rd Theory of Cryptography Conference (TCC'06). LNCS, vol. 3876, pp. 380-403. Springer, Heidelberg (2006).

Digital Library

[52]

Cortier, V., Hordegen, H., Warinschi, B.: Explicit randomness is not necessary when modeling probabilistic encryption. In: Workshop on Information and Computer Security (ICS 2006). Timisoara, Romania (2006).

[53]

Cortier, V., Kremer, S., K&#252;sters, R., Warinschi, B.: Computationally sound symbolic secrecy in the presence of hash functions. In: Proceedings of the 26th Conference on Fundations of Software Technology and Theoretical Computer Science (FSTTCS'06). LNCS, vol. 4337, pp. 176-187. Springer, Kolkata (2006).

Digital Library

[54]

Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08). ACM, Alexandria (2008).

Digital Library

[55]

Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: European Symposium on Programming (ESOP'05). LNCS, vol. 3444, pp. 157-171. Springer, Edinburgh (2005).

Digital Library

[56]

Cortier, V., Zalinescu, E.: Deciding key cycles for security protocols. In: Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06). Lecture Notes in Artificial Intelligence, vol. 4246, pp. 317-331. Springer, Phnom Penh (2006).

Digital Library

[57]

Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Proc. of 32nd International Colloquium on Automata, Languages and Programming, ICALP. LNCS, vol. 3580, pp. 16-29. Springer, Lisbon (2005).

Digital Library

[58]

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

Digital Library

[59]

Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321-334 (2006).

Digital Library

[60]

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

Digital Library

[61]

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

Digital Library

[62]

Galindo, D., Garcia, F.D., van Rossum, P.: Computational soundness of non-malleable commitments. In: Proc. 4th Information Security Practice and Experience Conference (ISPEC'08). LNCS, vol. 4991, pp. 361-376 (2008).

Digital Library

[63]

Goldwasser, S., Micali, S., Rivest, R.L.: A digital signature scheme secure against adaptive chosen message attacks. SIAM J. Comput. 17(2), 281-308 (1988).

Digital Library

[64]

Groth, J., Ostrovsky, R.: Cryptography in the multi-string model. In: Appears in Advances in Cryptology--CRYPTO 2007. LNCS, vol. 4622, pp. 323-341 (2007).

Digital Library

[65]

Gupta, P., Shmatikov, V.: Towards computationally sound symbolic analysis of key exchange protocols. In: Proc. of the 2005 ACM Workshop on Formal Methods in Security Engineering (FMSE'05), pp. 23-32. ACM, New York (2005).

Digital Library

[66]

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

[67]

Garcia, F.D., van Rossum, P.: Sound computational interpretation of symbolic hashes in the standard model. In: Proc. International Workshop on Security 2006 (IWSEC'06). LNCS, pp. 33-47. Springer, Heidelberg (2006).

Digital Library

[68]

Garcia, F.D., van Rossum, P.: Sound and complete computational interpretation of symbolic hashes in the standard model. Theor. Comp. Sci. 394, 112-133 (2008).

Digital Library

[69]

Herzog, J.: A computational interpretation of Dolev-Yao adversaries. In: Proceedings of the 3rd IFIPWG1.7 Workshop on Issues in the Theory of Security (WITS'03) (2003).

[70]

Herzog, J.: A computational interpretation of Dolev-Yao adversaries. Theor. Comp. Sci. 340, 57-81 (2005).

Digital Library

[71]

Horvitz, O., Gligor, V.D.: Weak key authenticity and the computational completeness of formal encryption. In: Advances in Cryptology--CRYPTO 2003. LNCS, vol. 2729, pp. 530-547. Springer, Heidelberg (2003).

[72]

Janvier, R., Lakhnech, Y., Mazar&#233;, L.: Completing the picture: soundness of formal encryption in the presence of active adversaries. In: European Symposium on Programming (ESOP'05). LNCS, vol. 3444, pp. 172-185. Springer, Heidelberg (2005).

Digital Library

[73]

Janvier, R., Lakhnechm, Y., Mazar&#233;, L.: Computational soundness of symbolic analysis for protocols using hash functions. In: Proceedings of the Workshop on Information and Computer Security (ICS'06), Electronic Notes in Theoretical Computer Scienc. Elsevier Science Publishers, Timisoara, Romania (2006).

Digital Library

[74]

K&#252;sters, R., Datta, A., Mitchell, J.C., Ramanathan, A.: On the Relationships Between Notions of Simulation-Based Security. J. Cryptol. 21, 492-546 (2008). 008-9019-9.

Digital Library

[75]

Kremer, S., Mazar&#233;, L.: Adaptive soundness of static equivalence. In: Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07). LNCS, vol. 4734, pp. 610-625. Springer, Dresden (2007).

Digital Library

[76]

Kremer, S., Mazar&#233;, L.: Computationally sound analysis of protocols using bilinear pairings. J. Comput. Secur. (2010, in press).

Digital Library

[77]

K&#252;sters, R., Tuengerthal, M.: Joint state theorems for public-key encryption and digital signature functionalities with local computations. In: Computer Security Foundations (CSF'08) (2008).

Digital Library

[78]

Laud, P.: Semantics and program analysis of computationally secure information flow. In: Proc. 10th European Symposium on Programming (ESOP'01). LNCS, vol. 2028, pp. 77-91. Springer, Heidelberg (2001).

Digital Library

[79]

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

[80]

Laud, P.: Handling encryption in an analysis for secure information flow. In: Proc. 12th European Symposium on Programming (ESOP'03). LNCS, vol. 2618, pp. 159-173. Springer, Heidelberg (2003).

Digital Library

[81]

Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. IEEE Symposium on Security and Privacy (SSP'04), pp. 71-85 (2004).

[82]

Laud, P.: Secrecy types for a simulatable cryptographic library. In: Proc. 12th ACM Conference on Computer and Communications Security (CCS'05) (2005).

Digital Library

[83]

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

Digital Library

[84]

Laud, P., Corin, R.: Sound computational interpretation of formal encryption with composed keys. In: Proc. 6th International Conference on Information Security and Cryptology (ICISC'03), LNCS, vol. 2971, pp. 55-66. Springer, Heidelberg (2004).

[85]

Lincoln, P., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proc. 5th ACM Conference on Computer and Communications Security (CCS'98), pp. 112-121 (1998).

Digital Library

[86]

Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96). LNCS, vol. 1055, pp. 147-166. Springer, Heidelberg (1996).

Digital Library

[87]

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

[88]

Laud, P., Vene, V.: A type system for computationally secure information flow. In: Proc. 15th International Symposium on Fundamentals of Computation Theory (FCT'05). LNCS, vol. 3623, pp. 365-377. Springer, Heidelberg (2005).

Digital Library

[89]

Mazar&#233;, L.: Computationally sound analysis of protocols using bilinear pairings. In: Proc. 7th International Workshop on Issues in the Theory of Security (WITS'07), pp. 6-21 (2007).

[90]

Micciancio, D., Panjwani, S.: Adaptive security of symbolic encryption. In: Proc. 2nd Theory of Cryptography Conference (TCC'05). LNCS, vol. 3378, pp. 169-187. Springer, Heidelberg (2005).

Digital Library

[91]

Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time calculus for analysis of cryptographic protocols. In: Proc. 17th Annual Conference on the Mathematical Foundations of Programming Semantics. ENTCS, vol. 45 (2001).

[92]

Miklau, G., Suciu, D.: Controlling access to published data using cryptography. In: VLDB '2003: Proceedings of the 29th International Conference on Very Large Data Bases, pp. 898-909. VLDB Endowment (2003).

Digital Library

[93]

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

[94]

Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. J. Comput. Secur. 12(1), 99-129 (2004).

Digital Library

[95]

Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Proc. 1st Theory of Cryptography Conference (TCC'04). LNCS, vol. 2951, pp. 133-151. Springer, Heidelberg (2004).

[96]

Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive proofs of computational secrecy. In: Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07). LNCS, vol. 4734, pp. 219-234. Springer (2007).

Digital Library

[97]

Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of Diffie-Hellman based protocols. In: Revised Selected Papers from the 3rd Symposium on Trustworthy Global Computing (TGC'07). LNCS, vol. 4912. Springer, Sophia-Antipolis (2008).

Digital Library

[98]

Ramanathan, A., Mitchell, J.C., Scedrov, A., Teague, V.: Probabilistic bisimulation and equivalence for security analysis of network protocols. In: Proc. 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'04). LNCS, vol. 2987, pp. 468-483. Springer, Heidelberg (2004).

[99]

Ramanathan, A., Mitchell, J.C., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comp. Sci. 353, 118-164 (2006).

Digital Library

[100]

Smith, G., Alp&#237;zar, R.: Secure information flow with random assignment and encryption. In: Proc. Workshop on Formal Methods in Security Engineering (FMSE'06), pp. 33-44. ACM, New York (2006).

Digital Library

[101]

Sprenger, C., Basin, D.: Cryptographically-sound protocol-model abstractions. In: Logic in Computer Science (LICS 08), pp. 3-17. IEEE Computer Society (2008).

Digital Library

[102]

Sprenger, C., Basin, D.: Cryptographically-sound protocol-model abstractions. In: Computer Security Foundations (CSF 08), pp. 115-129. IEEE Computer Society (2008).

Digital Library

[103]

Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: Proc. 19th IEEE Computer Science Foundations Workshop (CSFW'06), pp. 153-166 (2006).

Digital Library

[104]

Tarento, S.: Machine-checked security proofs of cryptographic signature schemes. In: Proc. 10th European Symposium on Research in Computer Security (ESORICS'05). LNCS, vol. 3679, pp. 140-158 (2005).

Digital Library

[105]

Warinschi, B.: A computational analysis of the Needham-Schroeder protocol. J. Comput. Secur. 13, 565-591 (2005).

Digital Library

Cited By

Klenze TSprenger CBasin D(2023)IsaNetJournal of Computer Security10.3233/JCS-22002131:3(217-259)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/JCS-220021
Bhargavan KCheval VWood CYin HStavrou ACremers CShi E(2022)A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client HelloProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3559360(365-379)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3559360
Kozyri ESchneider F(2020)RIFJournal of Computer Security10.3233/JCS-19131628:2(191-228)Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.3233/JCS-191316
Show More Cited By

Index Terms

A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

Index terms have been assigned to the content through auto-classification.

Recommendations

Improvement of a Convertible Undeniable Partially Blind Signature Scheme
AINA '06: Proceedings of the 20th International Conference on Advanced Information Networking and Applications - Volume 01

Undeniable signatures are the digital signatures that should be verified with the help of the signer. A signer may disavow a genuine document, if the signature is only verifiable with the aid of the signer under the condition that the signer is not ...
A computational analysis of the Needham-Schroeder-(Lowe) protocol

The Needham Schroeder protocol and its repaired verdion due to Lowe are the main test cases used by symbolic methods for cryptographic protocol analysis. In this paper we proved the first computational analysis of the protocol. We start by translating ...
Comparative Analysis of RSA and ElGamal Cryptographic Public-key Algorithms
ICASI'18: Proceedings of the Joint Workshop KO2PI and the 1st International Conference on Advance & Scientific Innovation

An asymmetric algorithm is an encryption technique that uses different keys on the process of encryption and decryption. This algorithm uses two keys, public key, and private key. The public key is publicly distributed while the private key is kept ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 46, Issue 3-4

April 2011

196 pages

ISSN:0168-7433

Issue’s Table of Contents

Copyright © Copyright © 2011 Springer Science+Business Media B.V.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 April 2011

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Klenze TSprenger CBasin D(2023)IsaNetJournal of Computer Security10.3233/JCS-22002131:3(217-259)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/JCS-220021
Bhargavan KCheval VWood CYin HStavrou ACremers CShi E(2022)A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client HelloProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3559360(365-379)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3559360
Kozyri ESchneider F(2020)RIFJournal of Computer Security10.3233/JCS-19131628:2(191-228)Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.3233/JCS-191316
Hale B(2020)User-mediated authentication protocols and unforgeability in key collisionInternational Journal of Information Security10.1007/s10207-019-00479-219:6(609-621)Online publication date: 1-Dec-2020
https://dl.acm.org/doi/10.1007/s10207-019-00479-2
Yan JWang YGoto YCheng J(2019)An Extension of Formal Analysis Method with Reasoning: A Case Study of Flaw Detection for Non-repudiation and FairnessCodes, Cryptology and Information Security10.1007/978-3-030-16458-4_23(399-408)Online publication date: 22-Apr-2019
https://dl.acm.org/doi/10.1007/978-3-030-16458-4_23
Blanchet B(2016)Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerifFoundations and Trends in Privacy and Security10.1561/33000000041:1-2(1-135)Online publication date: 31-Oct-2016
https://dl.acm.org/doi/10.1561/3300000004
Lochbihler A(2016)Probabilistic Functions and Cryptographic Oracles in Higher Order LogicProceedings of the 25th European Symposium on Programming Languages and Systems - Volume 963210.1007/978-3-662-49498-1_20(503-531)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49498-1_20
Cortier VKremer S(2014)Formal Models and Techniques for Analyzing Security ProtocolsFoundations and Trends in Programming Languages10.1561/25000000011:3(151-267)Online publication date: 13-Nov-2014
https://dl.acm.org/doi/10.1561/2500000001
Avalle MPironti ASisto R(2014)Formal verification of security protocol implementations: a surveyFormal Aspects of Computing10.1007/s00165-012-0269-926:1(99-123)Online publication date: 1-Jan-2014
https://dl.acm.org/doi/10.1007/s00165-012-0269-9
Wang HZhu LYang ZLiao L(2013)A new hierarchical and scalable group key exchange protocol with XOR operationInternational Journal of Wireless and Mobile Computing10.1504/IJWMC.2013.0565506:4(355-361)Online publication date: 1-Sep-2013
https://dl.acm.org/doi/10.1504/IJWMC.2013.056550
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents