A Formal Theory of Key Conjuring

Véronique Cortier 1 Stéphanie Delaune 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, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We describe a formalism for key conjuring, the process by which an attacker obtains an unknown, encrypted key by repeatedly calling a cryptographic API function with random values in place of keys. This technique has been used to attack the security APIs of several Hardware Security Modules (HSMs), which are widely deployed in the ATM (cash machine) network. We propose a formalism for detecting computationally feasible key conjuring operations, incorporated into a Dolev-Yao style model of the security API. We show that security in the presence of key conjuring operations is decidable for a particular class of APIs, which includes the key management API of IBM's Common Cryptographic Architecture (CCA).
Type de document :
Rapport
[Research Report] RR-6134, INRIA. 2007, pp.38
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00129642
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 26 février 2007 - 16:51:34
Dernière modification le : jeudi 15 février 2018 - 08:48:09
Document(s) archivé(s) le : mardi 21 septembre 2010 - 12:53:51

Fichiers

RR-6134.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00129642, version 2

Citation

Véronique Cortier, Stéphanie Delaune, Graham Steel. A Formal Theory of Key Conjuring. [Research Report] RR-6134, INRIA. 2007, pp.38. 〈inria-00129642v2〉

Partager

Métriques

Consultations de la notice

237

Téléchargements de fichiers

244