Skip to main content
SpringerLink
Log in

Historical Background and Further Reading

  • Chapter
Operational Semantics and Verification of Security Protocols

Part of the book series: Information Security and Cryptography ((ISC))

  • 2102 Accesses

Abstract

We provide historical background on our approach, we give pointers for further reading and we describe alternative approaches. We only cover those approaches that are closely related to ours.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.95
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 69.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Several years later, researchers started to work on automated tool support for computational models, e.g., [35].

References

  1. M. Abadi, B. Blanchet, C. Fournet, Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. 10(3), 9 (2007)

    Article  Google Scholar 

  2. M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’01), ed. by C. Hankin, D. Schmidt, London, UK (ACM, New York, 2001), pp. 104–115

    Chapter  Google Scholar 

  3. M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: the Spi calculus. Inf. Comput. 148, 1–70 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  4. M. Abadi, P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption), in IFIP International Conference on Theoretical Computer Science (IFIP TCS’00), ed. by J. van Leeuwen, O. Watanabe, M. Hagiya, P.D. Mosses, T. Ito, Sendai, Japan (2000), pp. 3–22

    Google Scholar 

  5. M. Abadi, M. Tuttle, A semantics for a logic of authentication, in 10th ACM Symposium on Principles of Distributed Computing (PODC’91), Montreal, Canada (ACM, New York, 1991), pp. 201–216

    Chapter  Google Scholar 

  6. M. Aizatulin, A.D. Gordon, J. Jürjens, Extracting and verifying cryptographic models from C protocol code by symbolic execution, in 18th ACM Conference on Computer and Communications Security (ACM CCS’11), ed. by Y. Chen, G. Danezis, V. Shmatikov, Chicago, USA (ACM, New York, 2011), pp. 331–340

    Google Scholar 

  7. J. Alves-Foss, Multiprotocol attacks and the public key infrastructure, in 21st National Information Systems Security Conference (NISSC’98), Arlington, USA (NIST, Gaithersburg, 1998), pp. 566–576

    Google Scholar 

  8. S. Andova, C.J.F. Cremers, K. Gjøsteen, S. Mauw, S.F. Mjølsnes, S. Radomirović, A framework for compositional verification of security protocols. Inf. Comput. 206(2–4), 425–459 (2008)

    Article  MATH  Google Scholar 

  9. M. Arapinis, E. Ritter, M.D. Ryan, StatVerif: verification of stateful processes, in 24th IEEE Computer Security Foundations Symposium (CSF’11) (IEEE Computer Society, Los Alamitos, 2011), pp. 33–47

    Chapter  Google Scholar 

  10. A. Armando, W. Arsac, T. Avanesov, M. Barletta, A. Calvi, A. Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cuéllar, G. Erzse, S. Frau, M. Minea, S. Mödersheim, D. von Oheimb, G. Pellegrino, S.E. Ponta, M. Rocchetto, M. Rusinowitch, M. Torabi Dashti, M. Turuani, L. Viganò, The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), ed. by C. Flanagan, B. König, Tallinn, Estonia. Lecture Notes in Computer Science, vol. 7214 (Springer, Berlin, 2012)

    Google Scholar 

  11. A. Armando, D.A. Basin, Y. Boichut, Y. Chevalier, L. Compagna, L. Cuellar, P.H. Drielsma, P. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, L. Vigneron, The AVISPA tool for the automated validation of internet security protocols and applications, in 17th International Conference on Computer Aided Verification (CAV’05), Edinburgh, UK. Lecture Notes in Computer Science, vol. 3576 (Springer, Berlin, 2005), pp. 281–285

    Chapter  Google Scholar 

  12. A. Armando, R. Carbone, L. Compagna, J. Cuéllar, M.L. Tobarra, Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google apps, in 6th ACM Workshop on Formal Methods in Security Engineering (FMSE’08), ed. by V. Shmatikov, Alexandria, USA (ACM, New York, 2008), pp. 1–10

    Chapter  Google Scholar 

  13. A. Armando, L. Compagna, SAT-based model checking for security protocols analysis. Int. J. Inf. Secur. 7(1), 3–32 (2008)

    Article  Google Scholar 

  14. G. Ateniese, M. Steiner, G. Tsudik, Authenticated group key agreement and friends, in 5th ACM Conference on Computer and Communications Security (ACM CCS’98), San Francisco, USA (ACM, New York, 1998), pp. 17–26

    Chapter  Google Scholar 

  15. G. Ateniese, M. Steiner, G. Tsudik, New multiparty authentication services and key agreement protocols. IEEE J. Sel. Areas Commun. 18(4), 628–639 (2000)

    Article  Google Scholar 

  16. M. Backes, B. Pfitzmann, M. Waidner, A composable cryptographic library with nested operations, in 10th ACM Conference on Computer and Communications Security (ACM CCS’03), ed. by S. Jajodia, V. Atluri, T. Jaeger (ACM, New York, 2003), pp. 220–230

    Chapter  Google Scholar 

  17. D.A. Basin, Lazy infinite-state analysis of security protocols, in Secure Networking (CQRE’99), ed. by R. Baumgart, Düsseldorf, Germany. Lecture Notes in Computer Science, vol. 1740 (Springer, Berlin, 1999), pp. 30–42

    Google Scholar 

  18. D.A. Basin, C.J.F. Cremers, Modeling and analyzing security in the presence of compromising adversaries, in 15th European Symposium on Research in Computer Security (ESORICS’10), Athens, Greece. Lecture Notes in Computer Science, vol. 6345 (Springer, Berlin, 2010), pp. 340–356

    Google Scholar 

  19. D.A. Basin, C.J.F. Cremers, S. Meier, Provably repairing the ISO/IEC 9798 standard for entity authentication, in 1st International Conference on Principles of Security and Trust (POST’12), ed. by P. Degano, J.D. Guttman, Tallinn, Estonia. Lecture Notes in Computer Science, vol. 7215 (Springer, Berlin, 2012), pp. 129–148

    Google Scholar 

  20. D.A. Basin, S. Mödersheim, L. Viganò, Algebraic intruder deductions, in 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’05), Montego Bay, Jamaica. Lecture Notes in Artificial Intelligence, vol. 3835 (Springer, Berlin, 2005), pp. 549–564

    Chapter  Google Scholar 

  21. D.A. Basin, S. Mödersheim, L. Viganò, OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181–208 (2005)

    Article  Google Scholar 

  22. G. Bella, F. Massacci, L.C. Paulson, The verification of an industrial payment protocol: the SET purchase phase, in 9th ACM Conference on Computer and Communications Security (ACM CCS’02), ed. by V. Atluri, Washington, USA (ACM, New York, 2002), pp. 12–20

    Chapter  Google Scholar 

  23. G. Bella, F. Massacci, L.C. Paulson, Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. 21(1), 77–87 (2003)

    Article  Google Scholar 

  24. G. Bella, F. Massacci, L.C. Paulson, An overview of the verification of SET. Int. J. Inf. Secur. 4(1–2), 17–28 (2005)

    Article  Google Scholar 

  25. G. Bella, F. Massacci, L.C. Paulson, P. Tramontano, Formal verification of cardholder registration in SET, in 6th European Symposium on Research in Computer Security (ESORICS’00), ed. by F. Cuppens, Y. Deswarte, D. Gollmann, M. Waidner, Toulouse, France. Lecture Notes in Computer Science, vol. 1895 (Springer, Berlin, 2000), pp. 159–174

    Google Scholar 

  26. G. Bella, L.C. Paulson, Using Isabelle to prove properties of the Kerberos authentication system, in Workshop on Design and Formal Verification of Security Protocols, ed. by H. Orman, C. Meadows, Piscataway, USA (DIMACS, Rutgers, 1997)

    Google Scholar 

  27. G. Bella, L.C. Paulson, Kerberos version IV: inductive analysis of the secrecy goals, in 5th European Symposium on Research in Computer Security (ESORICS’98), ed. by J.-J. Quisquater, Y. Deswarte, C. Meadows, D. Gollmann, Louvain-la-Neuve, Belgium. Lecture Notes in Computer Science, vol. 1485 (Springer, Berlin, 1998), pp. 361–375

    Google Scholar 

  28. G. Bella, L.C. Paulson, Mechanical proofs about a non-repudiation protocol, in 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’01), ed. by R.J. Boulton, P.B. Jackson, Edinburgh, UK. Lecture Notes in Computer Science, vol. 2152 (Springer, Berlin, 2001), pp. 91–104

    Chapter  Google Scholar 

  29. K. Bhargavan, C. Fournet, R.J. Corin, E. Zalinescu, Cryptographically verified implementations for TLS, in 15th ACM Conference on Computer and Communications Security (ACM CCS’08), ed. by P. Ning, P.F. Syverson, S. Jha, Alexandria, USA (ACM, New York, 2008), pp. 459–468

    Chapter  Google Scholar 

  30. K. Bhargavan, C. Fournet, A.D. Gordon, Modular verification of security protocol code by typing, in 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10), ed. by M.V. Hermenegildo, J. Palsberg, Madrid, Spain (ACM, New York, 2010), pp. 445–456

    Google Scholar 

  31. P. Bieber, N. Boulahia-Cuppens, Formal development of authentication protocols, in 6th BCS-FACS Refinement Workshop, London, UK (1994)

    Google Scholar 

  32. B. Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in 14th IEEE Computer Security Foundations Workshop (CSFW’01), Cape Breton, Canada (IEEE Computer Society, Los Alamitos, 2001), pp. 82–96

    Chapter  Google Scholar 

  33. B. Blanchet, Automatic proof of strong secrecy for security protocols, in 25th IEEE Symposium on Security & Privacy (S&P’04), Oakland, USA (IEEE Computer Society, Los Alamitos, 2004), pp. 86–100

    Chapter  Google Scholar 

  34. B. Blanchet, A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5(4), 193–207 (2008)

    Article  Google Scholar 

  35. C. Boyd, Towards extensional goals in authentication protocols, in Workshop on Design and Formal Verification of Security Protocols, ed. by H. Orman, C. Meadows, Piscataway, USA (DIMACS, Rutgers, 1997)

    Google Scholar 

  36. E. Bresson, O. Chevassut, D. Pointcheval, J.J. Quisquater, Provably authenticated group Diffie-Hellman key exchange, in 8th ACM Conference on Computer and Communications Security (ACM CCS’01), ed. by M.K. Reiter, P. Samarati, Philadelphia, USA (ACM, New York, 2001), pp. 255–264

    Chapter  Google Scholar 

  37. M. Burrows, M. Abadi, R.M. Needham, A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)

    Article  Google Scholar 

  38. L. Buttyán, A. Nagy, I. Vajda, Efficient multi-party challenge-response protocols for entity authentication. Period. Polytech. 45(1), 43–64 (2001)

    Google Scholar 

  39. R. Canetti, Universally composable security: a new paradigm for cryptographic protocols. IACR Cryptology ePrint Archive, Report 2000/067 (2000)

    Google Scholar 

  40. R. Canetti, C. Meadows, P. Syverson, Environmental requirements for authentication protocols, in Software Security—Theories and Systems, Mext-NSF-JSPS International Symposium (ISSS’02), ed. by M. Okada, B.C. Pierce, A. Scedrov, H. Tokuda, A. Yonezawa, Tokyo, Japan. Lecture Notes in Computer Science, vol. 2609 (Springer, Berlin, 2002), pp. 339–355

    Google Scholar 

  41. E.M. Clarke, S. Jha, W. Marrero, Verifying security protocols with Brutus. ACM Trans. Softw. Eng. Methodol. 9(4), 443–487 (2000)

    Article  Google Scholar 

  42. R.J. Corin, S. Etalle, An improved constraint-based system for the verification of security protocols, in 9th International Static Analysis Symposium (SAS’02), ed. by M.V. Hermenegildo, G. Puebla, Madrid, Spain. Lecture Notes in Computer Science, vol. 2477 (Springer, Berlin, 2002), pp. 326–341

    Google Scholar 

  43. R.J. Corin, A. Saptawijaya, S. Etalle, A logic for constraint-based security protocol analysis, in 27th IEEE Symposium on Security & Privacy (S&P’06), Berkeley, USA (IEEE Computer Society, Los Alamitos, 2006), pp. 155–168

    Google Scholar 

  44. V. Cortier, S. Delaune, Safely composing security protocols. Form. Methods Syst. Des. 34(1), 1–36 (2009)

    Article  MATH  Google Scholar 

  45. V. Cortier, S. Delaune, P. Lafourcade, A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006)

    Google Scholar 

  46. V. Cortier, S. Kremer, B. Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reason. 46(3–4), 225–259 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  47. V. Cortier, M. Rusinowitch, E. Zalinescu, Relating two standard notions of secrecy. Log. Methods Comput. Sci. 3(3), 1–29 (2007)

    MathSciNet  Google Scholar 

  48. C.J.F. Cremers, Feasibility of multi-protocol attacks, in 1st International Conference on Availability, Reliability and Security (ARES’06), Vienna, Austria (IEEE Computer Society, Los Alamitos, 2006), pp. 287–294

    Google Scholar 

  49. C.J.F. Cremers, On the protocol composition logic PCL, in ACM Symposium on Information, Computer & Communication Security (ASIACCS’08), ed. by M. Abe, V. Gligor, Tokyo, Japan (ACM, New York, 2008), pp. 66–76

    Google Scholar 

  50. C.J.F. Cremers, The Scyther tool: verification, falsification, and analysis of security protocols, in 20th International Conference on Computer Aided Verification (CAV’08), ed. by A. Gupta, S. Malik, Princeton, USA. Lecture Notes in Computer Science, vol. 5123 (Springer, Berlin, 2008), pp. 414–418

    Chapter  Google Scholar 

  51. C.J.F. Cremers, Session-state reveal is stronger than eCK’s ephemeral key reveal: using automatic analysis to attack the NAXOS protocol. Int. J. Appl. Cryptogr. 2(2), 83–99 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  52. C.J.F. Cremers, P. Lafourcade, P. Nadeau, Comparing state spaces in automatic protocol analysis, in Formal to Practical Security, ed. by V. Cortier, C. Kirchner, M. Okada, H. Sakurada. Lecture Notes in Computer Science, vol. 5458 (Springer, Berlin, 2009), pp. 70–94

    Chapter  Google Scholar 

  53. A. Datta, A. Derek, J.C. Mitchell, D. Pavlovic, Secure protocol composition, in 1st ACM Workshop on Formal Methods in Security Engineering (FMSE’03), ed. by M. Backes, D.A. Basin, Washington, USA (ACM, New York, 2003), pp. 11–23

    Google Scholar 

  54. A. Datta, A. Derek, J.C. Mitchell, A. Roy, Protocol Composition Logic (PCL), in Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, ed. by L. Cardelli, M. Fiore, G. Winskel. Electronic Notes in Theoretical Computer Science, vol. 172, (2007), pp. 311–358

    Google Scholar 

  55. A. Datta, J.C. Mitchell, A. Roy, S. Stiller, Protocol composition logic, in Formal Models and Techniques for Analyzing Security Protocols, ed. by V. Cortier, S. Kremer (IOS Press, Lansdale, 2011)

    Google Scholar 

  56. S. Delaune, S. Kremer, M.D. Ryan, Composition of password-based protocols, in 21st IEEE Computer Security Foundations Symposium (CSF’08), Pittsburgh, USA (IEEE Computer Society, Los Alamitos, 2008), pp. 239–251

    Chapter  Google Scholar 

  57. X. Didelot, COSP-J: a compiler for security protocols. Master’s thesis, University of Oxford, Computing Laboratory (2003)

    Google Scholar 

  58. W. Diffie, P.C. van Oorschot, M.J. Wiener, Authentication and authenticated key-exchanges. Des. Codes Cryptogr. 2(2), 107–125 (1992)

    Article  MathSciNet  Google Scholar 

  59. S. Doghmi, J.D. Guttman, F.J. Thayer, Skeletons and the shapes of bundles, in 7th International Workshop on Issues in the Theory of Security (WITS’07), Braga, Portugal (2007)

    Google Scholar 

  60. S.F. Doghmi, J.D. Guttman, F.J. Thayer, Searching for shapes in cryptographic protocols, in 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’07), ed. by O. Grumberg, M. Huth, Braga, Portugal. Lecture Notes in Computer Science, vol. 4424 (Springer, Berlin, 2007), pp. 523–537

    Chapter  Google Scholar 

  61. S.F. Doghmi, J.D. Guttman, F.J. Thayer, Skeletons, homomorphisms, and shapes: characterizing protocol executions, in 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII), New Orleans, USA. Electronic Notes in Theoretical Computer Science, vol. 173 (Elsevier, Amsterdam, 2007), pp. 85–102

    Google Scholar 

  62. D. Dolev, A.C. Yao, On the security of public key protocols (extended abstract), in 22nd IEEE Symposium on Foundations of Computer Science (FOCS’81), Nashville, USA (IEEE Computer Society, Los Alamitos, 1981), pp. 350–357

    Google Scholar 

  63. D. Dolev, A.C. Yao, On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  64. N.A. Durgin, P.D. Lincoln, J.C. Mitchell, A. Scedrov, Undecidability of bounded security protocols, in Formal Methods and Security Protocols (FMSP’99), Trento, Italy (1999)

    Google Scholar 

  65. N.A. Durgin, J.C. Mitchell, D. Pavlovic, A compositional logic for protocol correctness, in 14th IEEE Computer Security Foundations Workshop (CSFW’01), Cape Breton, Canada (IEEE Computer Society, Los Alamitos, 2001), pp. 241–272

    Chapter  Google Scholar 

  66. S. Erbatur, S. Escobar, D. Kapur, Z. Liu, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, S. Santiago, R. Sasse, Effective symbolic protocol analysis via equational irreducibility conditions, in 17th European Symposium on Research in Computer Security (ESORICS’12), ed. by S. Foresti, M. Yung, F. Martinelli, Pisa, Italy. Lecture Notes in Computer Science, vol. 7459 (Springer, Berlin, 2012), pp. 73–90

    Google Scholar 

  67. S. Escobar, D. Kapur, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, R. Sasse, Protocol analysis in Maude-NPA using unification modulo homomorphic encryption, in 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’11), ed. by P. Schneider-Kamp, M. Hanus, Odense, Denmark (ACM, New York, 2011), pp. 65–76

    Google Scholar 

  68. S. Escobar, C. Meadows, J. Meseguer, Maude-NPA: cryptographic protocol analysis modulo equational properties, in Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, ed. by A. Aldini, G. Barthe, R. Gorrieri. Lecture Notes in Computer Science, vol. 5705 (Springer, Berlin, 2009), pp. 1–50

    Chapter  Google Scholar 

  69. R. Focardi, F. Martinelli, A uniform approach for the definition of security properties, in World Congress on Formal Methods in the Development of Computing Systems (FM’99), ed. by J.M. Wing, J. Woodcock, J. Davies, Toulouse, France. Lecture Notes in Computer Science, vol. 1708 (Springer, Berlin, 1999), pp. 794–813

    Google Scholar 

  70. International Organization for Standardization. Information technology—security techniques—entity authentication, part 1: general model. ISO/IEC 9798-1 (1991)

    Google Scholar 

  71. D. Gollmann, What do we mean by entity authentication, in 17th IEEE Symposium on Security & Privacy (S&P’96), Oakland, USA (IEEE Computer Society, Los Alamitos, 1996), pp. 46–54

    Google Scholar 

  72. D. Gollmann, On the verification of cryptographic protocols—a tale of two committees, in Workshop on Secure Architectures and Information Flow 1999, London, UK. Electronic Notes in Theoretical Computer Science, vol. 32 (Elsevier, Amsterdam, 2000), pp. 42–58

    Google Scholar 

  73. L. Gong, R.M. Needham, R. Yahalom, Reasoning about belief in cryptographic protocol analysis, in 11th IEEE Symposium on Security & Privacy (S&P’90), Oakland, USA (IEEE Computer Society, Los Alamitos, 1990), pp. 234–248

    Google Scholar 

  74. L. Gong, P. Syverson, Fail-stop protocols: an approach to designing secure protocols, in 5th International Working Conference on Dependable Computing for Critical Applications (DCCA’95), Urbana-Champaign, USA (1995), pp. 44–55

    Google Scholar 

  75. J.D. Guttman, State and progress in Strand Spaces: proving fair exchange. J. Autom. Reason. 48(2), 159–195 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  76. J.D. Guttman, F.J. Thayer, Protocol independence through disjoint encryption, in 13th IEEE Computer Security Foundations Workshop (CSFW’00), Cambridge, UK (IEEE Computer Society, Los Alamitos, 2000), pp. 24–34

    Chapter  Google Scholar 

  77. J.D. Guttman, F.J. Thayer, Authentication tests and the structure of bundles. Theor. Comput. Sci. 283(2), 333–380 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  78. A. Huima, Efficient infinite-state analysis of security protocols, in FLOC Workshop on Formal Methods and Security Protocols (FMSP’99), ed. by N. Heintze, E. Clarke, Trento, Italy (1999)

    Google Scholar 

  79. J. Katz, M. Yung, Scalable protocols for authenticated group key exchange, in 23rd Annual International Cryptology Conference (CRYPTO’03), ed. by D. Boneh, Santa Barbara, USA. Lecture Notes in Computer Science, vol. 2729 (Springer, Berlin, 2003), pp. 110–125

    Google Scholar 

  80. J. Kelsey, B. Schneier, D. Wagner, Protocol interactions and the chosen protocol attack, in 5th International Workshop on Security Protocols, ed. by B. Christianson, B. Crispo, T.M.A. Lomas, M. Roe, Paris, France. Lecture Notes in Computer Science, vol. 1361 (Springer, Berlin, 1997), pp. 91–104

    Chapter  Google Scholar 

  81. R.A. Kemmerer, Analyzing encryption protocols using formal verification techniques, in Workshop on the Theory and Application of Cryptographic Techniques (EUROCRYPT’86), ed. by I. Ingemarsson, Linköping, Sweden (1986), p. 48

    Google Scholar 

  82. R.A. Kemmerer, C. Meadows, J.K. Millen, Three systems for cryptographic protocol analysis. J. Cryptol. 7, 79–130 (1994)

    Article  MATH  Google Scholar 

  83. S.T. Kent, Encryption-based protection for interactive user/computer communication, in 5th Symposium on Data Communications (SIGCOMM’77), Snowbird, USA (ACM, New York, 1977), pp. 5.7–5.13

    Chapter  Google Scholar 

  84. R. Küsters, T. Truderung, Using ProVerif to analyze protocols with Diffie-Hellman exponentiation, in 22nd IEEE Computer Security Foundations Symposium (CSF’09), Port Jefferson, USA (IEEE Computer Society, Los Alamitos, 2009), pp. 157–171

    Chapter  Google Scholar 

  85. R. Küsters, T. Truderung, Reducing protocol analysis with XOR to the XOR-free case in the Horn Theory based approach. J. Autom. Reason. 46(3–4), 325–352 (2011)

    Article  MATH  Google Scholar 

  86. P. Lincoln, J.C. Mitchell, M. Mitchell, A. Scedrov, A probabilistic poly-time framework for protocol analysis, in 5th ACM Conference on Computer and Communications Security (ACM CCS’98), ed. by L. Gong, M.K. Reiter, San Francisco, USA (ACM, New York, 1998), pp. 112–121

    Chapter  Google Scholar 

  87. D. Longley, S. Rigby, An automatic search for security flaws in key management schemes. Comput. Secur. 11(1), 75–89 (1992)

    Article  Google Scholar 

  88. G.L. Lowe, Casper: a compiler for the analysis of security protocols, in 10th IEEE Computer Security Foundations Workshop (CSFW’97), Rockport, USA (IEEE Computer Society, Los Alamitos, 1997), pp. 18–30

    Chapter  Google Scholar 

  89. G. Lowe, A hierarchy of authentication specifications, in 10th IEEE Computer Security Foundations Workshop (CSFW’97), Rockport, USA (IEEE Computer Society, Los Alamitos, 1997), pp. 31–44

    Chapter  Google Scholar 

  90. A. Mathuria, A.R. Singh, P.V. Sharavan, R. Kirtankar, Some new multi-protocol attacks, in 15th International Conference on Advanced Computing and Communications (ADCOM’07), Guwahati, India (IEEE Computer Society, Los Alamitos, 2007), pp. 465–471

    Chapter  Google Scholar 

  91. C. Meadows, The NRL protocol analyzer: an overview. J. Log. Program. 26(2), 113–131 (1996)

    Article  MATH  Google Scholar 

  92. C. Meadows, Analysis of the Internet Key Exchange Protocol using the NRL protocol analyzer, in 20th IEEE Symposium on Security & Privacy (S&P’99), Oakland, USA (IEEE Computer Society, Los Alamitos, 1999), pp. 216–231

    Google Scholar 

  93. S. Meier, C.J.F. Cremers, D.A. Basin, Strong invariants for the efficient construction of machine-checked protocol security proofs, in 23rd IEEE Computer Security Foundations Symposium (CSF’10), Edinburgh, UK (IEEE Computer Society, Los Alamitos, 2010), pp. 231–245

    Chapter  Google Scholar 

  94. S. Meier, B. Schmidt, The Tamarin prover: source code and case studies. http://hackage.haskell.org/package/tamarin-prover (accessed 18 Sept 2012)

  95. D. Micciancio, S. Panjwani, Optimal communication complexity of generic multicast key distribution, in Advances in Cryptology—International Conference on the Theory and Application of Cryptographic Techniques (EUROCRYPT’04), ed. by J. Camenisch, C. Cachin, Interlaken, Switzerland. Lecture Notes in Computer Science, vol. 3027 (Springer, Berlin, 2004), pp. 153–170

    Google Scholar 

  96. J.K. Millen, S.C. Clark, S.B. Freedman, The Interrogator: protocol security analysis. IEEE Trans. Softw. Eng. 13(2), 274–288 (1987)

    Article  Google Scholar 

  97. J.K. Millen, V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, in 8th ACM Conference on Computer and Communications Security (ACM CCS’01), ed. by M.K. Reiter, P. Samarati, Philadelphia, USA (ACM, New York, 2001), pp. 166–175

    Chapter  Google Scholar 

  98. J.K. Millen, V. Shmatikov, Symbolic protocol analysis with products and Diffie-Hellman exponentiation, in 16th IEEE Computer Security Foundations Workshop (CSFW’03), Pacific Grove, USA (IEEE Computer Society, Los Alamitos, 2003), pp. 47–61

    Google Scholar 

  99. R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, I. Inf. Comput. 100(1), 1–40 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  100. R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, II. Inf. Comput. 100(1), 41–77 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  101. J.C. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using Murϕ, in 18th IEEE Symposium on Security & Privacy (S&P’97), Oakland, USA (IEEE Computer Society, Los Alamitos, 1997), pp. 141–151

    Google Scholar 

  102. C. Morgan, The shadow knows: refinement and security in sequential programs. Sci. Comput. Program. 74(8), 629–653 (2009)

    Article  MATH  Google Scholar 

  103. R.M. Needham, M. Schroeder, Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  104. T. Nipkow, L.C. Paulson, M. Wenzel, Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283 (Springer, Berlin, 2002)

    MATH  Google Scholar 

  105. P.C. van Oorschot, Extending cryptographic logics of belief to key agreement protocols, in 1st ACM Conference on Computer and Communications Security (ACM CCS’93), ed. by D.E. Denning, R. Pyle, R. Ganesan, R.S. Sandhu, V. Ashby, Fairfax, USA (ACM, New York, 1993), pp. 232–243

    Chapter  Google Scholar 

  106. S. Owicki, D. Gries, An axiomatic proof technique for parallel programs I. Acta Inform. 6(4), 319–340 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  107. A. Pankova, P. Laud, Symbolic analysis of cryptographic protocols containing bilinear pairings, in 25th IEEE Computer Security Foundations Symposium (CSF’12), ed. by S. Chong, Cambridge, USA (IEEE Computer Society, Los Alamitos, 2012), pp. 63–77

    Chapter  Google Scholar 

  108. L.C. Paulson, Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828 (Springer, Berlin, 1994)

    MATH  Google Scholar 

  109. L.C. Paulson, Proving properties of security protocols by induction, in 10th IEEE Computer Security Foundations Workshop (CSFW’97), Rockport, Massachusetts (IEEE Computer Society, Los Alamitos, 1997), pp. 70–83

    Chapter  Google Scholar 

  110. L.C. Paulson, The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1–2), 85–128 (1998)

    Google Scholar 

  111. L.C. Paulson, Inductive analysis of the Internet protocol TLS. ACM Trans. Inf. Syst. Secur. 2(3), 332–351 (1999)

    Article  Google Scholar 

  112. L.C. Paulson, Relations between secrets: two formal analyses of the Yahalom protocol. J. Comput. Secur. 9(3), 197–216 (2001)

    MathSciNet  Google Scholar 

  113. L.C. Paulson, SET cardholder registration: the secrecy proofs, in 1st International Joint Conference on Automated Reasoning (IJCAR’01), ed. by R. Goré, A. Leitsch, T. Nipkow. Lecture Notes in Artificial Intelligence, vol. 2083 (Springer, Berlin, 2001), pp. 5–12

    Google Scholar 

  114. A. Pnueli, The temporal logic of programs, in 18th IEEE Symposium on Foundations of Computer Science (FOCS’77), Providence, USA (IEEE Computer Society, Los Alamitos, 1977), pp. 46–57

    Google Scholar 

  115. G.J. Popek, C.S. Kline, Encryption and secure computer networks. ACM Comput. Surv. 11(4), 331–356 (1979)

    Article  Google Scholar 

  116. J.D. Ramsdell, The cryptographic protocol shapes analyzer (CPSA). http://hackage.haskell.org/package/cpsa (accessed 18 Sept 2012)

  117. A.W. Roscoe, Intensional specifications of security protocols, in 9th IEEE Computer Security Foundations Workshop (CSFW’96), Dromquinna Manor, Kenmare, Ireland (IEEE Computer Society, Los Alamitos, 1996), pp. 28–38

    Chapter  Google Scholar 

  118. M. Rusinowitch, M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, in 14th IEEE Computer Security Foundations Workshop (CSFW’01), Cape Breton, Canada (IEEE Computer Society, Los Alamitos, 2001), pp. 174–187

    Chapter  Google Scholar 

  119. M. Rusinowitch, M. Turuani, Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theor. Comput. Sci. 299(1–3), 451–475 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  120. P.Y.A. Ryan, S. Schneider, Modelling and Analysis of Security Protocols: The CSP Approach (Addison-Wesley, Reading, 2001)

    Google Scholar 

  121. R. Sasse, S. Escobar, C. Meadows, J. Meseguer, Protocol analysis modulo combination of theories: a case study in Maude-NPA, in 6th International Workshop on Security and Trust Management (STM’10), ed. by J. Cuéllar, J. Lopez, G. Barthe, A. Pretschner, Athens, Greece. Lecture Notes in Computer Science, vol. 6710 (Springer, Berlin, 2010), pp. 163–178

    Google Scholar 

  122. B. Schmidt, S. Meier, C.J.F. Cremers, D.A. Basin, Automated analysis of Diffie-Hellman protocols and advanced security properties, in 25th IEEE Computer Security Foundations Symposium (CSF’12), ed. by S. Chong, Cambridge, USA (IEEE Computer Society, Los Alamitos, 2012), pp. 78–94

    Chapter  Google Scholar 

  123. S. Schneider, Security properties and CSP, in 17th IEEE Symposium on Security & Privacy (S&P’96), Oakland, USA (IEEE Computer Society, Los Alamitos, 1996), pp. 174–187

    Google Scholar 

  124. B. Smyth, M.D. Ryan, S. Kremer, M. Kourjieh, Towards automatic analysis of election verifiability properties, in Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS’10), ed. by A. Armando, G. Lowe, Paphos, Cyprus. Lecture Notes in Computer Science, vol. 6186 (Springer, Berlin, 2011), pp. 146–163

    Chapter  Google Scholar 

  125. D. Song, Athena: a new efficient automatic checker for security protocol analysis, in 12th IEEE Computer Security Foundations Workshop (CSFW’99), Mordano, Italy (IEEE Computer Society, Los Alamitos, 1999), pp. 192–202

    Google Scholar 

  126. D. Song, S. Berezin, A. Perrig, Athena: a novel approach to efficient automatic security protocol analysis. J. Comput. Secur. 9(1–2), 47–74 (2001)

    Google Scholar 

  127. C. Sprenger, D.A. Basin, Refining key establishment, in 25th IEEE Computer Security Foundations Symposium (CSF’12), ed. by S. Chong, Cambridge, USA (2012), pp. 230–246

    Chapter  Google Scholar 

  128. S.G. Stubblebine, R.N. Wright, An authentication logic with formal semantics supporting synchronization, revocation, and recency. IEEE Trans. Softw. Eng. 28(3), 256–285 (2002)

    Article  Google Scholar 

  129. P.F. Syverson, P.C. van Oorschot, A unified cryptographic protocol logic. CHACS Report 5540-227 NRL (1996)

    Google Scholar 

  130. F.J. Thayer, J.C. Herzog, J.D. Guttman, Honest ideals on Strand Spaces, in 11th IEEE Computer Security Foundations Workshop (CSFW’98), Rockport, USA (IEEE Computer Society, Los Alamitos, 1998), pp. 66–77

    Google Scholar 

  131. F.J. Thayer, J.C. Herzog, J.D. Guttman, Mixed Strand Spaces, in 12th IEEE Computer Security Foundations Workshop (CSFW’99), Mordano, Italy (IEEE Computer Society, Los Alamitos, 1999), pp. 72–82

    Chapter  Google Scholar 

  132. F.J. Thayer, J.C. Herzog, J.D. Guttman, Strand Spaces: proving security protocols correct. J. Comput. Secur. 7(2–3), 191–230 (1999)

    Google Scholar 

  133. F.L. Tiplea, C. Enea, C.V. Birjoveneanu, Decidability and complexity results for security protocols, in Verification of Infinite-State Systems with Applications to Security (VISSAS’05), ed. by E.M. Clarke, M. Minea, F.L. Tiplea, Timisoara, Romania. NATO Security Through Science Series D: Information and Communication Security, vol. 1 (IOS Press, Lansdale, 2006), pp. 185–211

    Google Scholar 

  134. M. Turuani, The CL-Atse protocol analyser, in 17th International Conference on Rewriting Techniques and Applications (RTA’06), ed. by F. Pfenning, Seattle, USA. Lecture Notes in Computer Science, vol. 4098 (Springer, Berlin, 2006), pp. 227–286

    Google Scholar 

  135. W.G. Tzeng, C.M. Hu, Inter-protocol interleaving attacks on some authentication and key distribution protocols. Inf. Process. Lett. 69(6), 297–302 (1999)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, ETH Zürich, Zürich, Switzerland

    Cas Cremers

  2. Computer Science and Communications Research Unit, University of Luxembourg, Luxembourg, Luxembourg

    Sjouke Mauw

Authors
  1. Cas Cremers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sjouke Mauw
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Cremers, C., Mauw, S. (2012). Historical Background and Further Reading. In: Operational Semantics and Verification of Security Protocols. Information Security and Cryptography. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78636-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78636-8_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78635-1

  • Online ISBN: 978-3-540-78636-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation