Paper 2013/686

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

Shiwei Xu, Sergiu Bursuc, and Julian P. Murphy


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.

Available format(s)
Publication info
Preprint. MINOR revision.
formal methods for securityautomated verificationtrusted computingplatform integrity
Contact author(s)
s bursuc @ bristol ac uk
2013-10-24: received
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.