Tutorial: A Simple Unilateral Authentication Protocol

This is a introductory tutorial for the StrandsRocq framework which illustrates a simple unilateral authentication protocol based on nonces. The initiator A sends a fresh nonce Na to the responder B who encrypts it together with A's identifier under a symmetric key SK A B shared with A. The protocol in the Alice/Bob notation follows:
A → B : A ⋅ B ⋅ Na
B → A : ⟨ Na ⋅ A ⟩_(SK A B)

We use ⟨ M ⟩_k to note the encryption of M under key k and M1 ⋅ M2 to denote the concatenation of M1 and M2. From now onwards we assume basic familiarity with the Strand spaces framework, for more information please refer to our paper or the original Strand spaces paper. We begin by importing some standard packages.

StrandsRocq provides some default instances for the universes, the terms, and the penetrator. These can be easily imported as follows.

Protocol Specification and Roles

The first step consists in specifying the protocol within our framework by inductively defining all the possible strands the participants can execute. A strand is just a pair (i, tr), where i is a natural number identifying the strand and tr is a trace. So, specifying the strands amounts to specifying the corresponding traces, since the identifier is immaterial and is usually universally quantified. In this simple protocol, the initiator and responder each execute a single strand, parameterized by the principal names A and B and the nonce Na. In general, each principal may execute multiple strands, as is the case with the penetrator. The initiator sends the principal names A and B, and a fresh nonce Na as output and reads the expected answer ⟨ Na ⋅ A ⟩_(SK A B) from the responder. Since the type of A, B, Na is T, representing atomic terms, we write $Na to represent those values as generic term of type 𝔸. Symbols ⊕ and ⊖ respectively represent output and input nodes. Thus, the corresponding trace is [ ⊕ $A ⋅ $B ⋅ $Na; ⊖ ⟨ $Na ⋅ $A ⟩_(SK A B) ]. Given A, B, Na, initiator strands execute this trace, while responder strands execute the dual trace (with ⊖ and ⊕ exchanged), as formalized below:

Finally, we define the protocol strand space as the combination of penetrator strands along with initiator and responder strands, parameterized by the penetrator's keys K__P:

We are now ready to prove our first fact: no symmetric key SK U U' ever originates on a regular strand, i.e., neither the initiator nor the responder send symmetric keys as protocol messages.

Protocol Security

We consider a strand s, a bundle C, principals A, B, and a nonce Na. All of these variables are generic and thus universally quantified in this section, allowing statements to be more readable.

We assume that:

• C is a bundle of the protocol strand space, where fun k ⇒ k ≠ SK A B specifies that the attacker knows any key except SK A B for the given A and B. Notice that the attacker knows the key of any other participant. This assumption is the minimal requirement for ensuring protocol security with respect to the given principals A and B;
• s is an initiator strand with parameters A, B, Na;
• s is a strand of bundle C.

C is a indeed bundle. This is useful for next definitions and proof.

We now prove unilateral authentication properties of the protocol from the initiator's perspective.

Non-injective agreement

The first security property states that the initiator is guaranteed that the responder run the protocol and agreed on parameters A, B and Na. Formally:
    ∃ s' : Σ,
      SA_responder_strand A B Na s' ∧
        is_strand_of s' C.
  

The proof revolves around showing that only the responder, with parameters A, B and Na, can generate the expected ciphertext ⟨ $Na ⋅ $A ⟩_(SK A B). We define the set of nodes belonging to bundle C, that have ⟨ $Na ⋅ $A ⟩_(SK A B) as subterm. First, we define a function Ncp from terms to Prop that checks if c ⊏ t and we prove its decidability. Then, we partially instantiate N, N_iff_inC_p and minimal_N_then_mpt from MinimalMPT.v in order to respectively define

• Nc : the set of nodes whose term satisfy Ncp;
• Nc_iff_inC_Ncp : the logical characterization of nodes belonging to Nc, i.e., In n (nodes_of C) ∧ Ncp (uns_term n)
• minimal_Nc_then_mpt : a lemma that allows to characterize the minimal of Nc as a Prop.

We now prove that Nc is not empty. This trivially comes from the fact that the term of second node of the initiator strand is indeed equal to ⟨ $Na ⋅ $A ⟩_(SK A B)

We now prove noninjective agreement. The proof is based on lemma exists_minimal_bundle stating that each nonempty subset of nodes has a minimal with respect to the bundle_le (⪯) relation. We apply the lemma to Nc. This minimal node is, intuitively, the one that performs the encryption in ⟨ $Na ⋅ $A ⟩_(SK A B). We reason by cases and we prove that this minimal node cannot lie neither on a Penetrator nor on an Initiator strand. It lies instead on a Responder strand whose parameters can be proved to be exactly A, B and Na, as required by the agreement property. Notice, in fact, that ⟨ $Na ⋅ $A ⟩_(SK A B) contains A, Na in the payload and B, implicitly, in the key SK A B.

Penetrator case

we now use the minimal_Nc_then_mpt lemma which provides a characterization of the minimal element of Nc in terms of a Prop covering all the possible cases.

For example, for the first case, which is the output of an atomic term t written [⊕ $ t] we obtain the following Prop: False ∨ ⟨ $ Na ⋅ $ A ⟩_ SK A B = $ t ∧ True ∧ index m = 0, stating that ⟨ $ Na ⋅ $ A ⟩_ SK A B = $ t, which is clearly false since $ t is an atomic term. In other cases the Prop is more complicate. For example, for pair generation [⊖ g; ⊖ h; ⊕ g ⋅ h] we obtain
      ((False ∨
        (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ g ∧
        False ∧ index m = 0) ∨
        ¬ (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ g ∧
        (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ h ∧
        False ∧ index m = 1) ∨
      ¬ (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ g ∧
      ¬ (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ h ∧
      (⟨ $ Na ⋅ $ A ⟩_ SK A B = g ⋅ h ∨
        (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ g ∨
        (⟨ $ Na ⋅ $ A ⟩_ SK A B) ⊏ h) ∧
      True ∧ index m = 2

that is less trivial to analyze by hand. We developed a tactic named simplify_prop, which simplifies the Prop by eliminating all cases except the nontrivial ones. For this protocol, the only nontrivial case is encryption: [⊖ # (SK A B); ⊖ $ Na ⋅ $ A; ⊕ c], the only penetrator strand that generates a ciphertext.

We easily eliminate this case by exploiting the fact that the penetrator can never learn a secure symmetric key, in this case SK A B.

Initiator case: this is trivially solved by the simplify_prop tactic

Responder case:

Here we have two cases depending whether A and B are equal or not. Both cases are solved trivially as they provide a valid binding for the protocol parameters.

Injective agreement

The second security property additionally states that each responder session correspond to different initiator session, i.e., that authentication is injective and cannot be reused in a replay attack. This property only holds if Na is freshly generated which, in the strand spaces model, is captured by the uniquely_originates definition. Formally:
  uniquely_originates $Na →
    (
      ∃ s' : Σ,
        SA_responder_strand A B Na s' ∧
        is_strand_of s' C
    )
    ∧
    (
      ∀ s'' : Σ,
        SA_initiator_strand A B Na s'' →
        s'' = s
    ).

We first prove injectivity alone, i.e., if Na uniquely originates then there's a unique initiator trace agreeing on Na. The proof just applies the definition on uniquely_originates:

From noninjective_agreement and injectivity we obtain injective agreement as a corollary: