draft Tamarin security model
cfm opened this issue · 6 comments
@TheZ3ro has drafted a Verifpal model of #16 in https://gist.github.com/TheZ3ro/81270c2c62922c9ba25500d8a2f2d0b3.
This weekend, at IETF 118, @lsd-cat and I will attend an introductory training in Tamarin. Afterwards I (at least) intend to see how much of https://gist.github.com/TheZ3ro/81270c2c62922c9ba25500d8a2f2d0b3 I can replicate in Tamarin. (I might also give Isabelle a shot, after a brief presentation that was given at IETF 117.)
After attending the workshop together, we have come to the conclusion that it should be doable with Tamarin. We have started drafting a basic model to experiment with, but it will be worth to invest time into this.
Recapping for the record: We were right to move on from Verifpal. Tamarin and ProVerif can handle the full, unsimplified protocol. After IETF 118, we started in on Tamarin, because that's what we have some training and now some contacts in. It seems that we can rule out Isabelle for now:
Isabelle is a general tool:
transport protocols can be modelled as wellTamarin has more automation for security protocols
they reported an order of magnitude of speedup vs Isabelle
I've moved the working gist @lsd-cat and I used to the tamarin branch here, with meaningful commit messages. The last WIP commit includes a readme of what's left to do. While the bottleneck that we ran into turns out to have involved a loop in the specification itself, @felixlinker advised us that the three-party Diffie-Hellman key-agreement may be complex enough to require source lemmas to avoid partial deconstructions.
In this week's time-box I was able to re-model that protocol sequentially. (I have one commit locally that I've not yet pushed to the tamarin branch here. I'm on a plane at the moment without the right key handy.) To avoid getting bogged down in both brain time and CPU time, so far I've written lemmas only for pairwise executability, i.e. that ping → pong.
I'm off for the next week, and when I'm back this will have to be a lower priority while we close things out towards the holiday break. But these are the next steps I'll chip away at:
That might be my unfamiliarity with Tamarin or maybe you are trying to prove a weaker property, but generally I think you want the correspondence property in the reverse direction pong -> ping (pong implies that ping was sent, and only that) if the correspondence holds it proves authentication of the sender to the receiver.
Thanks, @beurdouche! I was too casual with my notation in #26 (comment), thinking of ping [causes / is followed by] pong. pong implies ping is indeed the more-meaningful property here.
I should mention that my work on this model is on hold pending #33, about which we should know more soon.