[Verifpal] 0.4 missed attacks (on the trivial handshake)

[Nadim Kobeissi]

Dear Loup,

ok.vp
> -----
>
> Expected a green light, got an attack instead:
>
> - ad is sent by attacker instead of Alice
>
> Unless I made an error in the model itself (please check), `ad` has
> been verified by the checked primitive, and Bob does not read it before
> then.
>

Yup, I'm aware of this and will look at it in due course. Generally
speaking, false positives bother me infinitely less than missed attacks. In
comparison, I really don't care much about them and see them as
inconveniences to fix in due course (ProVerif gives false positives, and so
does Tamarin, etc.)

no_decryption.vp
> ----------------
>
> Expected a green light, got a green light. Good enough for version 0.5,
> but I do wish to add that warning about Bob not reading something we
> check the authentication of.
>

Warning will be added in the 0.4.x branch.

Now I'm not asking that you change this part of the model. Worst case,
> I can do aead manually with ENC/DEC and HMAC/HMACVERIF, and test false
> decryptions by removing the HMACVERIF line. As an optional behaviour
> perhaps? And there's still the additional data to contend with. Maybe
> merely performing AEAD_DEC on it doesn't count as "reading", but it
> still makes me feel a bit uneasy.
>

This is a much larger discussion for another time, post 0.4.x.

hmac_ok.vp
> ----------
>
> Expected a green light.
>
> Version 0.3 gives me that green light.
> Version 0.4 believes ciphertext is vulnerable to forgery.
>
> Git bisect says the error has apparently been introduced by the 89aa3d1
> commit, named "HIGHLY EXPERIMENTAL".
>

Already aware of this, we discovered it yesterday during testing. You'll
get the same misleading result with signatures as well.
Unlike some other things you've pointed out (eg. models yesterday), this in
particular isn't a bug in Verifpal, but it's rather that its security model
for this sort of test is currently overzealous. It will however be
corrected in 0.4.x as well (this will be I think difficult to correct, the
cause is understood but not simple to resolve.)

One annoying result of these fixes is a big increase in verification times:
Signal for example now takes about two hours whereas it previously took
about a minute. This is fine, however, and I knew it would happen.

I feel we are slowly getting somewhere. Keep it up! (Also, it's
> wonderful that you have someone taking care of the test suite. We kinda
> need it yesterday, though, could you give your intern a time machine?
> Or maybe a few lashes, that could work too. :-)
>

I feel like we're progressing very quickly, actually. The test suite will
be ready this month.

Will keep you posted.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Thu, Sep 5, 2019 at 12:01 AM Loup Vaillant David <loup at loup-vaillant.fr>
wrote:

> Ok, next rounds of tests, based on commit ef654a2 (3 commits after your
> 4.0.1 tag).  The files are the same as before, except when mentioned
> explicitly.
>
> This version is much better, but I think we've got ourselves a false
> positive.
>
>
> ok.vp
> -----
>
> Expected a green light, got an attack instead:
>
> - ad is sent by attacker instead of Alice
>
> Unless I made an error in the model itself (please check), `ad` has
> been verified by the checked primitive, and Bob does not read it before
> then.
>
> Note that Versions 0.4 and 0.4.1 do not have that false positive.
>
>
> unguarded_bob.vp
> ----------------
>
> expected 1 result:
>
> - plaintext  is obtained by attacker
>
> Instead, I got 2:
>
> - plaintext  is obtained by attacker
> - ad is sent by attacker instead of Alice
>
> Now, `ciphertext` is no longer considered forged, which is good. I
> suspect that the `ad` result comes from the same error that caused the
> false positive in ok.vp.
>
> Note that versions 0.4 and 0.4.1 have all 3 results (just like version
> 0.3).
>
>
> unguarded_alice.vp
> ------------------
>
> expected 2 results
>
> - ciphertext is sent by attacker instead of Alice
> - ad         is sent by attacker instead of Alice
>
> And we got exactly that! No more missed attacks. (Looks like this was
> corrected in 0.4.1)
>
>
> unchecked_aead.vp
> -----------------
>
> You should expect a green light (I have a different opinion, but let's
> keep that for later), but instead we got:
>
> - ad is sent by attacker instead of Alice
>
> Again, that's probably the same false positive as the one in ok.vp.
>
>
> no_decryption.vp
> ----------------
>
> Expected a green light, got a green light. Good enough for version 0.5,
> but I do wish to add that warning about Bob not reading something we
> check the authentication of.
>
>
> ---
>
> Now let us discuss. :-)
>
>
> > > The AEAD_DEC primitive is not checked, so the attacker can send
> > > whatever garbage they want, and Bob will successfully read it. We
> > > could *perhaps* split hairs and pretend `ad` wasn't really read,
> > > but `ciphertext` was definitely used to generate `plaintext_`.
> > > Either way, Verifpal should detect the possibility of forgery.
> >
> > Ah, here you are misinterpreting what I think is a perfectly correct
> > result, and it is again due to the misunderstanding over what checked
> > primitives do.
> > Checked primitives halt that particular execution of the protocol in
> > the case that a rewrite rule fails. Whether AEAD_DEC is checked or
> > not, it will not decrypt successfully in the presence of garbage
> > `ciphertext` or `ad`. Since both public keys are guarded, then such a
> > false decryption is impossible in this model.
>
> Ok, I see where you are coming from. For instance, if we're using
> Libsodium's secret_box_easy(), there's no additional data to worry
> about, and if the tag is wrong, there won't be any plaintext coming
> from the attacker. Even if there *was* additional data, we could
> imagine a combined mode where it wouldn't be copied to the destination
> buffer if the tag is wrong.
>
> With such an API, you would be right: failing to check the return code
> can hardly have any nefarious consequence (at least none that are the
> attacker's design).
>
> There are other APIs however that are much more problematic. Monocypher
> for instance has a streaming API users can use to handle huge buffers.
> Problem is, the authentication tag can only be confirmed when the
> message is already decrypted! (Libsodium solves the problem by
> authenticating each chunk separately, but this approach makes it
> incompatible with the monolithic interface. Monocypher chose to put
> blinking warnings in the manual.)
>
> With such an API, the user *can* forget to check the tag, and still end
> up with a decrypted message that the attacker controls.
>
> To sum this up:
>
> - The additional data doesn't have to be decrypted, it can be read
>   before we check the tag.
> - The ciphertext *can* be falsely decrypted with some dangerous APIs.
> - Even if it can't, the (unchecked) primitive still produces a
>   plaintext. Garbage plaintext perhaps, but still nonsensical
>   plaintext. I wonder how this affect the analysis.
>
> Now I'm not asking that you change this part of the model. Worst case,
> I can do aead manually with ENC/DEC and HMAC/HMACVERIF, and test false
> decryptions by removing the HMACVERIF line. As an optional behaviour
> perhaps? And there's still the additional data to contend with. Maybe
> merely performing AEAD_DEC on it doesn't count as "reading", but it
> still makes me feel a bit uneasy.
>
> ---
>
> Finally, some more tests: same trivial handshake, except this time we
> are using HMAC manually.
>
> hmac_ok.vp
> ----------
>
> Expected a green light.
>
> Version 0.3 gives me that green light.
> Version 0.4 believes ciphertext is vulnerable to forgery.
>
> Git bisect says the error has apparently been introduced by the 89aa3d1
> commit, named "HIGHLY EXPERIMENTAL".
>
> Do check that my model (attached) is correct, though. I'm tired right
> now, I may have made a mistake.
>
> ---
>
> I feel we are slowly getting somewhere. Keep it up! (Also, it's
> wonderful that you have someone taking care of the test suite. We kinda
> need it yesterday, though, could you give your intern a time machine?
> Or maybe a few lashes, that could work too. :-)
>
> Loup.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190905/5678b019/attachment.htm>