I’ve read the manual, this is fantastic. At last a formalism I can use, provided the engine underneath doesn’t explode (combinatorially). Nothing like ProVerif, or even Tamarin. Keep up the good work, we need it.
I have a question regarding the Monokex analysis I’m about to try: Monokex doesn’t use AEAD. Instead, it mixes the transcript (and the DH shared secrets) into a hash, then use a HKDF-like function to generate a tag (and a new hash, independent from the tag). Verification is done by checking that the received tag is the same as the generated tag.
In the interest of fostering discussion in the appropriate venue, I’d rather you post what you just wrote on the Verifpal Mailing List. I’ll respond there.
Neat, yet another crypto verification tool I can try for Monokex. Hope this one will work out. The other I’ve tried were too unwieldy.
Thanks, Loup. Monokex is awesome work and I hope I’ll be able to assist with your usage of Verifpal.
I’ll hold you to that, thanks. I’ll have a stab at it the next few days.
Don’t forget to check out the User Manual, which contains helpful information on getting started.
helpful information and a cool manga, starting on page 13 ;)
BTW: VerifPal is produced by the original author of Noise Explorer featured earlier here on Lobste.rs .
There is a complete example from Noise protocol: https://github.com/SymbolicSoft/verifpal/blob/master/examples/signal.vp
This is not the Noise protocol framework, but the Signal secure messaging protocol: https://signal.org/docs
Noise was authored by Trevor Perrin, one of the two co-authors for the Signal protocol.
Please review Chapter 5 of the Verifpal User Manual in order to better understand how this modeling was achieved in Verifpal.
You are perfectly right. Thanks for pointing it out. Reading the manual right now!