Secure composition of PKIs with public key protocols

Vincent Cheval , Veronique Cortier, Bogdan Warinschi

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

7 Citations (Scopus)
174 Downloads (Pure)


We use symbolic formal models to study the composition of public key-based protocols with public key infrastructures (PKIs). We put forth a minimal set of requirements which a PKI should satisfy and then identify several reasons why composition may fail. Our main results are positive and offer various trade-offs which align the guarantees provided by the PKI with those required by the analysis of protocol with which they are composed. We consider both the case of ideally distributed keys but also the case of more realistic PKIs.,,Our theorems are broadly applicable. Protocols are not limited to specific primitives and compositionality asks only for minimal requirements on shared ones. Secure composition holds with respect to arbitrary trace properties that can be specified within a reasonably powerful logic. For instance, secrecy and various forms of authentication can be expressed in this logic. Finally, our results alleviate the common yet demanding assumption that protocols are fully tagged
Original languageEnglish
Title of host publication2017 IEEE Computer Security Foundations Symposium
Number of pages15
ISBN (Electronic)978-1-5386-3217-8
Publication statusE-pub ahead of print - 28 Sept 2017

Publication series

Name2017 IEEE 30th Computer Security Foundations Symposium (CSF)
ISSN (Electronic)2374-8303


Dive into the research topics of 'Secure composition of PKIs with public key protocols'. Together they form a unique fingerprint.

Cite this