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

[Loup Vaillant David]

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.

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

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
    authentication? Alice -> Bob : ad
]
-------------- 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)?
]

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
    authentication? Alice -> Bob : ad
]
-------------- 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)
]

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
    authentication? Alice -> Bob : ad
]
-------------- 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)?
]

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
    authentication? Alice -> Bob : ad
]
-------------- 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)?
]

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