Synthesising Secure APIs

Synthesising Secure APIs. Véronique Cortier and Graham Steel. Rapport de recherche RR-6882, INRIA, 2009.

Download

Abstract

Security APIs are used to define the boundary between trusted and untrusted code. The security properties of existing API are not always clear. In this paper, we give a new generic API for managing symmetric keys on a trusted cryptographic device. We state and prove security properties for the API. In particular, our API offers a high level of security even when the host machine is controlled by an attacker. Our API is generic in the sense that it can implement a wide variety of (symmetric key) protocols. As a proof of concept, we give an algorithm for automatically instantiating the API commands for a given key management protocol. We demonstrate the algorithm on a set of key establishment protocols from the Clark-Jacob suite.

BibTeX

@techreport{CORTIER:2009:INRIA-00369395:1,
    hal_id = {inria-00369395},
    title = {{Synthesising Secure APIs}},
    author = {Cortier, V{\'e}ronique and Steel, Graham},
    abstract = {{Security APIs are used to define the boundary between trusted and untrusted code. The security properties of existing API are not always clear. In this paper, we give a new generic API for managing symmetric keys on a trusted cryptographic device. We state and prove security properties for the API. In particular, our API offers a high level of security even when the host machine is controlled by an attacker. Our API is generic in the sense that it can implement a wide variety of (symmetric key) protocols. As a proof of concept, we give an algorithm for automatically instantiating the API commands for a given key management protocol. We demonstrate the algorithm on a set of key establishment protocols from the Clark-Jacob suite.}},
    keywords = {Application Programming Interface, Hardware Security Module, Formal methods},
    language = {Anglais},
    affiliation = {CASSIS - INRIA Lorraine - LORIA / LIFC , Laboratoire Sp{\'e}cification et V{\'e}rification [Cachan] - LSV},
    pages = {24},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-6882},
    year = {2009},
}