| Title | Vertical Composition and Sound Payload Abstraction for Stateful Protocols |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Gondron, Sébastien, Mödersheim, Sebastian |
| Conference Name | 2021 IEEE 34th Computer Security Foundations Symposium (CSF) |
| Date Published | jun |
| Keywords | Collaboration, composability, compositionality, computer security, cryptography, formal methods and verification, Payloads, policy-based collaboration, privacy, protocol verification, Protocols, pubcrawl, security protocols, Standards, stateful protocols, Syntactics, Tools, vertical composition |
| Abstract | This paper deals with a problem that arises in vertical composition of protocols, i.e., when a channel protocol is used to encrypt and transport arbitrary data from an application protocol that uses the channel. Our work proves that we can verify that the channel protocol ensures its security goals independent of a particular application. More in detail, we build a general paradigm to express vertical composition of an application protocol and a channel protocol, and we give a transformation of the channel protocol where the application payload messages are replaced by abstract constants in a particular way that is feasible for standard automated verification tools. We prove that this transformation is sound for a large class of channel and application protocols. The requirements that channel and application have to satisfy for the vertical composition are all of an easy-to-check syntactic nature. |
| DOI | 10.1109/CSF51468.2021.00038 |
| Citation Key | gondron_vertical_2021 |
Vertical Composition and Sound Payload Abstraction for Stateful Protocols