Cryptographically Verified Design and Implementation of a Distributed Key Manager

Tolga Acar, Cedric Fournet, and Dan Shumow

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2014-48
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