Stateful Protocol Composition

Andreas Viktor Hess*, Sebastian A. Mödersheim, Achim D. Brucker

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

35 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationESORICS 2018: Computer Security
EditorsJavier Lopez , Jianying Zhou , Miguel Soriano
PublisherSpringer
Publication date2018
Pages427-446
ISBN (Print)978-3-319-99072-9
ISBN (Electronic)978-3-319-99073-6
DOIs
Publication statusPublished - 2018
Event23rd European Symposium on Research in Computer Security - Barcelona, Spain
Duration: 3 Sep 20187 Sep 2018

Conference

Conference23rd European Symposium on Research in Computer Security
Country/TerritorySpain
CityBarcelona
Period03/09/201807/09/2018
SeriesLecture Notes in Computer Science
Volume11098
ISSN0302-9743

Keywords

  • Data security
  • Protocols
  • Formal logic
  • protocols
  • security of data
  • theorem proving
  • compositionality conditions
  • compositionality paradigm
  • sequential composition
  • proof correctness guarantee
  • shared databases
  • Isabelle/HOL
  • parallel compositionality result
  • stateful protocol composition
  • shared secrets
  • stateful parallel composition

Fingerprint

Dive into the research topics of 'Stateful Protocol Composition'. Together they form a unique fingerprint.

Cite this