A Generic Security API for Symmetric Key Management on Cryptographic Devices

A Generic Security API for Symmetric Key Management on Cryptographic Devices. Véronique Cortier and Graham Steel. Information and Computation, 238:208–232, Elsevier Science Publishers, 2014.

Download

[PDF] [HTML]

Abstract

We present the design of a new symmetric key management API for cryptographic devices intended to implement security protocols in distributed systems. Our API has a formal security policy expressed in terms of invariants under various threat scenarios, and proofs of security in the symbolic model. This sets it apart from previous APIs such as RSA PKCS#11, which are under-specified, lack a clear secuity policy and are often subject to attacks.
Our design is based on the principle of explicitness: the security policy for a key must be given at creation time, and this policy is then included in any ciphertext containing the key. The policy is expressed in terms of a position in a hierarchy of keys and a set of agents. Our API also contains novel features such as the possibility of insisting on a freshness check before accepting an encrypted key for import. To show the applicability of our design, we give an algorithm for automatically instantiating the API commands for a given key management protocol. We demonstrate the algorithm on a set of symmetric key establishment protocols from the Clark-Jacob suite. We show that in the restricted mode of operation where freshness checks are required, some protocols from the test suite cannot be implemented: precisely those now known to be susceptible to replay attacks.
This paper is an extended version of a paper published at the ESORICS conference in September 2009. It contains proofs of more fine-grained security properties than the original paper (for the same API), in particular in the case where some but not all long-term keys on a particular token are lost to the attacker. Since the original paper was submitted, another key management API with a security proof has appeared in the literature due to Cachin and Chandran. This present paper contains a comparison of the two designs and their security properties, as well as a more detailed comparison to other API designs.

BibTeX

@article{CS-api-IaC14,
  author =        {Cortier, V{\'e}ronique and
                   Steel, Graham},
  journal =       {Information and Computation},
  OPTmonth =       {},
  OPTnumber =        {0},
  pages =         {208-232},
  publisher =     {Elsevier Science Publishers},
  title =         {A Generic Security {API} for Symmetric Key
Management on Cryptographic Devices},
  volume =        {238},
  year =          {2014},
  abstract =      { We present the design of a new symmetric key management API for cryptographic
  devices intended to implement security protocols in distributed
  systems. Our API has a formal security policy expressed in terms of
  invariants under various threat scenarios, and proofs of security in
  the symbolic model. This sets
  it apart from previous APIs such as RSA PKCS#11, which are under-specified, lack a clear secuity policy and are often subject to
  attacks.
\par
  Our design is based on the principle of explicitness: the security policy for a key must be given at creation time, and this policy is then included in any ciphertext containing the key. The policy is expressed in terms of a position in a hierarchy of keys and a set of agents. Our API also contains novel features such as the possibility of
  insisting  on a freshness check before accepting an encrypted key for import.
  To show the applicability of our design, we give an algorithm for
  automatically instantiating the API commands for a given key
  management protocol. We demonstrate the algorithm on a set of
  symmetric key establishment protocols from the Clark-Jacob suite. We show that in
  the restricted mode of operation where freshness checks are
  required, some protocols from the test suite cannot be implemented:
  precisely those now known to be susceptible to replay attacks.
\par
This paper is an extended version of a paper published at the ESORICS
conference in September 2009. It contains proofs of more fine-grained
security properties than the original paper (for the same API), in
particular in the case where some but not all long-term keys on a
particular token are lost to the attacker. Since the original paper was submitted,
another key management API with a security proof has appeared in the
literature due to Cachin and Chandran. This present paper contains a comparison of
the two designs and their security properties, as well as a more
detailed comparison to other API designs.
},
  doi =           {10.1016/j.ic.2014.07.010},
}