Secure Composition of PKIs with Public Key Protocols
Title | Secure Composition of PKIs with Public Key Protocols |
Publication Type | Conference Paper |
Year of Publication | 2017 |
Authors | Cheval, V., Cortier, V., Warinschi, B. |
Conference Name | 2017 IEEE 30th Computer Security Foundations Symposium (CSF) |
Date Published | aug |
Keywords | composition, compositionality, Computational modeling, cryptographic protocols, Encryption, formal method, PKI, Protocols, pubcrawl, Public key, public key cryptography, public key infrastructures, public key protocols, secure composition, symbolic formal models, symbolic model, tagging, telecommunication security, Tools |
Abstract | 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. |
URL | http://ieeexplore.ieee.org/document/8049717/ |
DOI | 10.1109/CSF.2017.28 |
Citation Key | cheval_secure_2017 |
- Public key
- tools
- telecommunication security
- tagging
- symbolic model
- symbolic formal models
- secure composition
- public key protocols
- public key infrastructures
- public key cryptography
- Composition
- pubcrawl
- Protocols
- PKI
- formal method
- encryption
- Cryptographic Protocols
- Computational modeling
- Compositionality