Model Checking Security Protocols | SpringerLink
Skip to main content
Springer Nature Link
Log in

Model Checking Security Protocols

  • Chapter
  • First Online:
Handbook of Model Checking

  • 11k Accesses

Abstract

The formal analysis of security protocols is a prime example of a domain where model checking has been successfully applied. Although security protocols are typically small, analysis by hand is difficult as a protocol should work even when arbitrarily many runs are interleaved and in the presence of an adversary. Specialized model-checking techniques have been developed that address both the problems of unbounded, interleaved runs and a prolific, highly nondeterministic adversary. These techniques have been implemented in model-checking tools that now scale to protocols of realistic size and can be used to aid protocol design and standardization.

In this chapter, we provide an overview of the main applications of model checking in security protocol analysis. We explain the central concepts involved in the analysis of security protocols: the abstraction of messages, protocols as role automata, the adversary model, and property specification. We explain and relate the main algorithms used and describe systems based on them. We also give examples of the successful applications of model checking to protocol standards. Finally, we provide an outlook on the field: What is possible with the state of the art and what are the future challenges?

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1–2), 2–32 (2006)

    Article  MathSciNet  Google Scholar 

  2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 104–115. ACM, New York (2001)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  4. Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J.A. (eds.) Logics in Artificial Intelligence—Journées Européennes sur la Logique en Intelligence Artificielle (JELIA). LNCS, vol. 3229, pp. 730–733. Springer, Heidelberg (2004)

    Google Scholar 

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

    Article  Google Scholar 

  7. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

  8. Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symb. Comput. 21(2), 211–243 (1996)

    Article  MathSciNet  Google Scholar 

  9. Backes, M., Pfitzmann, B.: Limits of the cryptographic realization of Dolev–Yao-style XOR. In: di Vimercati, S.D.C., Syverson, P.F., Gollmann, D. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol. 3679, pp. 178–196. Springer, Heidelberg (2005)

    Google Scholar 

  10. Backes, M., Pfitzmann, B., Waidner, M.: Limits of the BRSIM/UC soundness of Dolev–Yao models with hashes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol. 4189, pp. 404–423. Springer, Heidelberg (2006)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  12. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  13. Balfanz, D., Smetters, D.K., Stewart, P., Wong, H.C.: Talking to strangers: authentication in ad-hoc wireless networks. In: Network and Distributed System Security Symp. (NDSS) (2002)

    Google Scholar 

  14. Basin, D.: Lazy infinite-state analysis of security protocols. In: Secure Networking—CQRE [Secure] ’99. LNCS, vol. 1740, pp. 30–42. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  15. Basin, D., Cremers, C.: Degrees of security: protocol guarantees in the face of compromising adversaries. In: Dawar, A., Veith, H. (eds.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol. 6247, pp. 1–18. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Basin, D., Cremers, C.: Modeling and analyzing security in the presence of compromising adversaries. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol. 6345, pp. 340–356. Springer, Heidelberg (2010)

    Google Scholar 

  17. Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO/IEC 9798 standard for entity authentication. In: Degano, P., Guttman, J.D. (eds.) Intl. Conf. Principles of Security and Trust (POST). LNCS, vol. 7215, pp. 129–148. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  18. Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. J. Assoc. Comput. Mach. 48(1), 70–109 (2001)

    Article  MathSciNet  Google Scholar 

  19. Basin, D., Mödersheim, S., Viganò, L.: Algebraic intruder deductions. In: Sutcliffe, G., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 3835, pp. 549–564. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  21. Basin, D., Čapkun, S., Schaller, P., Schmidt, B.: Let’s get physical: models and methods for real-world security protocols. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Intl. Conf. on Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 5674, pp. 1–22. Springer, Heidelberg (2009). Invited paper

    Chapter  Google Scholar 

  22. Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Atluri, V., Meadows, C., Juels, A. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp. 16–25. ACM, New York (2005)

    Google Scholar 

  23. Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. In: Treinen, R. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA). LNCS, vol. 5595, pp. 148–163. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. In: Treinen, R. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA), pp. 148–163. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  26. Baudet, M., Warinschi, B., Abadi, M.: Guessing attacks and the computational soundness of static equivalence. J. Comput. Secur. 18(5), 909–968 (2010)

    Article  Google Scholar 

  27. Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp. 459–468. ACM, New York (2008)

    Google Scholar 

  28. Bhargavan, K., Fournet, C., Gordon, A.D., Swamy, N.: Verified implementations of the information card federated identity-management protocol. In: Abe, M., Gligor, V.D. (eds.) Symp. on Information, Computer and Communications Security (ASIACCS), pp. 123–135. ACM, New York (2008)

    Google Scholar 

  29. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW), pp. 82–96. IEEE, Piscataway (2001)

    Google Scholar 

  30. Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363–434 (2009)

    Article  Google Scholar 

  31. Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Symp. on Logic in Computer Science (LICS), pp. 331–340. IEEE, Piscataway (2005)

    Google Scholar 

  32. Brands, S., Chaum, D.: Distance-bounding protocols. In: Helleseth, T. (ed.) Workshop on the Theory and Application of Cryptographic Techniques (EUROCRYPT ’93), pp. 344–359. Springer, Heidelberg (1994)

    Google Scholar 

  33. Canetti, R., Krawczyk, H.: Analysis of key-exchange protocols and their use for building secure channels. In: Pfitzmann, B. (ed.) Intl. Conf. on the Theory and Application of Cryptographic Techniques (EUROCRYPT). LNCS, vol. 2045, pp. 453–474. Springer, Heidelberg (2001)

    Google Scholar 

  34. Ciobâca, S., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R.A. (ed.) Intl. Conf. on Automated Deduction (CADE), pp. 355–370. Springer, Heidelberg (2009)

    Google Scholar 

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

    Article  Google Scholar 

  36. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude—A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  37. Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA). LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)

    Google Scholar 

  38. Comon-Lundh, H., Treinen, R.: Easy intruder deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. LNCS, vol. 2772, pp. 225–242. Springer, Heidelberg (2003)

    Google Scholar 

  39. Conchinha, B., Basin, D., Caleiro, C.: Efficient decision procedures for message deducibility and static equivalence. In: Degano, P., Etalle, S., Guttman, J.D. (eds.) Intl. Workshop on Formal Aspects of Security and Trust (FAST 2010). LNCS, vol. 6561, pp. 34–49 (2011)

    Chapter  Google Scholar 

  40. Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Electron. Notes Theor. Comput. Sci. 121, 47–63 (2005)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  42. Cremers, C.: The Scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  43. Cremers, C.: Key exchange in IPsec revisited: formal analysis of IKEv1 and IKEv2. In: Atluri, V., Díaz, C. (eds.) European Conf. on Research in Computer Security (ESORICS), pp. 315–334. Springer, Heidelberg (2011)

    Google Scholar 

  44. Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.1. Tech. Rep. RFC 4346, Internet Engineering Task Force (2006)

    Google Scholar 

  45. Dolev, D., Even, S., Karp, R.M.: On the security of ping-pong protocols. Inf. Control 55(1–3), 57–68 (1982)

    Article  MathSciNet  Google Scholar 

  46. Dolev, D., Yao, A.C.C.: On the security of public key protocols (extended abstract). In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 350–357. IEEE, Piscataway (1981)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  48. Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12(2), 247–311 (2004)

    Article  Google Scholar 

  49. Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols (1999)

    MATH  Google Scholar 

  50. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) Foundations of Security Analysis and Design (FOSAD), 2007/2008/2009 Tutorial Lectures. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)

    Google Scholar 

  51. Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theor. Comput. Sci. 238(3), 103–119 (2009)

    Article  Google Scholar 

  52. Even, S., Goldreich, O., Shamir, A.: On the security of ping-pong protocols when implemented using the RSA. In: Williams, H.C. (ed.) Intl. Cryptology Conf. (CRYPTO). LNCS, vol. 218, pp. 58–72. Springer, Heidelberg (1985)

    Google Scholar 

  53. Guttman, J., Thayer, F.: Protocol independence through disjoint encryption. In: Computer Security Foundations Workshop (CSFW), pp. 24–34. IEEE, Piscataway (2000)

    Google Scholar 

  54. Harkins, D., Carrel, D., et al.: The internet key exchange (IKE) (1998)

    Google Scholar 

  55. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 3920, pp. 441–444 (2006)

    Google Scholar 

  56. Holzmann, G.: The model checker SPIN. Trans. Softw. Eng. 23(5), 279–295 (2002)

    Article  Google Scholar 

  57. Hopcroft, P.J., Lowe, G.: Analysing a stream authentication protocol using model checking. Int. J. Inf. Secur. 3(1), 2–13 (2004)

    Article  Google Scholar 

  58. Just, M., Vaudenay, S.: Authenticated multi-party key agreement. In: Kim, K., Matsumoto, T. (eds.) Advances in Cryptology (ASIACRYPT ’96). LNCS, vol. 1163, pp. 36–49 (1996)

    Chapter  Google Scholar 

  59. Kaufman, C., Hoffman, P., Nir, Y., Eronen, P.: Internet key exchange protocol version 2 (IKEV2). Tech. Rep. RFC 5996, Internet Engineering Task Force (September 2010)

    Google Scholar 

  60. Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol. 6345, pp. 389–404. Springer, Heidelberg (2010)

    Google Scholar 

  61. Küsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp. 129–138. ACM, New York (2008)

    Google Scholar 

  62. Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: Computer Security Foundations Symp. (CSF), pp. 157–171. IEEE, Piscataway (2009)

    Google Scholar 

  63. Lamport, L.: The temporal logic of actions. Trans. Program. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  64. Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Automatic analysis of a non-repudiation protocol. Electron. Notes Theor. Comput. Sci. 112, 113–129 (2005)

    Article  Google Scholar 

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

    Article  Google Scholar 

  66. Lowe, G.: Breaking and fixing the Needham–Schroeder public-key protocol using FDR. Softw., Concepts Tools 17(3), 93–102 (1996)

    Google Scholar 

  67. Lowe, G.: A hierarchy of authentication specifications. In: Computer Security Foundations Workshop (CSFW), pp. 31–44 (1997)

    Chapter  Google Scholar 

  68. Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1–2), 53–84 (1998)

    Article  Google Scholar 

  69. Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  70. Meadows, C.: Applying formal methods to the analysis of a key management protocol. J. Comput. Secur. 1(1), 5–36 (1992)

    Article  Google Scholar 

  71. Meadows, C.: The NRL Protocol Analyzer: an overview. J. Log. Program. 26(2), 113–131 (1996)

    Article  Google Scholar 

  72. Meadows, C.: Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer. In: Symp. on Security and Privacy (S & P), pp. 216–231. (1999)

    Google Scholar 

  73. Meadows, C., Poovendran, R., Pavlovic, D., Chang, L., Syverson, P.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Poovendran, R., Wang, C., Roy, S. (eds.) Secure Localization and Time Synchronization in Wireless Ad Hoc and Sensor Networks. Springer, Heidelberg (2006)

    Google Scholar 

  74. Meadows, C., Syverson, P.F., Cervesato, I.: Formal specification and analysis of the Group Domain of Interpretation Protocol using NPATRL and the NRL Protocol Analyzer. J. Comput. Secur. 12(6), 893–931 (2004)

    Article  Google Scholar 

  75. Menezes, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)

    Book  Google Scholar 

  76. Millen, J.K.: A necessarily parallel attack. In: Workshop on Formal Methods and Security Protocols (1999)

    Google Scholar 

  77. Millen, J.K.: On the freedom of decryption. Inf. Process. Lett. 86(6), 329–333 (2003)

    Article  MathSciNet  Google Scholar 

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

    Article  Google Scholar 

  79. Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Reiter, M.K., Samarati, P. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp. 166–175 (2001)

    Google Scholar 

  80. Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: Symp. on Security and Privacy (S & P), pp. 141–151. IEEE, Piscataway (1997)

    Google Scholar 

  81. Mödersheim, S., Viganò, L., Basin, D.: Constraint differentiation: search-space reduction for the constraint-based analysis of security protocols. J. Comput. Secur. 18(4), 575–618 (2010)

    Article  Google Scholar 

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

    Article  Google Scholar 

  83. Neuman, C., Hartman, S., Raeburn, K.: The Kerberos network authentication service (V5). Tech. Rep. RFC 4120, Internet Engineering Task Force (July 2005)

    Google Scholar 

  84. Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J. Comput. Secur. 14(6), 561–589 (2006)

    Article  Google Scholar 

  85. Peled, D.: Partial-order reduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  86. Perrig, A., Tygar, J.D.: Secure Broadcast Communication in Wired and Wireless Networks. Kluwer Academic, Norwell (2002)

    Google Scholar 

  87. Reiter, M., Rubin, A.: Crowds: anonymity for web transactions. Trans. Inf. Syst. Secur. 1(1), 66–92 (1998)

    Article  Google Scholar 

  88. Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Computer Security Foundations Workshop (CSFW), p. 174. IEEE, Piscataway (2001)

    Google Scholar 

  89. Schaller, P., Schmidt, B., Basin, D., Čapkun, S.: Modeling and verifying physical properties of security protocols for wireless networks. In: Computer Security Foundations Symp. (CSF), pp. 109–123. IEEE, Piscataway (2009)

    Google Scholar 

  90. Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations Symp. (CSF), pp. 78–94 (2012)

    Google Scholar 

  91. Schmidt-Schauß, M.: Unification in permutative theories is undecidable. J. Symb. Comput. 8, 415–421 (1989)

    Article  MathSciNet  Google Scholar 

  92. Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3), 355–377 (2004)

    Article  Google Scholar 

  93. Shoup, V.: On formal models for secure key exchange (version 4) (1999). Revision of IBM Research Report RZ 3120, (April 1999)

    Google Scholar 

  94. Song, D.X.A.: A new efficient automatic checker for security protocol analysis. In: Computer Security Foundations Workshop (CSFW), pp. 192–202 (1999)

    Google Scholar 

  95. Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) Correct Hardware Design and Verification Methods. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  96. Syverson, P.F., Meadows, C.: A formal language for cryptographic protocol requirements. Des. Codes Cryptogr. 7(1–2), 27–59 (1996)

    MathSciNet  MATH  Google Scholar 

  97. Thayer, F.J., Swarup, V., Guttman, J.D.: Metric strand spaces for locale authentication protocols. In: Nishigaki, M., Jøsang, A., Murayama, Y., Marsh, S. (eds.) IFIP International Conference on Trust Management (IFIPTM), vol. 321, pp. 79–94. Springer, Heidelberg (2010)

    Google Scholar 

  98. Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA). LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)

    Google Scholar 

  99. Čapkun, S., Hubaux, J.: Secure positioning in wireless networks. J. Sel. Areas Commun. 24(2), 221–232 (2006)

    Article  Google Scholar 

  100. Viganò, L.: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61–86 (2006)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ETH Zürich, Zürich, Switzerland

    David Basin

  2. University of Oxford, Oxford, UK

    Cas Cremers

  3. Naval Research Laboratory, Washington, DC, USA

    Catherine Meadows

Authors
  1. David Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cas Cremers
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Catherine Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cas Cremers .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Basin, D., Cremers, C., Meadows, C. (2018). Model Checking Security Protocols. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation