0
$\begingroup$

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?

$\endgroup$
0
$\begingroup$

Maybe this is a good starting point:

"Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme", 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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.