Formal analysis of protocols based on TPM state registers

Stéphanie Delaune 1, 2 Steve Kremer 1, 2 Ryan Mark 3 Graham Steel 1, 2
1 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We present a Horn-clause-based framework for analysing security protocols that use platform configuration registers (PCRs), which are registers for maintaining state inside the Trusted Platform Module (TPM). In our model, the PCR state space is unbounded, and our experience shows that a naïve analysis using ProVerif or SPASS does not terminate. To address this, we extract a set of instances of the Horn clauses of our model, for which ProVerif does terminate on our examples. We prove the soundness of this extraction process: no attacks are lost, that is, any query derivable in the more general set of clauses is also derivable from the extracted instances. The effectiveness of our framework is demonstrated in two case studies: a simplified version of Microsoft Bitlocker, and a digital envelope protocol that allows a user to choose whether to perform a decryption, or to verifiably renounce the ability to perform the decryption.
Type de document :
Communication dans un congrès
24th IEEE Computer Security Foundations Symposium (CSF'11), Jun 2011, Cernay-la-Ville, France. IEEE Computer Society, 2011, Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11). 〈10.1109/CSF.2011.12〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00636747
Contributeur : Steve Kremer <>
Soumis le : vendredi 9 octobre 2015 - 10:52:14
Dernière modification le : jeudi 11 janvier 2018 - 06:20:14
Document(s) archivé(s) le : dimanche 10 janvier 2016 - 10:13:54

Fichier

DKRS-csf11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Stéphanie Delaune, Steve Kremer, Ryan Mark, Graham Steel. Formal analysis of protocols based on TPM state registers. 24th IEEE Computer Security Foundations Symposium (CSF'11), Jun 2011, Cernay-la-Ville, France. IEEE Computer Society, 2011, Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11). 〈10.1109/CSF.2011.12〉. 〈inria-00636747〉

Partager

Métriques

Consultations de la notice

141

Téléchargements de fichiers

84