[Verifpal] Simple challenge/response with freshness

Eric Simpson simpson.eric at gmail.com
Thu Aug 13 22:36:40 CEST 2020


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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200813/17820224/attachment.htm>


More information about the Verifpal mailing list