Vertical Composition and Sound Payload Abstraction for Stateful Protocols

Sebastien Gondron, Sebastian Modersheim

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

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.
Original languageEnglish
Title of host publicationProceedings of 2021 IEEE 34th Computer Security Foundations Symposium
PublisherIEEE
Publication date2021
Pages329-344
ISBN (Print)978-1-7281-7608-6
DOIs
Publication statusPublished - 2021
Event2021 IEEE 34th Computer Security Foundations Symposium - Virtual conference, Dubrovnik, Croatia
Duration: 21 Jun 202125 Jun 2021
Conference number: 34
http://www.ieee-security.org/TC/CSF2021/
https://ieeexplore.ieee.org/xpl/conhome/9504607/proceeding

Conference

Conference2021 IEEE 34th Computer Security Foundations Symposium
Number34
LocationVirtual conference
Country/TerritoryCroatia
CityDubrovnik
Period21/06/202125/06/2021
Internet address

Fingerprint

Dive into the research topics of 'Vertical Composition and Sound Payload Abstraction for Stateful Protocols'. Together they form a unique fingerprint.

Cite this