Probably the spthy code isn't the best as a reference for building an implementation. For that I'd recommend: https://www.wireguard.io/papers/wireguard.pdf htt

Probably the spthy code isn't the best as a reference for building an implementation. For that I'd recommend: https://www.wireguard.io/papers/wireguard.pdf https://www.wireguard.io/papers/wireguard.pdf https://www.wireguard.io/protocol/ https://www.wireguard.io/protocol/ http://noiseprotocol.org/noise.pdf http://noiseprotocol.org/noise.pdf However, if you actually read the Tamarin manual -- the documentation is really terrific -- I think you'll find that the spthy code quickly comes into focus as something very straight-forward. https://tamarin-prover.github.io/manual/book/001_introduction.html https://tamarin-prover.github.io/manual/book/001_introductio... So much so, in fact, that I'd really recommend fluency with something like Tamarin as an essential thing for anybody working on crypto things, even if they're not in academia. It should be accessible to folks who describe themselves as "crypto engineers." Next time you find yourself having to work on or analyze a custom crypto protocol, give it a shot.