**Strand Spaces**

by Javier Thayer, Jonathan Herzog, and Joshua Guttman

**Analysing a Protocol**

1. Describe the protocol as a *strand*
(which is simple kind of graph)

2. Describe the attacker as *strands*

3. Make simple (inductive) proofs over sets of strands (containing 1. and 2.) to guarantee security properties of the protocol

Technical University of Denmark / Informatics and Mathematical Modelling / Safe and Secure IT-Systems

**An Example**

Needham-Schroeder-Lowe public key:

◦

◦

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

Technical University of Denmark / Informatics and Mathematical Modelling / Safe and Secure IT-Systems

**An Example**

Needham-Schroeder-Lowe public key:

◦

◦

◦

◦
{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

**An Example**

Needham-Schroeder-Lowe public key:

◦

◦

◦

◦
{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

Init[A, B, N^{a}, N^{b}] Resp[A, B, N^{a}, N^{b}]

Technical University of Denmark / Informatics and Mathematical Modelling / Safe and Secure IT-Systems

**An Example**

Needham-Schroeder-Lowe public key:

◦

◦

◦

◦
{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{N }

**Messages Consist of Terms**

Terms t ∈ A are built by

t ::= K keys from the set K

| T text from the set T

| {t}^{K} encryption

| t^{1} t^{2} concatenation
K and T are disjoined sets

K is equipped with an operation inv : K → K.
We write inv(K) as K^{−}^{1}.

**Definitions**

s

◦

◦

◦

t1

t^{2}

t3

**Definitions**

s

◦

◦

◦

t1

t^{2}

t3

tr(s) = (+t1, −t2, +t3) +t1

−t^{2}

+t3

**Definitions**

s (s, 1)

(s, 2)

(s, 3)

t1

t^{2}

t3

(s, 1) ∈ N

index((s, 1)) = 1
term((s, 1)) = +t^{1}

uns_term((s, 1)) = t^{1}

**Definitions**

s n1

n^{3}

n5

n2

n^{4}

n6

s^{0} ⇒⊆ N × N

→⊆ N × N

⇒ ∪ → is the edge relation in a directed graph

_{C} is the reflexive, transitive
closure of C ⊆ ⇒ ∪ →

**Bundles**

**Definition** Let C be a set of edges and N_{C} be
corresponding nodes. This graph is a *bundle* if:

C is finite and acyclic

If n^{2} ∈ N_{C} and term(n^{2}) is negative, then there is
a unique n^{1} such that n^{1} → n^{2} ∈ C

If n^{2} ∈ N_{C} and n^{1} ⇒ n^{2} then n^{1} ⇒ n^{2} ∈ C

Summary: Bundles are causally well-founded strand spaces

**Well-founded Partial Order**

n1

n^{3}

n5

n2

n^{4}

n6

**Lemma 2.6**

Let C be a bundle. Then _{C}
is a partial order (i.e. it is
also anti-symmetric).

Every non-empty subset of nodes in C has a minimal element (i.e. the nodes are a well-ordered set).

**A Simple Proof**

n1

n^{3}

n5

n2

n^{4}

n6

**Lemma 2.7**

Let C be a bundle. If n is a
_{C}-minimal element of N_{C}
then term(n) is positive.

**A Simple Proof**

n1

n^{3}

n5

n2

n^{4}

n6

**Lemma 2.7**

Let C be a bundle. If n is a
_{C}-minimal element of N_{C}
then term(n) is positive.

Also holds for subsets, S,
of N_{C} whenever both n^{1}
and n are in S for all

**Penetrator Strands**

M

◦ T

for T ∈ T

F

◦ t

T

◦

◦

◦

t t t

C

◦

◦

◦

t1

t^{2}
t^{1} t^{2}

◦

◦

◦

t1 t2

t1

t2

◦ K

for K ∈ KP

◦

◦

◦

K
t
{t}^{K}

◦

◦

◦

K^{−}^{1}
{t}^{K}

t

**A Proposition about Penetrators**

**Proposition 3.3** Let C be a bundle and let K be a
key not in KP.

If K never originates on a regular node, then

K 6@ term(p) for node p on a penetrator strand in C.

Note: t *originates at* n means that t @ term(n), that
term(n) is positive, and that t is not a sub-term of
any preceding node on the same strand

Note: t @ t means that t is a sub-term of t , which

**A Proposition about Penetrators**

**Proposition 3.3** Let C be a bundle and let K be a
key not in KP.

If K never originates on a regular node, then

K 6@ term(p) for node p on a penetrator strand in C.
**Proof strategy**

Consider the set S = {n ∈ C | K @ term(n)}

Show that S is empty — by contradiction S has a minimal element (Lemma 2.6)

**Proving a Protocol Correct**

1. Define a strand space, Σ, consisting of strands describing the protocol

penetrator strands

2. Write down the property you want to hold
3. Prove this by considering all *bundles* of Σ

**NSL-spaces**

**Definition** An NSL-space consists only of

Init[A, B, N^{a}, N^{b}]-strands, Resp[A, B, N^{a}, N^{b}]-strands,
and penetrator strands.

◦

◦

◦

◦
{N^{a} A}^{K}_{B}

{Na Nb B}^{K}_{A}

{N^{a} A}^{K}_{B}

{Na Nb B}^{K}_{A}

Init[A, B, Na, Nb] Resp[A, B, Na, Nb]

**Authentication**

The right principals should communicate Formulated as:

When a responder ends a protocol run, a unique initiator must have been present NSL-space

Resp[A, B, Na, Nb]

◦

◦

**Authentication**

The right principals should communicate Formulated as:

When a responder ends a protocol run, a unique initiator must have been present NSL-space

Resp[A, B, Na, Nb]

◦ here ◦

then there is a

Init[A, B, Na, Nb]

◦

◦

**Authentication**

**Proposition 4.2** For all bundles C of an NSL-space
if

1. there is a strand Resp[A, B, N^{a}, N^{b}] in C
3. N^{a} 6= N^{b} and N^{b} is uniquely originating in C

then there is a strand Init[A, B, N^{a}, N^{b}] in C.
**Proof strategy**

Fix an arbitrary C where 1., 2., and 3. hold

Show that N^{b} is manipulated by a *regular* strand
Show that this strand is Init[A, B, N^{a}, N^{b}]

**Authentication**

**Proposition 4.2** For all bundles C of an NSL-space
if

1. there is a strand Resp[A, B, N^{a}, N^{b}] in C
2. K_{A}^{−}^{1} 6∈ K^{P}

3. N^{a} 6= N^{b} and N^{b} is uniquely originating in C
then there is a strand Init[A, B, N^{a}, N^{b}] in C.

Fix an arbitrary C where 1., 2., and 3. hold

Show that N^{b} is manipulated by a *regular* strand
Show that this strand is Init[A, B, N^{a}, N^{b}]

**Authentication**

**Proposition 4.2** For all bundles C of an NSL-space
if

1. there is a strand Resp[A, B, N^{a}, N^{b}] in C
2. K_{A}^{−}^{1} 6∈ K^{P}

3. N^{a} 6= N^{b} and N^{b} is uniquely originating in C
then there is a strand Init[A, B, N^{a}, N^{b}] in C.

**Proof strategy**

Fix an arbitrary C where 1., 2., and 3. hold

Show that N is manipulated by a *regular* strand

**Authentication of NSL**

◦

n^{0}

n3

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{Nb}^{K}_{B}
Init[A, B, Na, Nb] is unique.

**Authentication of NSL**

◦

n^{0}

n3

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{Nb}^{K}_{B}

{n ∈ C | N^{b} @ term(n) ∧

{N^{a} N^{b} B}^{K}_{A} 6@ term(n)}

has a minimal element, n^{2},
which is *regular* and positive

n2

. . . N^{b} . . .
Init[A, B, Na, Nb] is unique.

**Authentication of NSL**

◦

n^{0}

n3

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{Nb}^{K}_{B}
n2

. . . N^{b} . . .
n^{1} {N^{a} N^{b} B}^{K}_{A}

Some node n1 precedes n2

and {N^{a} N^{b} B}^{K}_{A} @ term(n^{1})

...

Init[A, B, Na, Nb] is unique.

**Authentication of NSL**

◦

n^{0}

n3

{N^{a} A}^{K}_{B}

{N^{a} N^{b} B}^{K}_{A}

{Nb}^{K}_{B}
n2

. . . N^{b} . . .
n^{1} {N^{a} N^{b} B}^{K}_{A}

Can only be a regular initiator strand:

◦ {N^{a} A}^{K}_{A}

**Summary of Authentication Proof**

**Proof strategy**

Fix an arbitrary C where 1., 2., and 3. hold

Show that N^{b} is manipulated by a *regular* strand
Show that this strand is Init[A, B, N^{a}, N^{b}]

**In retrospect**

The difficult part was establishing that there was
a *regular* strand

The rest was just reading off parameters

**Authentication Tests**

There is a general result about an *outgoing tests:*

If a bundle C contains

◦

◦

{. . . N . . .}^{K}

t

N originate uniquely here; and K 6∈ KP

N @ t and {. . . N . . .}^{K} @ t
then there is a *regular* transforming edge in C.

**Using an Outgoing Test**

◦

◦

◦

◦

◦

◦
{N^{a} A}^{K}_{B}

{Na Nb B}^{K}_{A}

{N^{b}}^{K}_{B}

{N^{a} A}^{K}_{B}

{Na Nb B}^{K}_{A}

{N^{b}}^{K}_{B}

**Confidentiality of** N

_{b}

**Proposition 4.10** Let C be a bundle of an
NSL-space where

1. there is a strand Resp[A, B, N^{a}, N^{b}] in C
2. K_{A}^{−}^{1} 6∈ K^{P} and K_{B}^{−}^{1} 6∈ K^{P}; and

3. N^{a} 6= N^{b} and N^{b} is uniquely originating in C

Then for all nodes m ∈ C such that N^{b} @ term(m),

either {N^{a} N^{b} B}^{K}_{A} @ term(m) or {N^{b}}^{K}_{B} @ term(m).
In particular, Nb 6= term(m).

**Analysing a Protocol**

1. Describe the protocol as a *strand*
(which is simple kind of graph)

2. Describe the attacker as *strands*

3. Make simple proofs over sets of strands

(containing 1. and 2.) to guarantee security properties of the protocol