Paper 2013/237

Type-Based Analysis of Generic Key Management APIs (Long Version)

Pedro Adão, Riccardo Focardi, and Flaminia L. Luccio

Abstract

In the past few years, cryptographic key management APIs have been shown to be subject to tricky attacks based on the improper use of cryptographic keys. In fact, real APIs provide mechanisms to declare the intended use of keys but they are not strong enough to provide key security. In this paper, we propose a simple imperative programming language for specifying strongly-typed APIs for the management of symmetric, asymmetric and signing keys. The language requires that type information is stored together with the key but it is independent of the actual low-level implementation. We develop a type-based analysis to prove the preservation of integrity and confidentiality of sensitive keys and we show that our abstraction is expressive enough to code realistic key management APIs.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Full Version of CSF2013
Keywords
Key-Management APIsSecure HardwareType-based AnalysisPKCS#11
Contact author(s)
pedro adao @ ist utl pt
History
2013-05-01: revised
2013-04-29: received
See all versions
Short URL
https://ia.cr/2013/237
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2013/237,
      author = {Pedro Adão and Riccardo Focardi and Flaminia L.  Luccio},
      title = {Type-Based Analysis of Generic Key Management APIs (Long Version)},
      howpublished = {Cryptology ePrint Archive, Paper 2013/237},
      year = {2013},
      note = {\url{https://eprint.iacr.org/2013/237}},
      url = {https://eprint.iacr.org/2013/237}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.