Secure Key Management Policies in Strand Spaces

Key management is the Achilles heel of cryptography. In recent years, several attacks have been identified due to poor key management or too liberal APIs, which do not provide a policy that precisely determines the intended use of cryptographic keys. In this paper, we have taken advantage of the expressiveness and simplicity of strand spaces, first introduced in 1998 by Joshua Guttman et al., to specify a significant subset of key management APIs. We used the automatic CPSA tool to rediscover, in an extremely clear and effective way, some known attacks. We have therefore defined a generic key management policy model and proved a key secrecy theorem for a typed version of the API. The proof highlighted the necessary requirements of the policy that we formalized through a closure property that, in fact, computes which types a key can take at runtime.