Formal modeling and automated verification of a remote attestation protocol I'm involved in the design of a communication protocol that requires mutual
remote attestation of both communicating parties prior to exchanging any other
data. We found several tools for symbolic security analysis of cryptographic
protocols such as ProVerif, Tamarin or Verifpal.
However, we barely have any experience with formally analyzing crypto protocols.
The manuals of the previously mentioned tools already provide some
examples. Are there any other good sources that concretly explain how to
formalize a secure communication protocol in a machine checkable way? Are there
any other tools that are better suited for this task considering the focus on
remote attestation?
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.