[Verifpal] Verifpal 0.5

[Loup Vaillant David]

> Did you notice also that the `_` feature was implemented? I remember
> that you asked for it.

Yes I did notice, and nil too! I just didn't need it for the trivial
examples, because I used it only once, so using "_" worked anyway. But
it will be a big help with more meaty protocols, such as Monokex, where
ASSERT is called multiple times.


> Regarding your “USE()” idea, I wanted to ask you to please test using
> HASH instead and see if Verifpal produces output that conforms with
> your requirements. If so, then HASH should be sufficient. Please try
> it out and get back to me.

Yup, it works. Good enough for me if I know of the thing.

In unchecked_aead.vp, adding that spurious hash works:

    principal Bob[
        ss_        = a_public^b
        key_       = HASH(ss_)
        plaintext_ = AEAD_DEC(key_, ciphertext, ad)
        _          = HASH(ad)
    ]

Verifpal warns me that `ad` is successfully used in HASH(), despite
having been sent by the attacker. But then I wonder: how exactly do we
must use a value for it to count as "used" in an authentication result?
My intuition is that checked primitives and MAC would not trigger the
result, while all the others would. Or something like that. Correct?


> Unrelated: I really want to rename HMACVERIF to ASSERT, but am
> annoyed by how this will break backwards compatibility.

ASSERT works, but then I would expect a single boolean argument.
ASSERT_EQUAL is closer to what you encounter in typical test suites.
That is:

    ASSERT(mac, real_mac)       // maybe a bit confusing
    ASSERT(mac = real_mac)      // pretty, but complicates parsing
    ASSERT_EQUAL(mac, real_mac) // not confusing, but more verbose
     
On the other hand, "ASSERT" is shorter. Not sure which I would have
chosen

Loup.



> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
> > On Sep 8, 2019, at 9:55 PM, Loup Vaillant David <
> > loup at loup-vaillant.fr> wrote:
> > 
> > Excellent, thanks!
> > 
> > Just tested on my test files, and except for a false positive, it
> > works
> > as expected:
> > 
> > - ok.vp             : green light as expected.
> > - unchecked_aead.vp : green light… as expected.
> > - no_decryption.vp  : error is reported, this is perfect.
> > - unguarded_alice.vp: authentication is broken, as expected.
> > - unguarded_bob.vp  : confidentiality is broken, as expected.
> > - hmac_ok.vp        : false positive: "confidentiality broken"
> > 
> > Now the next step, I think, would be to get rid of that false
> > positive.
> > I'm OK with false positives, *if* they're rare enough. But this is
> > a
> > fairly trivial model. I suspect we're hitting a fairly broad class
> > of
> > false positives here, not just narrow corner case. I believe this
> > should be addressed before version 1.0.
> > 
> > ---
> > 
> > Regarding my uneasiness about giving a green light in
> > unchecked_aead, I
> > may have a solution. Failing to check a checked primitive means we
> > don't block execution. But the primitive still fails to produce a
> > meaningful value, protecting us against most attacker interference.
> > The
> > big problems arise when we actually use unauthenticated data for
> > something significant, such as a decryption.
> > 
> > The thing is, the additional data will often not be used at all in
> > the
> > model. If for instance, it is something like an identifier the
> > recipient can then check against a list of valid senders, Verifpal
> > has
> > no way of representing it —it's out of scope.
> > 
> > How about having a generic way to use a value, without telling
> > Verifpal
> > what that use is exactly?  Something like `USE(data)`. We could
> > modify
> > the last Bob in `ok.vp` thus:
> > 
> >    principal Bob[
> >        ss_        = a_public^b
> >        key_       = HASH(ss_)
> >        plaintext_ = AEAD_DEC(key_, ciphertext, ad)?
> >        _          = USE(ad)
> >    ]
> > 
> > That way we clearly signal to Verifpal that we are relying on `ad`
> > for
> > some security sensitive matter, and that it'd better be
> > authenticated,
> > or be derived from authenticated values. In this case, removing the
> > question mark should cause Verifpal to warn us about
> > unauthenticated
> > `ad` (as successfully used in the USE primitive).
> > 
> > (We could replace "USE" by "RELY_ON" or something.)
> > 
> > While we're at it, something similar could be done with plaintext_:
> > 
> >    principal Bob[
> >        ss_        = a_public^b
> >        key_       =
> > HASH(ss_)
> >        plaintext_ = AEAD_DEC(key_, ciphertext, ad)?
> >        _ 
> > = USE(ad)
> >        _          = USE(plaintext_)
> >    ]
> > 
> > The idea behind AEAD_DEC is that it should not produce a meaningful
> > value if its internal checks fails. So, removing the question mark,
> > and
> > allow attacker interference should not cause `plaintext_` to be
> > under
> > attacker control. But real implementations often *do* produce some
> > kind
> > of `plaintext_`: an empty buffer, a buffer full of zeroes, or
> > uninitialised memory (that last one is potentially nasty). If that
> > broken plaintext is not used in the model itself, it might be a
> > good
> > idea to let the user mark it as used by the application itself.
> > 
> > Here, the additional error I would expect if we remove the question
> > mark is that `plaintext_` is successfully used in
> > `USE(plaintext_)`,
> > but is garbage when `ciphertext` or `ad` is sent by the attacker.
> > 
> > Just a suggestion, though. There may be better alternatives.
> > 
> > Loup.
> > 
> > 
> > 
> > 
> > On Sun, 2019-09-08 at 19:16 +0200, Nadim Kobeissi via Verifpal
> > wrote:
> > > Hello everyone,
> > > Verifpal 0.5 is now available.
> > > 
> > > RELEASE NOTES
> > >    - Increased analysis speeds by only mutating relevant values.
> > >    - Fixed even more parsing errors pointed out by Mike.
> > > Take note of the release notes for the previous version as well,
> > > which were quite substantial:
> > >    - NEW: nil keyword. Self-explanatory (by popular request).
> > >    - NEW: _ can be used to assign anonymous constants (by popular
> > > request).
> > >    - Fix yet more parsing errors pointed out by Mike.
> > >    - More fixes and improvements to authentication queries.
> > >    - Added a new hopefully instructional example model:
> > > ephemerals_and_signature.vp
> > > 
> > > INSTALLING AND UPDATING
> > >    - If you’re fine with running arbitrary scripts in your
> > > terminal,
> > > you can instantly update like this:
> > >        - bash -c 'curl -sL https://verifpal.com/install|bash'
> > >    - Or you can download a pre-compiled binary here:
> > >        - 
> > > https://source.symbolic.software/verifpal/verifpal/releases
> > > 
> > > NOTES ABOUT THIS VERSION
> > >    - As usual, please continue your testing, everyone!
> > > 
> > > Looking forward to hearing from you all!
> > > 
> > > Nadim Kobeissi
> > > Symbolic Software • https://symbolic.software
> > > Sent from office
> > > _______________________________________________
> > > Verifpal mailing list
> > > Verifpal at lists.symbolic.software
> > > https://lists.symbolic.software/mailman/listinfo/verifpal
> > 
> > <hmac_ok.vp>
> 
> 
-------------- next part --------------
attacker[active]

// initialisation
principal Alice[
    knows private a
    a_public = G^a
]
principal Bob[
    knows private b
    b_public = G^b
]
Alice -> Bob   : [a_public]
Bob   -> Alice : [b_public]


// Key exchange
principal Alice[
    generates plaintext
    generates ad
    ss         = b_public^a
    key        = HASH(ss)
    ciphertext = AEAD_ENC(key, plaintext, ad)
]
Alice -> Bob : ad, ciphertext

principal Bob[
    ss_        = a_public^b
    key_       = HASH(ss_)
    plaintext_ = AEAD_DEC(key_, ciphertext, ad)
    _          = HASH(ad)
]

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
    authentication? Alice -> Bob : ad
]