[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later

  • Chapter
  • First Online:
Logic, Rewriting, and Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9200))

Abstract

In 2003 I published a paper “Formal Methods in Cryptographic Protocol Analysis: Emerging Issues and Trends”, in which I identified the various open problems related to applying formal methods to the analysis of cryptographic protocols as we saw them then, and discussed the state of the art and the problems that still needed to be solved. Twelve years later, it is time for a an update and a reassessment. In this paper I revisit the open problems that I addressed in the original paper, discussing the progress that has been made in the intervening years, and the problems that still remain to be solved. I also discuss some new open problems that have arisen since then.

The rights of this work are transferred to the extent transferable according to title 17 §105 U.S.C.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • Compact, lightweight 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

Similar content being viewed by others

Notes

  1. 1.

    CryptoVerif also provides a completely automated option, but it is the interactive one that seems to be usually applied.

References

  1. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D., (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 17-19 January 2001, pp. 104–115, London, UK. ACM (2001)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. Adida, B., De Marneffe, O., Pereira, O., Quisquater, J.-J.: Electing a university president using open-audit voting: analysis of real-world use of helios. In: Electrionic Voting Technology/Workshop on Trustworthy Elections: EVT/WOTE (2009). https://www.usenix.org/legacy/event/evtwote09/tech/

  4. Adida, B.: Helios: web-based open-audit voting. In: van Oorschot, P.C. (ed.) Proceedings of the 17th USENIX Security Symposium, 28 July - 1 August 2008, San Jose, CA, USA, pp. 335–348. USENIX Association (2008)

    Google Scholar 

  5. Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, 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.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Arnaud, M., Cortier, V., Delaune, S.: Deciding security for protocols with recursive tests. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 49–63. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Backes, M., Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Cryptographically sound security proofs for basic and public-key kerberos. Int. J. Inf. Sec. 10(2), 107–134 (2011)

    Article  Google Scholar 

  8. Backes, M., Goldberg, I., Kate, A., Mohammadi, E.: Provably secure and practical onion routing. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, 25–27 June 2012, Cambridge, MA, USA, pp. 369–385. IEEE (2012)

    Google Scholar 

  9. Backes, M., Hofheinz, D., Unruh, D.: Cosp: a general framework for computational soundness proofs. In: Al-Shaer, E., Jha, S., Keromytis, A.D. (eds.) Proceedings of the 2009 ACM Conference on Computer and Communications Security, CCS 2009, Chicago, Illinois, USA, 9-13 November2009, pp. 66–78. ACM (2009)

    Google Scholar 

  10. Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Alt, H., Habib, M. (eds.) STACS 2003. Lecture Notes in Computer Science, vol. 2607, pp. 675–686. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive 2003:15 (2003)

    Google Scholar 

  12. Bana, G., Comon-Lundh, H.: Towards unconditional soundness: computationally complete symbolic attacker. In: Degano, P., Guttman, J.D. (eds.) [38], pp.189–208

    Google Scholar 

  13. Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: Ahn, G-J., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, 3–7 November 2014, pp. 609–620. ACM (2014)

    Google Scholar 

  14. Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Lakhnech, Y., Schmidt, B., Béguelin, S.Z.: Fully automated analysis of padding-based encryption in the computational model. In: Sadeghi, A.R., Gligor, V.D., Yung, M. (eds.) 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, Berlin, Germany, 4–8 November 2013 pp. 1247–1260. ACM (2013)

    Google Scholar 

  15. Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652–663. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

  18. Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Autom. Reasoning 36(1–2), 5–37 (2006)

    Article  MATH  Google Scholar 

  19. Bellare, M.: New proofs for NMAC and HMAC: security without collision-resistance. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 602–619. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Bernhard, D., Cortier, V., Pereira, O., Smyth, B., Warinschi, B.: Adapting helios for provable ballot privacy. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 335–354. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  22. Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proceedings of 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26–29 June 2005, Chicago, IL, USA, pp. 331–340. IEEE Computer Society, Chicago (2005)

    Google Scholar 

  23. Blaze, M.: Toward a broader view of security protocols. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2004. LNCS, vol. 3957, pp. 106–120. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Bond, M.: A chosen key difference attack on control vectors (2000). http://www.cl.cam.ac.uk/mkb23/research.html

  25. Boyd, C., Mao, W.: Design and analysis of key exchange protocols via secure channel identification. In: Safavi-Naini, R., Pieprzyk, J.P. (eds.) ASIACRYPT 1994. LNCS, vol. 917, pp. 171–181. Springer, Heidelberg (1995)

    Google Scholar 

  26. Brands, S., Chaum, D.: Distance bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344–359. Springer, Heidelberg (1994)

    Google Scholar 

  27. Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. In: SOSP, pp. 1–13 (1989)

    Google Scholar 

  28. Burton, C., Culnane, C., Heather, J., Peacock, T., Ryan, P.Y.A., Schneider, S., Teague, V., Wen, R., Xia, Z., Srinivasan, S.: Using prêt à voter in victoria state elections. In: Halderman, J.A., Pereira, O. (eds.) 2012 Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, EVT/WOTE 2012, Bellevue, WA, USA, 6–7 August 2012. USENIX Association (2012)

    Google Scholar 

  29. Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A., Walstad, C.: Formal analysis of kerberos 5. Theor. Comput. Sci. 367(1–2), 57–87 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  30. Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, Las Vegas, Nevada, USA, 14–17 October 2001, pp. 136–145. IEEE Computer Society (2001)

    Google Scholar 

  31. Carback, R., Chaum, D., Clark, J., Conway, J., Essex, A., Herrnson, P.S., Mayberry, T., Popoveniuc, S., Rivest, R.L., Shen, E., Sherman, A.T., Vora, P.L.: Scantegrity II municipal election at takoma park: the first E2E binding governmental election with ballot privacy. In: Proceedings of 19th USENIX Security Symposium, Washington, DC, USA, 11–13 August 2010, pp. 291–306. USENIX Association (2010)

    Google Scholar 

  32. Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: A secure voting system. Technical report, Cornell University (2007)

    Google Scholar 

  33. Comon-Lundh, H., Cortier, V.: How to prove security of communication protocols? a discussion on the soundness of formal models w.r.t. computational ones. In: Schwentick, T., Dürr, C. (eds.) 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, 10–12 March 2011, Dortmund, Germany, vol. 9, LIPIcs, pp. 29–44. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)

    Google Scholar 

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

    Chapter  Google Scholar 

  35. Cortier, V., Degrieck, J., Delaune, S.: Analysing routing protocols: four nodes topologies are sufficient. In: Degano, P., Guttman, J.D. (eds.) [38], pp. 30–50

    Google Scholar 

  36. Cortier, V., Smyth, B.: Attacking and fixing helios: an analysis of ballot secrecy. J. Comput. Secur. 21(1), 89–148 (2013)

    Article  Google Scholar 

  37. Cryptosense. Cryptosense web page. cryptosense.com

  38. Degano, P., Guttman, J.D. (eds.): POST 2012. LNCS, vol. 7215. Springer, Heidelberg (2012)

    Google Scholar 

  39. Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  40. Dolev, D., Yao, A, C-C.: On the security of public key protocols (extended abstract). In: 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28–30 October 1981, pp. 350–357. IEEE Computer Society (1981)

    Google Scholar 

  41. Ellison, C.M.: Ceremony design and analysis. IACR Cryptology ePrint Archive 2007:399 (2007)

    Google Scholar 

  42. Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C.A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 231–248. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  43. Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7–8), 898–928 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  44. Feigenbaum, J., Johnson, A., Syverson, P.F.: Probabilistic analysis of onion routing in a black-box model. ACM Trans. Inf. Syst. Secur. 15(3), 14 (2012)

    Article  Google Scholar 

  45. Focardi, R., Luccio, F.L., Steel, G.: An introduction to security API analysis. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 35–65. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  46. Goldschlag, D.M., Reed, M.G., Syverson, P.F.: Onion routing. Commun. ACM 42(2), 39–41 (1999)

    Article  Google Scholar 

  47. Groß, T., Mödersheim, s.: Vertical protocol composition. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27–29 June 2011, pp. 235–250. IEEE Computer Society (2011)

    Google Scholar 

  48. Groza, B., Warinschi, B.: Cryptographic puzzles and dos resilience, revisited. Des. Codes Crypt. 73(1), 177–207 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  49. Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive 2005:181 (2005)

    Google Scholar 

  50. Juels, A., Brainard, J.G.: Client puzzles: a cryptographic countermeasure against connection depletion attacks. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 1999, San Diego, California, USA. The Internet Society (1999)

    Google Scholar 

  51. Kemmerer, R.A.: Using formal verification techniques to analyze encryption protocols. In: Proceedings of the 1987 IEEE Symposium on Security and Privacy, Oakland, California, USA, 27–29 April 1987, pp. 134–139. IEEE Computer Society (1987)

    Google Scholar 

  52. Khader, D., Tang, Q., Ryan, P.Y.A.: Proving prêt à voter receipt free using computational security models. In: 2013 Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, EVT/WOTE 2013, Washington, D.C., USA, 12–13 August 2013. USENIX Association (2013)

    Google Scholar 

  53. Kürtz, K.O., Küsters, R., Wilke, T.: Selecting theories and nonce generation for recursive protocols. In: Ning, P., Atluri, V., Gligor, V.D., Mantel, H. (eds.) Proceedings of the 2007 ACM workshop on Formal methods in security engineering, FMSE 2007, Fairfax, VA, USA, 2 November 2007, pp. 61–70. ACM (2007)

    Google Scholar 

  54. Küsters, R., Truderung, T.: An epistemic approach to coercion-resistance for electronic voting protocols. In: 30th IEEE Symposium on Security and Privacy (S&P 2009), 17–20 May 2009, Oakland, California, USA, pp. 251–266. IEEE Computer Society (2009)

    Google Scholar 

  55. Küsters, R., Truderung, T., Vogt, A.: Proving coercion-resistance of scantegrity II. In: Soriano, M., Qing, S., López, J. (eds.) ICICS 2010. LNCS, vol. 6476, pp. 281–295. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  56. Küsters, R., Wilke, T.: Automata-based analysis of recursive cryptographic protocols. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 382–393. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  57. Lowe, G.: Analysing protocols subject to guessing attacks. In: WITS 2002 (2002)

    Google Scholar 

  58. Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19–22 July 2014, pp. 140–152. IEEE (2014)

    Google Scholar 

  59. Maurer, U.M., Schmid, P.E.: A calculus for security bootstrapping in distributed systems. J. Comput. Secur. 4(1), 55–80 (1996)

    Article  Google Scholar 

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

    Article  Google Scholar 

  61. Meadows, C.: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: 1999 IEEE Symposium on Security and Privacy, Oakland, California, USA, 9–12 May 1999, pp. 216–231. IEEE Computer Society (1999)

    Google Scholar 

  62. Meadows, C.: A cost-based framework for analysis of denial of service networks. J. Comput. Secur. 9(1/2), 143–164 (2001)

    Article  Google Scholar 

  63. Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)

    Article  Google Scholar 

  64. Meadows, C., Syverson, P.F.: A formal specification of requirements for payment transactions in the SET protocol. In: Hirschfeld, R. (ed.) FC 1998. LNCS, vol. 1465, pp. 122–140. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  65. Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  66. Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0. In: Rubin, A.D.: (ed.) Proceedings of the 7th USENIX Security Symposium, San Antonio, TX, USA, 26–29 January 1998. USENIX Association (1998)

    Google Scholar 

  67. Mödersheim, S., Viganò, L.: Sufficient conditions for vertical composition of security protocols. In: Moriai, S., Jaeger, T., Sakurai, K. (eds.) 9th ACM Symposium on Information, Computer and Communications Security, ASIA CCS 2014, Kyoto, Japan, 03–06 June 2014, pp. 435–446. ACM (2014)

    Google Scholar 

  68. Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org

  69. Paiola, M., Blanchet, B.: Verification of security protocols with lists: From length one to unbounded length. J. Comput. Secur. 21(6), 781–816 (2013)

    Article  MATH  Google Scholar 

  70. Pavlovic, D., Meadows, C.: Deriving ephemeral authentication using channel axioms. In: Christianson, B., Malcolm, J.A., Matyáš, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 240–261. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  71. Pavlovic, D., Meadows, C.: Actor-network procedures. In: Ramanujam, R., Ramaswamy, S. (eds.) ICDCIT 2012. LNCS, vol. 7154, pp. 7–26. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  73. Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of diffie-hellman-based protocols. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 312–329. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  74. Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is np-complete. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11–13 June 2001, Cape Breton, Nova Scotia, Canada, p. 174. IEEE Computer Society (2001)

    Google Scholar 

  75. Ryan, P.Y.A., Bismark, D., Heather, J., Schneider, S., Xia, Z.: Prêt à voter: a voter-verifiable voting system. IEEE Trans. Inf. Forensics Secur. 4(4), 662–673 (2009)

    Article  Google Scholar 

  76. Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using Maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162–177. Springer, Heidelberg (2014)

    Google Scholar 

  77. Schneider, S., Teague, V., Culnane, C., Heather, J.: Special section on vote-id 2013. J. Inf. Sec. Appl. 19(2), 103–104 (2014)

    Google Scholar 

  78. SET Secure Electronic Transactions LLC. SET Secure Electronic Transactions, Version 1.0 (2002). http://www.exelana.com/set/

  79. Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004:332 (2004)

    Google Scholar 

  80. Thayer, J.F., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999)

    Article  Google Scholar 

  81. Tor Project. The Tor Project: Anonymity Online. https://www.torproject.org/

  82. Truderung, T.: Selecting theories and recursive protocols. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 217–232. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  83. Vaudenay, S.: Secure communications over insecure channels based on short authenticated strings. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 309–326. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Acknowlegements

I would like to thank José Meseguer for our long and fruitful collaboration, much of which has resulted in research described in this paper. Furthermore, I would like to thank all the other researchers whose efforts have contributed to the work described in this paper, especially those that I have had the good fortune to collaborate with. Finally, I would like to thank Anupam Datta for suggesting that an update of my 2003 paper might be of interest to readers.

Author information

Authors and Affiliations

  1. Naval Research Laboratory, Washington, D.C., WA, USA

    Catherine Meadows

Authors
  1. Catherine Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Catherine Meadows .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Meadows, C. (2015). Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23165-5_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23164-8

  • Online ISBN: 978-3-319-23165-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation