1. 19
  1.  

  2. 5

    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.

    • Is there a way to check that what we receive in a message and what we compute locally are equal?
    • If not, could we cheat by using AEAD somehow?
    1. 4

      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.

      1. 2

        Okay

    2. 5

      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.

      1. 3

        Thanks, Loup. Monokex is awesome work and I hope I’ll be able to assist with your usage of Verifpal.

        1. 3

          I’ll hold you to that, thanks. I’ll have a stab at it the next few days.

          1. 2

            Don’t forget to check out the User Manual, which contains helpful information on getting started.

            1. 2

              helpful information and a cool manga, starting on page 13 ;)

      2. 3

        BTW: VerifPal is produced by the original author of Noise Explorer featured earlier here on Lobste.rs .

        1. 1

          There is a complete example from Noise protocol: https://github.com/SymbolicSoft/verifpal/blob/master/examples/signal.vp

          1. 3

            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.

            1. 2

              You are perfectly right. Thanks for pointing it out. Reading the manual right now!