Provable security for cryptographic protocols - exact analysis and engineering applications

Abstract

We develop an approach to deriving concrete engineering advice for cryptographic protocols from provable-security-style proofs of security. The approach is illustrated with a simple, yet useful protocol. Our main result provides the first published proof of an exact probabilistic relationship between a high-level protocol and multiple cryptographic primitives. This exact relationship enables us to rigorously derive concrete recommendations on the bitlengths of cryptographic keys and on how often principals should rekey. As an additional benefit of our approach, the process of developing our theorem and proof lead us to identify and implement an improvement in our example protocol.