Formal modeling and automated verification of a remote attestation protocol
Maybe this is a good starting point:
&quot;Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme&quot;, which appeared at ASIACCS 2020:
https://people.inf.ethz.ch/rsasse/pub/eccdaaimp-asiaccs20.pdf
It uses the Tamarin prover, and the Tamarin model files are available for download.