Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
High Assurance Policy-Based Key Management at Low Cost

Tolga Acar and Lan Nguyen


Past decade has witnessed the availability of Trusted Platform Modules (TPM) on commodity computers. While the most common use of TPM appears to be BitLocker on Windows OS, server class motherboards have not yet enjoyed a similar TPM deployment base. Recent research and products show that the TPM can provide a level of trust on locally executing software. Nonetheless, TPMs haven’t been utilized in data center cryptographic key management for higher levels of security assurance than software-only techniques. Hardware-based key management has so far been constrained to higher cost add-on hardware. We present a large scale policy-driven cryptographic key manager built with TPM security assurances. We describe our design principles and axioms, architecture and abstractions, security policy, and implementation. We create a role-based security model and express the model with SecPal security policy assertions. We describe our implementation of three roles, actions, resources, SecPal policies and tokens that com- bine them. Finally, we present our implementation results with SecPal proof graphs.


Publication typeTechReport
PublisherMicrosoft Research Technical Report

Newer versions

Tolga Acar, Cedric Fournet, and Dan Shumow. Cryptographically Verified Design and Implementation of a Distributed Key Manager, Microsoft Technical Report, 15 April 2014.

Previous versions

Moritz Y. Becker, Cedric Fournet, and Andrew D. Gordon. SecPAL: Design and Semantics of a Decentralized Authorization Language, Journal of Computer Security (JCS), IOS Press, 2010.

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

> Publications > High Assurance Policy-Based Key Management at Low Cost