Paper 2013/686

New abstractions in applied pi-calculus and automated verification of protected executions

Shiwei Xu, Sergiu Bursuc, and Julian P. Murphy

Abstract

Protocols for the protected execution of programs, like those based on a hardware root of trust, will become of fundamental importance for computer security. In parallel to such protocols, there is therefore a need to develop models and tools that allow formal specification and automated verification of the desired security properties. Still, current protocols lack realistic models and automated proofs of security. This is due to several challenges that we address in this paper. We consider the classical setting of applied pi-calculus and ProVerif, that we enrich with several generic models that allow verification of protocols designed for a given computing platform. Our contributions include models for specifying platform states and for dynamically loading and executing protected programs. We also propose a new method to make ProVerif terminate on a challenging search space - the one obtained by allowing an unbounded number of extensions and resets for the platform configuration registers of the TPM. We illustrate our methods with the case study of a protocol for a dynamic root of trust (based on a TPM), which includes dynamic loading, measurement and protected execution of programs. We prove automatically with ProVerif that code integrity and secrecy of sealed data hold for the considered protocol.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Preprint. MINOR revision.
Keywords
formal methods for securityautomated verificationtrusted computingplatform integrity
Contact author(s)
s bursuc @ bristol ac uk
History
2013-10-24: received
Short URL
https://ia.cr/2013/686
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2013/686,
      author = {Shiwei Xu and Sergiu Bursuc and Julian P.  Murphy},
      title = {New abstractions in applied pi-calculus and automated verification of protected executions},
      howpublished = {Cryptology ePrint Archive, Paper 2013/686},
      year = {2013},
      note = {\url{https://eprint.iacr.org/2013/686}},
      url = {https://eprint.iacr.org/2013/686}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.