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:
Analyzing and Fixing the QACCE Security of QUIC Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Cross-Tool Semantics for Protocol Security Goals

verfasst von : Joshua D. Guttman, John D. Ramsdell, Paul D. Rowe

Erschienen in: Security Standardisation Research

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Formal protocol analysis tools provide objective evidence that a protocol under standardization meets security goals, as well as counterexamples to goals it does not meet (“attacks”). Different tools are however based on different execution semantics and adversary models. If different tools are applied to alternative protocols under standardization, can formal evidence offer a yardstick to compare the results?
We propose a family of languages within first order predicate logic to formalize protocol safety goals (rather than indistinguishability). Although they were originally designed for the strand space formalism that supports the tool cpsa, we show how to translate them to goals for the applied \(\pi \) calculus that supports the tool ProVerif. We give a criterion for protocols expressed in the two formalisms to correspond, and prove that if a protocol in the strand space formalism satisfies a goal, then a corresponding applied \(\pi \) process satisfies the translation of that goal. We show that the converse also holds for a class of goal formulas, and conjecture a broader equivalence. We also describe a compiler that, from any protocol in the strand space formalism, constructs a corresponding applied \(\pi \) process and the relevant goal translation.

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 Analyzing and Fixing the QACCE Security of QUIC
Nächstes Kapitel Cryptanalysis of GlobalPlatform Secure Channel Protocols
Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115, January 2001
2.
Almousa, O., Mödersheim, S., Viganò, L.: Alice and Bob: reconciling formal models and implementation. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 66–85. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-25527-9_​7 CrossRef
3.
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
4.
Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28756-5_​19 CrossRef
5.
Basin, D.A., Cremers, C.J.F., Miyazaki, K., Radomirovic, S., Watanabe, D.: Improving the security of cryptographic protocol standards. IEEE Secur. Priv. 13(3), 24–31 (2015)CrossRef
6.
Bistarelli, S., Cervesato, I., Lenzini, G., Martinelli, F.: Relating multiset rewriting and process algebras for security protocol analysis. J. Comput. Secur. 13(1), 3–47 (2005)CrossRef
7.
Blanchet, B.: An efficient protocol verifier based on Prolog rules. In: 14th Computer Security Foundations Workshop, pp. 82–96. IEEE CS Press, June 2001
8.
Blanchet, B.: Vérification automatique de protocoles cryptographiques: modèle formel et modèle calculatoire. Automatic verification of security protocols: formal model and computational model. Mémoire d’habilitation à diriger des recherches, Université Paris-Dauphine, November 2008
9.
Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.93: Automatic Cryptographic Protocol Verifier. User Manual and Tutorial (2016)
10.
11.
Cervesato, I., Durgin, N.A., Lincoln, P.: A comparison between strand spaces and multiset rewriting for security protocol analysis. J. Comput. Secur. 13(2), 265–316 (2005)CrossRefMATH
12.
13.
Cortier, V., Dallon, A., Delaune, S.: Bounding the number of agents, for equivalence too. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 211–232. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49635-0_​11 CrossRef
14.
Cortier, V., Kremer, S. (eds.): Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series. IOS Press (2011)
15.
Crazzolara, F., Winskel, G.: Events in security protocols. In: Proceedings of the 8th ACM Conference on Computer and Communications Security, CCS 2001, 6–8 November 2001, Philadelphia, Pennsylvania, USA, pp. 96–105 (2001)
16.
Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012)CrossRefMATH
17.
18.
Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electron. Notes Theoret. Comput. Sci. 172, 311–358 (2007)MathSciNetCrossRefMATH
19.
Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105(2), 217–273 (1992)MathSciNetCrossRefMATH
20.
Gordon, A.D., Jeffrey, A.: Types, effects for asymmetric cryptographic protocols. J. Comput. Secur. 12(3–4), 435–484 (2004)CrossRef
21.
Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)MATH
22.
Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201–267 (2014)CrossRef
23.
ISO/IEC 29128: Information Technology-Security techniques–Verification of Cryptographic Protocols (2011)
24.
Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, 18–21 May 2014, Berkeley, CA, USA, pp. 163–178 (2014)
25.
Lynch, C., Meadows, C.A.: On the relative soundness of the free algebra model for public key encryption. Electron. Notes Theoret. Comput. Sci. 125(1), 43–54 (2005)CrossRefMATH
26.
Matsuo, S., Miyazaki, K., Otsuka, A., Basin, D.: How to evaluate the security of real-life cryptographic protocols? In: Sion, R., Curtmola, R., Dietrich, S., Kiayias, A., Miret, J.M., Sako, K., Sebé, F. (eds.) FC 2010. LNCS, vol. 6054, pp. 182–194. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14992-4_​16 CrossRef
27.
Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113–131 (1996)CrossRefMATH
28.
Meadows, C: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy. IEEE CS Press, May 1999
29.
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
30.
31.
Miller, D.: Encryption as an abstract data type. Electron. Notes Theoret. Comput. Sci. 84, 18–29 (2003)CrossRefMATH
32.
33.
Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. International Journal of Information Security (Accepted, Forthcoming)
34.
Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Oper. Syst. Rev. 28, 24–37 (1994)CrossRef
Metadaten
Titel
Cross-Tool Semantics for Protocol Security Goals
verfasst von
Joshua D. Guttman
John D. Ramsdell
Paul D. Rowe
Copyright-Jahr
2016
Buch
Security Standardisation Research

Print ISBN: 978-3-319-49099-1

Electronic ISBN: 978-3-319-49100-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-49100-4_2