DKM: Design and Verification of a Crypto-Agile Distributed Key Manager

Tolga Acar, Cédric Fournet, and Dan Shumow.

We present the design and verification of a distributed key management system. This component implements a new data protection API for groups of users. It manages groups and their underlying cryptographic keys and policies. It is currently used by several large data-center applications. To ensure long-term data protection, it supports cryptographic agility, so that cryptography algorithms and policies can evolve for protecting fresh data while preserving access to old data. To verify the security of our design and our production code (written in C#), we also write a reference implementation in F#. Formally, we verify our F# code against a symbolic model of cryptography using F7, a refinement typechecker coupled with a model checker. Experimentally, we test that the corresponding C# and F# code fragments are interchangeable. We also report on several problems we uncovered and fixed during this verification effort.

Draft Technical Report (.pdf) and Verified Reference Implementation (F# and F7 source files).

Related work on symbolic cryptographic verification:

Verified Interoperable Implementations of Security Protocol , MSR-TR-2006-46; the final version appeared in TOPLAS, v.30 n.6, p.1-59.
Refinement Types for Secure Implementations, MSR-TR-2008-118, last revised Feb 2010; the final version will appear in TOPLAS.
Modular Verification of Security Protocol Code by Typing , draft extended version of POPL'10.

Related work on cryptographic agility:

Key Management In Distributed Systems, MSR-TR-2010-78, June 2010.
Cryptographic Agility and its Relation to Circular Encryption, EUROCRYPT 2010.