Amir Herzberg (University of Connecticut)- Provable Security for PKI Schemes - and the (Composable) Modular Security Specifications Framework

PKI schemes provide a critical foundation for applied cryptographic protocols. However, there are no rigorous security specifications for realistic PKI schemes, and therefore, no PKI schemes were proven secure. Cryptographic systems that use PKI are analyzed by adopting overly simplified models of the PKI, often, simply assuming secure public keys. This is problematic considering the extensive reliance on PKI, the multiple failures of PKI systems, and the fact that proposed and deployed PKI are complex, have complex requirements and assume complex models.

We present game-based security specifications for PKI schemes, and analyse important, widely deployed PKIs: PKIX and two variants of Certificate Transparency (CT). All PKIs are based on the X.509v3 standard and its CRL revocation mechanism. Our analysis identified few subtle vulnerabilities, and includes reduction-based proofs showing that the PKIs ensure specific requirements under specific models (assumptions).To our knowledge, this is the first reduction-based definition and proof of security for a realistic PKI scheme.

Our specifications and analysis use the Modular Security Specifications (MoSS) framework [Crypto’21]. The talk will explain the relevant aspects of MoSS. We may briefly discuss the extensions that allow provably-secure compositions of protocols.