[Verifpal] Simple challenge/response with freshness

Nadim Kobeissi nadim at symbolic.software
Fri Aug 14 12:00:11 CEST 2020


I’m going to summarize here the discussion I had with Eric on the Discord for the public interest.

Consider this suggestion:
https://verifhub.verifpal.com/5fa621aa8a8718ec136814588c31693c

On line 26, I added a hashing of `br` to indicate that it's being used by Bob as part of the protocol somewhere after being authenticated by the checked ASSERT of the MAC and not before (necessary for authentication queries to mean anything). Since Alice will check it against `anonce`, which is fresh, we have a guarantee of freshness. If you remove the check on the ASSERT, you get this:

   Result • authentication? Bob -> Alice: br[
                precondition[Alice -> Bob: done]
        ] — When:
            br → done ← mutated by Attacker (originally MAC(psk, anonce))
            unnamed_0 → ASSERT(done, MAC(psk, anonce))
            unnamed_1 → HASH(done)
            br (done), sent by Attacker and not by Bob, is successfully used in HASH(done) within Alice's state.
            Furthermore, the following query options fail:
             - Alice sends done to Bob despite the query failing.

The part you care about here specifically is the "Furthermore…"

This is the best way to illustrate what you want, I think. The result you were being given by the freshness query is actually correct but not what you actually want: br (MAC(psk, nil)) is not a fresh value. If used as a message, it could be replayed, leading to potential replay attacks. It's warning you that br wouldn't be useful as a fresh element in any message/key/payload etc. so you shouldn't use it there if you need guaranteed freshness.

If psk was declared using generates I suspect you'd have a different result. But then you wouldn't be able to just "generate" the same PSK on both Alice and Bob's side, as that doesn't make sense given that it would be random…

Eric then said:
"Hmm, I understand the attacker can modify br to be a non-fresh value, but since it's authenticated under psk, shouldn't this cause the assert to fail?”

To which I responded:
"Yes and it does fail as shown in the authentication query. But the freshness query here checks whether br can *ever* be made non-fresh.”

And then I later said:
"Perhaps this behavior should be changed and we should check if it's ever USED anywhere without being fresh. Not just whether it can ever be non-fresh.”

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

> On 13 Aug 2020, at 10:36 PM, Eric Simpson via Verifpal <verifpal at lists.symbolic.software> wrote:
> 
> I'm trying to do some basic usage of verifpal.  I'm having problems trying to express a "freshness" requirement for a challenge/response protocol.  Could I get some insight as to why the below protocol description is failing:
> 
> I'd like to model an anti-replay characteristic with the freshness query.  Is the freshness query the correct approach?
> 
> In addition, I'd like to only use MAC/HASH primitives to accomplish this.
> 
> From my understanding, I'd expect the below protocol to be valid from an anti-replay perspective assuming "generates anonce" is the correct way to express a session nonce.
> 
> Code is below:
> 
> attacker [active]
> 
> // ------------------------------------
> // Setup
> // ------------------------------------
> principal alice [
> knows private psk
> ]
> 
> principal bob [
>     knows private psk
> ]
> 
> // ------------------------------------
> // Attempting to model a challenge/response type protocol
> // with anti-replay
> //
> // Protocol "freshness" fails when "anonce -> nil"
> //
> // Questions:
> // 1. Is this a valid assumption by the analyzer?
> // 2. Is there an ASSERT(nonce != nil) approach that is valid?
> // ------------------------------------
> principal alice [
> generates anonce
> ]
> 
> alice -> bob: anonce
> 
> principal bob [
>     br = MAC(psk, anonce)
> ]
> 
> bob -> alice: br
> 
> principal alice [
>     br_expected = MAC(psk, anonce)?
>     _ = ASSERT(br, br_expected)?
>     generates done
> ]
> 
> alice -> bob: done
> 
> queries[
> authentication? bob -> alice: br
>     freshness? br[
>         precondition[alice -> bob: done]
>     ]
> ]
> 
> The output is:
> 
> 
>  Verifpal • Verification completed for 'replay-simple.vp' at 04:18:59 PM. 
>  Verifpal • Summary of failed queries will follow. 
> 
>    Result • freshness? br[
>                 precondition[Alice -> Bob: done]
>         ] — When:
>             anonce → nil ← mutated by Attacker (originally anonce)
>             br → MAC(psk, nil)
>             unnamed_0 → ASSERT(MAC(psk, nil), MAC(psk, anonce))?
>             br (MAC(psk, nil)) is not a fresh value. If used as a message, it could be replayed, leading to potential replay attacks.
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal



More information about the Verifpal mailing list