[Verifpal] Verifpal 0.5

[Loup Vaillant David]

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
-------------- 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
    ss         = b_public^a
    key        = HASH(ss)
    ciphertext = ENC(key, plaintext)
    tag        = HMAC(key, ciphertext)
]
Alice -> Bob : ciphertext, tag

principal Bob[
    ss_        = a_public^b
    key_       = HASH(ss_)
    tag_       = HMAC(key_, ciphertext)
    _          = HMACVERIF(tag, tag_)?
    plaintext_ = DEC(key_, ciphertext)
]

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