IACR News item: 24 October 2013
Shiwei Xu, Sergiu Bursuc, Julian P. Murphy
ePrint ReportWe 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.
Additional news items may be found on the IACR news page.