Security critical applications often store keys on dedicated HSM or key-management servers to separate highly sensitive cryptographic operations from more vulnerable parts of the network. Access to such devices is given to protocol parties by the means of Security APIs, e.g., the RSA PKCS#11 standard, IBM's CCA and the TPM API, all of which protect keys by providing an API that allows to address keys only indirectly. This thesis has two parts. The first part deals with formal methods that allow for the identification of secure configurations in which Security APIs improve the security of existing protocols, e.g., in scenarios where parties can be corrupted. A promising paradigm is to regard the Security API as a participant in a protocol and then use traditional protocol analysis techniques. But, in contrast to network protocols, Security APIs often rely on the state of an internal database. When it comes to an analysis of an unbounded number of keys, this is the reason why current tools for protocol analysis do not work well. We make a case for the use of MSR as the back-end for verification and propose a new process calculus, which is a variant of the applied pi calculus with constructs for manipulation of a global state. We show that this language can be translated to MSR rules while preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a back-end. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and a contract signing protocol. The second part of this thesis aims at identifying security properties that a) can be established independent of the protocol, b) allow to catch flaws on the cryptographic level, and c) facilitate the analysis of protocols using the Security API. We adapt the more general approach to API security of Kremer et.al. to a framework that allows for composition in form of a universally composable key-management functionality. The novelty, compared to other definitions, is that this functionality is parametric in the operations the Security API allows, which is only possible due to universal composability. A Security API is secure if it implements correctly both key-management (according to our functionality) and all operations that depend on keys (with respect to the functionalities defining those operations). We present an implementation which is defined with respect to arbitrary functionalities (for the operations that are not concerned with key-management), and hence represents a general design pattern for Security APIs.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00942459 |
| Date | 07 January 2014 |
| Creators | Künnemann, Robert |
| Publisher | École normale supérieure de Cachan - ENS Cachan |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | English |
| Type | PhD thesis |
Page generated in 0.0022 seconds