Skip to main content

2018 | OriginalPaper | Buchkapitel

Stateful Protocol Composition

verfasst von : Andreas V. Hess, Sebastian A. Mödersheim, Achim D. Brucker

Erschienen in: Computer Security

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

We prove a parallel compositionality result for protocols with a shared mutable state, i.e., stateful protocols. For protocols satisfying certain compositionality conditions our result shows that verifying the component protocols in isolation is sufficient to prove security of their composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants maintain shared databases. Because of the generality of our result we also cover many forms of sequential composition as a special case of stateful parallel composition. Moreover, we support declassification of shared secrets. As a final contribution we prove the core of our result in Isabelle/HOL, providing a strong correctness guarantee of our proofs.

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!

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!

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!

Fußnoten
1
We require also well-formedness of the \(\star \)-projected protocols. This is violated, for instance, if a protocol contains a rule where only one outgoing message is labeled \(\star \) and this message contains variables. However, given that the concrete protocol is already well-formed, this is easy to fix automatically, transparent to the user.
 
Literatur
2.
Zurück zum Zitat Andova, S., Cremers, C.J.F., Gjøsteen, K., Mauw, S., Mjølsnes, S.F., Radomirović, S.: A framework for compositional verification of security protocols. Inf. Comput. 206(2–4), 425–459 (2008)MathSciNetCrossRef Andova, S., Cremers, C.J.F., Gjøsteen, K., Mauw, S., Mjølsnes, S.F., Radomirović, S.: A framework for compositional verification of security protocols. Inf. Comput. 206(2–4), 425–459 (2008)MathSciNetCrossRef
4.
Zurück zum Zitat Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685–1720 (2007)MathSciNetCrossRef Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685–1720 (2007)MathSciNetCrossRef
5.
Zurück zum Zitat Butin, D.F.: Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. Ph.D. thesis, Dublin City University, November 2012 Butin, D.F.: Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. Ph.D. thesis, Dublin City University, November 2012
8.
Zurück zum Zitat Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322–336. IEEE (2010) Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322–336. IEEE (2010)
13.
Zurück zum Zitat Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: CSFW, pp. 24–34. IEEE (2000) Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: CSFW, pp. 24–34. IEEE (2000)
16.
Zurück zum Zitat Hess, A.V., Mödersheim, S.: Formalizing and proving a typing result for security protocols in Isabelle/HOL. In: CSF (2017) Hess, A.V., Mödersheim, S.: Formalizing and proving a typing result for security protocols in Isabelle/HOL. In: CSF (2017)
17.
Zurück zum Zitat Hess, A.V., Mödersheim, S.: A typing result for stateful protocols. In: CSF (2018) Hess, A.V., Mödersheim, S.: A typing result for stateful protocols. In: CSF (2018)
Metadaten
Titel
Stateful Protocol Composition
verfasst von
Andreas V. Hess
Sebastian A. Mödersheim
Achim D. Brucker
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-319-99073-6_21