Conference paper · Book chapter
Stateful Protocol Composition
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2018 |
| Pages: | 427-446 |
| Proceedings: | 23rd European Symposium on Research in Computer Security |
| Series: | Lecture Notes in Computer Science |
| ISBN: | 3319990721 , 331999073X , 331999073x , 9783319990729 and 9783319990736 |
| ISSN: | 16113349 and 03029743 |
| Types: | Conference paper and Book chapter |
| DOI: | 10.1007/978-3-319-99073-6_21 |
| ORCIDs: | Hess, Andreas Viktor , Mödersheim, Sebastian A. and 0000-0002-6355-1200 |
Data security Formal logic Isabelle/HOL Protocols compositionality conditions compositionality paradigm parallel compositionality result proof correctness guarantee protocols security of data sequential composition shared databases shared secrets stateful parallel composition stateful protocol composition theorem proving
