Secure composition of PKIs with public key protocols
Vincent Cheval, Véronique Cortier, and Bogdan Warinschi. Secure composition of PKIs with public key protocols. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, August 2017.
Download
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.
BibTeX
@InProceedings{CSF2017-PKI,
author = {Vincent Cheval and V\'eronique Cortier and Bogdan
Warinschi},
title = {Secure composition of PKIs with public key
protocols},
booktitle = {{P}roceedings of the 30th {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'17)},
year = 2017,
month = {August},
publisher = {{IEEE} Computer Society Press},
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. \par 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. },
={https://members.loria.fr/VCortier/files/Papers/CSF2017-PKI.pdf},
}