Analysing a Protocol

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¹ t² concatenation K and T are disjoined sets

K is equipped with an operation inv : K → K. We write inv(K) as K⁻¹.

Definitions

s

◦

◦

◦

t1

t²

t3

Definitions

s

◦

◦

◦

t1

t²

t3

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

−t²

+t3

Definitions

s (s, 1)

(s, 2)

(s, 3)

t1

t²

t3

(s, 1) ∈ N

index((s, 1)) = 1 term((s, 1)) = +t¹

uns_term((s, 1)) = t¹

Definitions

s n1

n³

n5

n2

n⁴

n6

s⁰ ⇒⊆ 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² ∈ N_C and term(n²) is negative, then there is a unique n¹ such that n¹ → n² ∈ C

If n² ∈ N_C and n¹ ⇒ n² then n¹ ⇒ n² ∈ C

Summary: Bundles are causally well-founded strand spaces

Well-founded Partial Order

n1

n³

n5

n2

n⁴

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³

n5

n2

n⁴

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³

n5

n2

n⁴

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¹ and n are in S for all

Penetrator Strands

M

◦ T

for T ∈ T

F

◦ t

T

◦

◦

◦

t t t

C

◦

◦

◦

t1

t² t¹ t²

◦

◦

◦

t1 t2

t1

t2

◦ K

for K ∈ KP

◦

◦

◦

K t {t}^K

◦

◦

◦

K⁻¹ {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]

◦

◦

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

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]

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

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⁻¹ 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⁻¹ 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

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

Authentication of NSL

◦

n⁰

n3

{N^a A}^K_B

{N^a N^b B}^K_A

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

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

Authentication of NSL

◦

n⁰

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², which is regular and positive

n2

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

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

Authentication of NSL

◦

n⁰

n3

{N^a A}^K_B

{N^a N^b B}^K_A

{Nb}^K_B n2

. . . N^b . . . n¹ {N^a N^b B}^K_A

Some node n1 precedes n2

and {N^a N^b B}^K_A @ term(n¹)

...

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

Authentication of NSL

◦

n⁰

n3

{N^a A}^K_B

{N^a N^b B}^K_A

{Nb}^K_B n2

. . . N^b . . . n¹ {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

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⁻¹ 6∈ K^P and K_B⁻¹ 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