# Automated verification of dynamic root of trust protocols (long version)

## TL;DR

This paper presents a formal modeling and automated verification approach for security protocols based on dynamic root of trust, addressing challenges in representing TPM states and extensions using ProVerif.

## Contribution

It introduces new formal models and a transformation technique to enable ProVerif to verify complex dynamic root of trust protocols.

## Key findings

- Successfully modeled TPM and trusted computing platform behaviors
- Enabled automated security verification of dynamic root of trust protocols
- Provided formal guarantees for protocol security properties

## Abstract

Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing platforms (including CPU, TPM, OS, and other essential components) and of associated protocols in a classical process calculus accepted by ProVerif. As part of the formalization effort, we introduce new equational theories for representing TPM specific platform states and dynamically loaded programs. Formal models for such an extensive set of features cannot be readily handled by ProVerif, due especially to the search space generated by unbounded extensions of TPM registers. In this context we introduce a transformation of the TPM process, that simplifies the structure of the search space for automated verification, while preserving the security properties of interest. This allows to run ProVerif on our proposed models, so we can derive automatically security guarantees for protocols running in a dynamic root of trust context.