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:
Timing-Sensitive Noninterference through Composition Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols

verfasst von : Jannik Dreier, Charles Duménil, Steve Kremer, Ralf Sasse

Erschienen in: Principles of Security and Trust

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

The Tamarin prover is a state-of-the-art protocol verification tool. It supports verification of both trace and equivalence properties, a rich protocol specification language that includes support for global, mutable state and allows the user to specify cryptographic primitives as an arbitrary subterm convergent equational theory, in addition to several built-in theories, which include, among others, Diffie-Hellman exponentiation.
In this paper, we improve the underlying theory and the tool to allow for more general user-specified equational theories: our extension supports arbitrary convergent equational theories that have the finite variant property, making Tamarin the first tool to support at the same time this large set of user-defined equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties. We demonstrate the effectiveness of this generalization by analyzing several protocols that rely on blind signatures, trapdoor commitment schemes, and ciphertext prefixes that were previously out of scope.

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 Automated Verification of Dynamic Root of Trust Protocols
Nächstes Kapitel On Communication Models When Verifying Equivalence Properties
Fußnoten
1
For private function symbols the deconstruction rule must be usable up to n times, as there is no corresponding construction rule.
 
Literatur
1.
Adida, B.: Helios: web-based open-audit voting. In: Proceedings of the 17th USENIX Security Symposium, pp. 335–348. USENIX Association (2008)
2.
3.
Arapinis, M., Ritter, E., Ryan, M.: StatVerif: verification of stateful processes. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF 2011), pp. 33–47. IEEE Press (2011)
4.
Armando, A., et al.: 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). doi:10.​1007/​11513988_​27 CrossRef
5.
6.
Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. ACM (2015)
7.
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Logic Algebraic Program. 75(1), 3–51 (2008)MathSciNetCrossRefMATH
8.
Blanchet, B., Smyth, B.: Automated reasoning for equivalences in the applied pi calculus with barriers. In: Proceedings of the 29th Computer Security Foundations Symposium (CSF 2016), pp. 310–324. IEEE Computer Society (2016)
9.
Blanchet, B., Smyth, B., Cheval, V.: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial (2016)
10.
Chadha, R., Cheval, V., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocol. ACM Trans. Comput. Logic, 17(4) (2016). Article 23
11.
Chaum, D.: Blind signatures for untraceable payments. In: Advances in Cryptology: Proceedings of CRYPTO 1982, pp. 199–203. Plenum Press (1982)
12.
Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: negative tests and non-determinism. In: 18th Conference on Computer and Communications Security (CCS 2011). ACM, Chicago, October 2011
13.
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). doi:10.​1007/​978-3-540-32033-3_​22 CrossRef
14.
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006)CrossRef
15.
Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-70545-1_​38 CrossRef
16.
Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17, 435–487 (2009)CrossRefMATH
17.
18.
Dreier, J., Kassem, A., Lafourcade, P.: Formal analysis of e-cash protocols. In: SECRYPT 2015 - Proceedings of the 12th International Conference on Security and Cryptography, pp. 65–75. SciTePress (2015)
19.
Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-03829-7_​1 CrossRef
20.
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Logic Algebraic Program. 81(7–8), 898–928 (2012)MathSciNetCrossRefMATH
21.
Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: Seberry, J., Zheng, Y. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993). doi:10.​1007/​3-540-57220-1_​66 CrossRef
22.
23.
Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: ACM Workshop on Privacy in the Electronic Society (WPES 2005), pp. 61–70. ACM (2005)
24.
25.
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). doi:10.​1007/​978-3-642-39799-8_​48 CrossRef
26.
Okamoto, T.: An electronic voting scheme. In: IFIP World Conference on IT Tools, pp. 21–30 (1996)
27.
Ramsdell, J.D., Dougherty, D.J., Guttman, J.D., Rowe, P.D.: A hybrid analysis for security protocols with state. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 272–287. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-10181-1_​17
28.
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). doi:10.​1007/​978-3-319-11851-2_​11
29.
Schmidt, B.: Formal Analysis of Key Exchange Protocols and Physical Protocols. Ph.D. dissertation, ETH Zurich (2012)
30.
Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE (2012)
31.
Metadaten
Titel
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
verfasst von
Jannik Dreier
Charles Duménil
Steve Kremer
Ralf Sasse
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
Buch
Principles of Security and Trust

Print ISBN: 978-3-662-54454-9

Electronic ISBN: 978-3-662-54455-6

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-662-54455-6_6