Cryptographically Verified Design and Implementation of a Distributed Key Manager

Tolga Acar, Cedric Fournet, and Dan Shumow


We present DKM, a distributed key management system with a cryptographically verified code base. DKM implements a new data protection API. It manages keys and policies on behalf of groups of users that share data. To ensure long-term protection, DKM supports cryptographic agility: algorithms, keys, and policies can evolve for protecting fresh data while preserving access to old data. DKM is written in C# and currently used by several large data center applications. To verify our design and implementation, we also write a lightweight reference implementation of DKM in F#. This code closes the gap between formal cryptographic models and production code:

Formally, the F# code is a very precise model of DKM: we automatically verify its security against active adversaries, using a refinement type-checker coupled with an SMT solver and new symbolic libraries for cryptographic agility.

Concretely, the F# code closely mirrors our production code, and we automatically test that the corresponding C# and F# fragments can be swapped without affecting the runtime behavior of DKM.

To the best of our knowledge, this is the largest cryptographically-verified implementation to date. We also describe several problems we uncovered and fixed as part of this joint design, implementation, and verification process.


Publication typeTechReport
PublisherMicrosoft Technical Report

Previous versions

Tolga Acar, Mira Belenkiy, Mihir Bellare, and David Cash. Cryptographic Agility and its Relation to Circular Encryption, Springer Verlag, May 2010.

> Publications > Cryptographically Verified Design and Implementation of a Distributed Key Manager