Abstract
We propose PCS_AC – a new cryptographic framework for post-compromise security (PCS) in secure-communication protocols, which caters not only for the traditional PCS-corruption of key material, but also for adversarial controls of a PCS-nature at the application level. That is, we study and formalise when and how an adversary can maintain or lose post-compromise advantages due to application-driven controls as well, rather than do so based on cryptographic manipulations and settings alone. In fact, the motivation and ideas in our PCS_AC are in line with a recent document by NIST [14], where adversarial application-level influence on key compromise are discussed, and it is the first of this kind to be produced.
Since measures of PCS “healing” are discrete, we also mechanised an approximation of our cryptographic PCS_AC framework, in symbolic/Dolev-Yao models, as well; we do this in the two state-of-the-art protocol verifiers, ProVerif and Tamarin, and – in the process – we also compare and discuss different tool-assistance aspects in each. We include a summary of this in this version of the paper, too.
We apply PCS_AC to the 5G procedure called AKMA (Authentication and Key Management for Application), showing new PCS-attacks therein and proposing patches, including a backwards-compatible one. We implement and test AKMA as well as of one of our PCS-driven patches, on top of Fraunhofer’s Open5GCore.
We also cast ‘TLS1.3 with session resumption and key updates’ in PCS_AC in various ways, looking at different keys being potentially targeted by one type of attacker or another, amongst the multiple possible choices formalised in PCS_AC. This captures new and varied PCS dimensions of TLS, underlining the versatility and usefulness of our framework.