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

[Loup Vaillant David]

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 --------------
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
]