Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Analyzing and Fixing the QACCE Security of QUIC Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Cross-Tool Semantics for Protocol Security Goals

Authors : Joshua D. Guttman, John D. Ramsdell, Paul D. Rowe

Published in: Security Standardisation Research

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Analyzing and Fixing the QACCE Security of QUIC
next chapter Cryptanalysis of GlobalPlatform Secure Channel Protocols
Appendix
Available only for authorised users
Literature
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
Metadata
Title
Cross-Tool Semantics for Protocol Security Goals
Authors
Joshua D. Guttman
John D. Ramsdell
Paul D. Rowe
Copyright Year
2016
Book
Security Standardisation Research

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

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

Copyright Year: 2016

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

Premium Partner

    Image Credits