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.
|Title of host publication||Proceedings of 2021 IEEE 34th Computer Security Foundations Symposium|
|Publication status||Published - 2021|
|Event||2021 IEEE 34th Computer Security Foundations Symposium - Virtual conference, Dubrovnik, Croatia|
Duration: 21 Jun 2021 → 25 Jun 2021
Conference number: 34
|Conference||2021 IEEE 34th Computer Security Foundations Symposium|
|Period||21/06/2021 → 25/06/2021|