Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Synthesising Secure APIs

Véronique Cortier 1 Graham Steel 2 
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Véronique Cortier Connect in order to contact the contributor
Submitted on : Thursday, March 19, 2009 - 4:08:57 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:21 AM
Long-term archiving on: : Tuesday, June 8, 2010 - 11:39:31 PM


Files produced by the author(s)


  • HAL Id : inria-00369395, version 1


Véronique Cortier, Graham Steel. Synthesising Secure APIs. [Research Report] RR-6882, INRIA. 2009, pp.24. ⟨inria-00369395⟩



Record views


Files downloads