Subject: [Acme] WIP Tamarin Models for ACME

From: Eric Rescorla <[email-masked]>
Date: Wed, 30 Sep 2015 15:07:06 -0700

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