Automated Analysis of Key Management Policies

Key management is the Achilles’ heel of cryptography, as the security of any cryptographic mechanism depends on the protection of its underlying keys. Key management is notoriously challenging because, in many practical scenarios, keys must be securely encrypted for export and import between different devices and applications. If these operations are not well-regulated, they can be vulnerable to attacks that expose sensitive keys in plaintext, as demonstrated in various research studies over the last 15+ years. In this paper, we consider a recently proposed model for key management and investigate its automated verification using the Tamarin prover. Our results show that specific instances of key management policies can be successfully verified in Tamarin, but achieving this requires the careful development of so-called source lemmas. These lemmas disambiguate the origins of cryptographic terms, a condition that is often essential for ensuring the correct termination of the analysis. We hint at a general method to derive, from a given policy, a Tamarin specification along with the corresponding source lemma, enabling automated proof of various secrecy properties of cryptographic keys.