Hi folks, I spent some time over the past few weeks using the Tamarin theorem prover [0] to put together some protocol models for ACME. These are very preliminary (since I've never really done a Tamarin model before) but they do illustrate some relevant security features. In particular, the acmev1 model allows you to reproduce the duplicate signature vulnerability and the acmev2 model (representing Richard's PR) doesn't show that, though of course that could be pilot error on my part.
If you're interested, you can find the models at: https://github.com/ekr/tamarin-dv -Ekr [0] https://github.com/tamarin-prover/tamarin-prover
_______________________________________________ Acme mailing list Acme@ietf.org https://www.ietf.org/mailman/listinfo/acme
