Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
José Meseguer: Scientist and Friend Extraordinaire Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

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

verfasst von : Catherine Meadows

Erschienen in: Logic, Rewriting, and Concurrency

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
Nächstes Kapitel A Denotational Semantic Theory of Concurrent Systems
Fußnoten
1
CryptoVerif also provides a completely automated option, but it is the interactive one that seems to be usually applied.
 
Literatur
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)
2.
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 15(2), 103–127 (2002)MathSciNetCrossRefMATH
3.
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)
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) CrossRef
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) CrossRef
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)CrossRef
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)
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)
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)CrossRef
11.
Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive 2003:15 (2003)
12.
Bana, G., Comon-Lundh, H.: Towards unconditional soundness: computationally complete symbolic attacker. In: Degano, P., Guttman, J.D. (eds.) [38], pp.189–208
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)
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)
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) CrossRef
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) CrossRef
17.
Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. 21(1), 77–87 (2003)CrossRefMATH
18.
Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Autom. Reasoning 36(1–2), 5–37 (2006)CrossRefMATH
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) CrossRef
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) CrossRef
21.
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Sec. Comput. 5(4), 193–207 (2008)CrossRef
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)
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) CrossRef
24.
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)
26.
Brands, S., Chaum, D.: Distance bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344–359. Springer, Heidelberg (1994)
27.
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. In: SOSP, pp. 1–13 (1989)
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)
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)MathSciNetCrossRefMATH
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)
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)
32.
Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: A secure voting system. Technical report, Cornell University (2007)
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)
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) CrossRef
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
36.
Cortier, V., Smyth, B.: Attacking and fixing helios: an analysis of ballot secrecy. J. Comput. Secur. 21(1), 89–148 (2013)CrossRef
37.
38.
Degano, P., Guttman, J.D. (eds.): POST 2012. LNCS, vol. 7215. Springer, Heidelberg (2012)
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) CrossRef
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)
41.
Ellison, C.M.: Ceremony design and analysis. IACR Cryptology ePrint Archive 2007:399 (2007)
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) CrossRef
43.
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7–8), 898–928 (2012)MathSciNetCrossRefMATH
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)CrossRef
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) CrossRef
46.
Goldschlag, D.M., Reed, M.G., Syverson, P.F.: Onion routing. Commun. ACM 42(2), 39–41 (1999)CrossRef
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)
48.
49.
Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive 2005:181 (2005)
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)
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)
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)
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)
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)
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) CrossRef
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) CrossRef
57.
Lowe, G.: Analysing protocols subject to guessing attacks. In: WITS 2002 (2002)
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)
59.
Maurer, U.M., Schmid, P.E.: A calculus for security bootstrapping in distributed systems. J. Comput. Secur. 4(1), 55–80 (1996)CrossRef
60.
Meadows, C.: Applying formal methods to the analysis of a key management protocol. J. Comput. Secur. 1(1), 5–36 (1992)CrossRef
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)
62.
Meadows, C.: A cost-based framework for analysis of denial of service networks. J. Comput. Secur. 9(1/2), 143–164 (2001)CrossRef
63.
Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)CrossRef
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) CrossRef
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) CrossRef
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)
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)
68.
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)CrossRefMATH
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) CrossRef
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) CrossRef
72.
Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. 1(1), 66–92 (1998)CrossRef
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) CrossRef
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)
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)CrossRef
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)
77.
Schneider, S., Teague, V., Culnane, C., Heather, J.: Special section on vote-id 2013. J. Inf. Sec. Appl. 19(2), 103–104 (2014)
78.
79.
Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004:332 (2004)
80.
Thayer, J.F., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999)CrossRef
81.
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) CrossRef
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) CrossRef
Metadaten
Titel
Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later
verfasst von
Catherine Meadows
Copyright-Jahr
2015
Buch
Logic, Rewriting, and Concurrency

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

Electronic ISBN: 978-3-319-23165-5

Copyright-Jahr: 2015

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