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?