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.Category / Keywords: foundations / formal methods for security, automated verification, trusted computing, platform integrity Date: received 24 Oct 2013 Contact author: s bursuc at bristol ac uk Available format(s): PDF | BibTeX Citation Version: 20131024:161009 (All versions of this report) Short URL: ia.cr/2013/686 Discussion forum: Show discussion | Start new discussion