[Verifpal] Authentication after sending a new private key

Nadim Kobeissi nadim at symbolic.software
Mon Aug 17 16:25:03 CEST 2020


Verifpal 0.19.1 fixes this issue.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Fri, Aug 14, 2020 at 5:34 PM Eric Simpson via Verifpal
<verifpal at lists.symbolic.software> wrote:

> 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
>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200817/802efdd9/attachment.htm>


More information about the Verifpal mailing list