[Verifpal] Authentication after sending a new private key

Eric Simpson simpson.eric at gmail.com
Fri Aug 14 17:34:18 CEST 2020


Test case goal:

- [Offline] Alice and Bob have a pre-shared key
- [Online] Alice wants to share a new static secret key with Bob
- [Online] Bob receives new key from alice
- [Online] Bob verifies to Alice he knows the new key

Test case result:

- The authentication query from Bob-to-Alice fails at the end

Thoughts:

In this protocol, I believe it's valid to say that either Alice
or Bob could have sent the final message below:

  bob -> alice: br

Since 'anonce' is freshly generated in each session, I'm not sure
it's valid to say an Attacker could generate/replay the message.

Questions:

1. Is this a correct result from the verifpal output?
2. Is there another way I should express this in verifpal?


// Begin Code -----------------------------------------------------
attacker [active]

// ------------------------------------
// Offline Setup
// ------------------------------------
principal alice [
    knows private psk
    knows private alice_key
]
principal bob [
    knows private psk
]

// ----------------------------------------------------------------
// Online exchange where Alice encrypts new key to Bob
// ----------------------------------------------------------------
principal alice [
    generates anonce
    encVal = AEAD_ENC(psk, alice_key, anonce)
]

alice -> bob: anonce, encVal

// ----------------------------------------------------------------
// Here Bob receives new key from Alice, and proves knowledge of
// new key by computing MAC over a nonce and sending result to
// alice.
// ------------------------------------
principal bob [
    bob_key = AEAD_DEC(psk, encVal, anonce)?
    br = MAC(bob_key, anonce)
]

bob -> alice: br

principal alice [
    br_expected = MAC(alice_key, anonce)
    _ = ASSERT(br_expected, br)
    generates done
]

alice -> bob: done

queries[
    // These two queries pass
    confidentiality? alice_key
    authentication? alice -> bob: encVal

    // This query fails authentication
    authentication? bob -> alice: br[
        precondition[alice -> bob: done]
    ]
]
// End Code -------------------------------------------------------

// Results Begin
Verifpal - Verification completed for 'nonce-auth.vp' at 08:49:07 AM.
Verifpal - Summary of failed queries will follow.

Result - authentication? Bob -> Alice: br[
            precondition[Alice -> Bob: done]
    ] — When:
        bob_key → alice_key
        br → MAC(alice_key, anonce) ← obtained by Attacker
        unnamed_0 → ASSERT(MAC(alice_key, anonce), MAC(alice_key, anonce))

        In another session:
        bob_key → alice_key
        br → MAC(alice_key, anonce) ← mutated by Attacker (originally
MAC(bob_key, anonce))
        unnamed_0 → ASSERT(MAC(alice_key, anonce), MAC(alice_key, anonce))
        br (MAC(alice_key, anonce)), sent by Attacker and not by Bob,
is successfully used in ASSERT(MAC(alice_key, anonce), MAC(alice_key,
anonce)) within Alice's state.
        Furthermore, the following query options fail:
            - Alice sends done to Bob despite the query failing.
// Results end


More information about the Verifpal mailing list