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:
Attribute-Based Encryption as a Service for Access Control in Large-Scale Organizations Read chapter Read first chapter

2018 | OriginalPaper | Chapter

Formal Analysis of Combinations of Secure Protocols

Authors : Elliott Blot, Jannik Dreier, Pascal Lafourcade

Published in: Foundations and Practice of Security

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

When trying to prove the security of a protocol, one usually analyzes the protocol in isolation, i.e., in a network with no other protocols. But in reality, there will be many protocols operating on the same network, maybe even sharing data including keys, and an intruder may use messages of one protocol to break another. We call that a multi-protocol attack. In this paper, we try to find such attacks using the Tamarin prover. We analyze both examples that were previously analyzed by hand or using other tools, and find novel attacks.

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 Secure Protocol of ABAC Certificates Revocation and Delegation
next chapter Formal Analysis of the FIDO 1.x Protocol
Literature
1.
Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6–15 (1996)CrossRef
2.
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). https://​doi.​org/​10.​1007/​11513988_​27 CrossRef
3.
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE Workshop on Computer Security Foundations, CSFW 2001, Washington, DC, USA, pp. 82–96. IEEE Computer Society (2001)
4.
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)CrossRefMATH
5.
Buttyan, L., Staamann, S., Wilhelm, U.: A simple logic for authentication protocol design. In: 11th IEEE Computer Security Foundations Workshop, pp. 153–162. IEEE Computer Society Press (1998)
6.
7.
Clark, J., Jacob, J.: A survey of authentication protocol literature: version 1.0 (1997)
8.
Clark, J.A., Jacob, J.: On the security of recent protocols. Inf. Process. Lett. 56(3), 151–155 (1995)CrossRefMATH
9.
C. Cremers. Feasibility of multi-protocol attacks. In: Proceedings of the First International Conference on Availability, Reliability and Security (ARES), Vienna, Austria, pp. 287–294. IEEE Computer Society (2006)
10.
11.
Cremers, C., Mauw, S., de Vink, E.: Injective synchronisation: an extension of the authentication hierarchy. Theor. Comput. Sci. 367(1), 139–161 (2006)MathSciNetCrossRefMATH
12.
Cremers, C.J.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, CCS 2008, pp. 119–128. ACM, New York (2008)
13.
Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Commun. ACM 24(8), 533–536 (1981)CrossRef
14.
Durgin, N.A., Mitchell, J.C., Pavlovic, D.: A compositional logic for proving security properties of protocols. J. Comput. Secur. 11(4), 677–722 (2003)CrossRef
15.
16.
Hwang, T., Chen, Y.-H.: On the security of SPLICE/AS - the authentication system in WIDE internet. Inf. Process. Lett. 53(2), 97–101 (1995)CrossRefMATH
17.
Kao, I.-L., Chow, R.: An efficient and secure authentication protocol using uncertified keys. SIGOPS Oper. Syst. Rev. 29(3), 14–21 (1995)CrossRef
18.
19.
Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–133 (1995)CrossRefMATH
20.
Lowe, G.: A hierarchy of authentication specification. In: 10th Computer Security Foundations Workshop (CSFW 1997), 10–12 June 1997, Rockport, Massachusetts, USA, pp. 31–44. IEEE Computer Society (1997)
21.
Lowe, G.: Towards a completeness result for model checking of security protocols. J. comput. secur. 7(2–3), 89–146 (1999)CrossRef
22.
Mathuria, A., Singh, A.R., Shravan, P.V., Kirtankar, R.: Some new multi-protocol attacks. In: Proceedings of the 15th International Conference on Advanced Computing and Communications, ADCOM 2007, Washington, DC, USA, pp. 465–471. IEEE Computer Society (2007)
23.
24.
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)CrossRefMATH
25.
Needham, R.M., Schroeder, M.D.: Authentication revisited. SIGOPS Oper. Syst. Rev. 21(1), 7 (1987)CrossRef
26.
Perrig, A., Song, D.: Looking for diamonds in the desert - extending automatic protocol generation to three-party authentication and key agreement protocols. In: Proceedings of the 13th IEEE Workshop on Computer Security Foundations, CSFW 2000, Washington, DC, USA, pp. 64–76. IEEE Computer Society (2000)
27.
Song, D.X., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. J. Comput. Secur. 9(1–2), 47–74 (2001)CrossRef
28.
Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. SIGOPS Oper. Syst. Rev. 28(3), 24–37 (1994)CrossRef
29.
Yamaguchi, S., Okayama, K., Miyahara, H.: The design and implementation of an authentication system for the wide area distributed environment. IEICE Trans. Inf. Syst. 74(11), 3902–3909 (1991)
30.
Zhou, H., Foley, S.N.: Fast automatic synthesis of security protocols using backward search. In: Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering, FMSE 2003, pp. 1–10. ACM, New York (2003)
Metadata
Title
Formal Analysis of Combinations of Secure Protocols
Authors
Elliott Blot
Jannik Dreier
Pascal Lafourcade
Copyright Year
2018
Book
Foundations and Practice of Security

Print ISBN: 978-3-319-75649-3

Electronic ISBN: 978-3-319-75650-9

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-319-75650-9_4

Premium Partner

    Image Credits