Formal model of PUF-based protocols.
This repository contains the Tamarin prover models that we used to specify and check PUF-based protocols described in the paper Automated Analysis of PUF-based Protocols, by R. Focardi and F. L. Luccio, that has been presented at IEEE CSF 2020 in June 2020.
To check the model you need to install the Tamarin prover
Models can be checked with Tamarin as follows:
$ tamarin-prover --prove model.spthy