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

[Nadim Kobeissi]

Just pushed 0.4.1. I’m calling the 0.4.x release branch “Valiant Wolf’s Challenge”, as I’ve decided that we won’t move to 0.5 until we’ve addressed all the issues Loup points out using basic models.

There’s still stuff he’s pointed out that’s not implemented yet even in 0.4.1, for example warnings on unused authentication query values.

Once Loup is satisfied we will move to 0.5.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 4, 2019, at 1:44 PM, Nadim Kobeissi <nadim at symbolic.software> wrote:
> 
> Thanks Loup, this is exactly what I was hoping for.
> 
>> ok.vp
>> -----
>> 
>> Expected a green light, got a green light. So far so good.
> 
> Great.
> 
>> unguarded_bob.vp
>> ----------------
>> 
>> expected 1 result:
>> 
>> - plaintext  is obtained by attacker
>> 
>> Instead, I got 2:
>> 
>> - plaintext  is obtained by attacker
>> - ciphertext is sent by attacker instead of Alice
>> 
>> I see two errors blended in one: first, ciphertext and ad are verified
>> by the same checked primitive. If one can be forged, so can the other.
>> We should see either 2 authentication results, or zero.
>> 
>> Second, the attacker cannot forge anything here. Alice's key has been
>> sent securely to bob (because it was guarded), and no secret key was
>> leaked. Bob's ability to authenticate incoming messages is intact.
> 
> I hope that the commit I just pushed addresses this class of errors. Please keep testing.
> 
>> unguarded_alice.vp
>> ------------------
>> 
>> expected 2 results
>> 
>> - ciphertext is sent by attacker instead of Alice
>> - ad         is sent by attacker instead of Alice
>> 
>> Verifpal missed both results, and gave the green light.
>> 
>> Here's the attack: Alice sends her public key to Bob, over an
>> *insecure* channel. The attacker intercepts that key, and give their
>> own to Bob instead. Then the attacker does what Alice would have done
>> except with their own plaintext and ad. In the end, Bob authenticates a
>> ciphertext and an ad that came from the attacker, instead of Alice.
> 
> Yup, indeed a missed attack. I was able to further address this in the commit I just pushed, and I hope that we can now improve our capacity to handle these attacks. Please keep testing.
> 
>> unchecked_aead.vp
>> -----------------
>> 
>> expected 2 results:
>> 
>> - ciphertext is sent by attacker instead of Alice
>> - ad         is sent
>> by attacker instead of Alice
>> 
>> 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.
> 
> I am comfortable with Verifpal’s existing result in this model. It is fully correct and sensible.
> 
>> no_decryption.vp
>> ----------------
>> 
>> Expected 1 warning:
>> 
>> - ciphertext and ad are sent to Bob, but not used.
>> 
>> Technically, the attacker can forge them and Bob would not notice. But
>> if Bob doesn't read the values, such forgeries simply have no effect.
>> This is not a vulnerability, and Verifpal has no reason to report a
>> result.
>> 
>> On the other hand, we wrote a query about those values. In most
>> contexts, this means we care about their authentication. If Bob does
>> not read them, we probably forgot something, and we should be warned
>> about it.
> 
> An early version of Verifpal had exactly this warning, but it was removed before 0.1 was released since I was wondering whether it would be useful or not. I’ll bring it back, you make a good case for its existence.
> 
>> If I may, I believe you need an automated test suite (I took a very
>> quick look, didn't see one). Just start with a couple models, along
>> with expected results. Finding more or fewer results than expected
>> means you have a bug (or that you expect the wrong things…). Later,
>> some property based tests may also help: for instance, a passive
>> attacker should never find more attacks than an active attacker.
> 
> We are indeed working on an automated test suite as we speak — I have an intern who’s tasked to spend September creating just that.
> 
> Keep ‘em coming, Loup. This is extremely valuable and we are on the right track towards progress here. Thanks so much for your help.
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
>> On Sep 4, 2019, at 1:06 AM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
>> 
>> Just to be clear: by "missed attack", I mean that I think the model is
>> vulnerable somehow, yet Verifpal gave me the green light.
>> 
>> Here are 4 files (attached), that illustrate the problem. I believe
>> version 0.3 gives the same results as 0.4.
>> 
>> 
>> ok.vp
>> -----
>> 
>> Expected a green light, got a green light. So far so good.
>> 
>> 
>> unguarded_bob.vp
>> ----------------
>> 
>> expected 1 result:
>> 
>> - plaintext  is obtained by attacker
>> 
>> Instead, I got 2:
>> 
>> - plaintext  is obtained by attacker
>> - ciphertext is sent by attacker instead of Alice
>> 
>> I see two errors blended in one: first, ciphertext and ad are verified
>> by the same checked primitive. If one can be forged, so can the other.
>> We should see either 2 authentication results, or zero.
>> 
>> Second, the attacker cannot forge anything here. Alice's key has been
>> sent securely to bob (because it was guarded), and no secret key was
>> leaked. Bob's ability to authenticate incoming messages is intact.
>> 
>> 
>> unguarded_alice.vp
>> ------------------
>> 
>> expected 2 results
>> 
>> - ciphertext is sent by attacker instead of Alice
>> - ad         is sent by attacker instead of Alice
>> 
>> Verifpal missed both results, and gave the green light.
>> 
>> Here's the attack: Alice sends her public key to Bob, over an
>> *insecure* channel. The attacker intercepts that key, and give their
>> own to Bob instead. Then the attacker does what Alice would have done
>> except with their own plaintext and ad. In the end, Bob authenticates a
>> ciphertext and an ad that came from the attacker, instead of Alice.
>> 
>> 
>> 
>> unchecked_aead.vp
>> -----------------
>> 
>> expected 2 results:
>> 
>> - ciphertext is sent by attacker instead of Alice
>> - ad         is sent
>> by attacker instead of Alice
>> 
>> 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.
>> 
>> 
>> no_decryption.vp
>> ----------------
>> 
>> Expected 1 warning:
>> 
>> - ciphertext and ad are sent to Bob, but not used.
>> 
>> Technically, the attacker can forge them and Bob would not notice. But
>> if Bob doesn't read the values, such forgeries simply have no effect.
>> This is not a vulnerability, and Verifpal has no reason to report a
>> result.
>> 
>> On the other hand, we wrote a query about those values. In most
>> contexts, this means we care about their authentication. If Bob does
>> not read them, we probably forgot something, and we should be warned
>> about it.
>> 
>> ---
>> 
>> If I may, I believe you need an automated test suite (I took a very
>> quick look, didn't see one). Just start with a couple models, along
>> with expected results. Finding more or fewer results than expected
>> means you have a bug (or that you expect the wrong things…). Later,
>> some property based tests may also help: for instance, a passive
>> attacker should never find more attacks than an active attacker.
>> 
>> Loup.
>> 
>> <no_decryption.vp><ok.vp><unchecked_aead.vp><unguarded_alice.vp><unguarded_bob.vp>
>> _______________________________________________
>> Verifpal mailing list
>> Verifpal at lists.symbolic.software
>> https://lists.symbolic.software/mailman/listinfo/verifpal
>