Basic Diffie-Hellman modeling

[Alessandro Zanatta]

Good evening,

I'm Alessandro Zanatta and I'm a bachelor student. I'm writing my thesis, which involves the use of Tamarin.

I'm currently trying to get hands-on-experience. I've been trying to model the Diffie-Hellman protocol (without authentication).

I don't know if I've modeled it in a good way, but it seems to at least work for the injective correspondence and the reachability lemmas. I'm completely stuck on the secrecy lemma for the secret message the two peers exchange with the new key they setup. I've tried for a few hours to no avail.

Could you please show me my errors/bad practices? It would be a huge help to me.

You can find my best try following the link below (attachments were rejected).

https://github.com/AlessandroZanatta/Proverif-Tamarin-Translations/blob/master/diffie_hellman/protocol.spthy

Thanks in advance,

Alessandro Zanatta