pdfreaders.org

Stateful Protocol Composition (Extended Version)

by Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker

Cover for hess.ea:tr-stateful-protocol:2018.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 analyzing the component protocols in isolation is sufficient to prove security of the more complex composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants main- tain shared databases. We also 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.

Keywords: protocol composition, security protocol, compositionality
Categories: ,
Documents: (full text as PDF file)

QR Code for hess.ea:tr-stateful-protocol:2018.Please cite this article as follows:
Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker. Stateful Protocol Composition (Extended Version). DTU Compute, Technical University Denmark, Technical Report 2018-03, 2018.
Keywords: protocol composition, security protocol, compositionality
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@TechReport{ hess.ea:tr-stateful-protocol:2018,
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 analyzing the component protocols in isolation is sufficient to prove security of the more complex composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants main- tain shared databases. We also 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.},
author = {Andreas V. Hess and Sebastian A. M{\"o}dersheim and Achim D. Brucker},
institution = {DTU Compute, Technical University Denmark},
issn = {1601-2321},
keywords = {protocol composition, security protocol, compositionality},
language = {USenglish},
num_pages = {28},
number = {2018-03},
pdf = {https://www.brucker.ch/bibliography/download/2018/hess.ea-tr-stateful-protocol-2018.pdf},
title = {Stateful Protocol Composition (Extended Version)},
url = {https://www.brucker.ch/bibliography/abstract/hess.ea-tr-stateful-protocol-2018},
year = {2018},
}