• Ingen resultater fundet

# Analysing a Protocol

N/A
N/A
Info
Protected

Del "Analysing a Protocol"

Copied!
34
0
0

Indlæser.... (se fuldtekst nu)

Hele teksten

(1)

### Strand Spaces

by Javier Thayer, Jonathan Herzog, and Joshua Guttman

(2)

### 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

(3)

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

### An Example

Needham-Schroeder-Lowe public key:

{Na A}KB

{Na Nb B}KA

{N }

(4)

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

### An Example

Needham-Schroeder-Lowe public key:

◦ {Na A}KB

{Na Nb B}KA

{N }

{Na A}KB

{Na Nb B}KA

{N }

(5)

### An Example

Needham-Schroeder-Lowe public key:

◦ {Na A}KB

{Na Nb B}KA

{N }

{Na A}KB

{Na Nb B}KA

{N }

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

(6)

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

### An Example

Needham-Schroeder-Lowe public key:

◦ {Na A}KB

{Na Nb B}KA

{N }

{Na A}KB

{Na Nb B}KA

{N }

(7)

### 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

| t1 t2 concatenation K and T are disjoined sets

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

(8)

s

t1

t2

t3

(9)

### Definitions

s

t1

t2

t3

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

−t2

+t3

(10)

### Definitions

s (s, 1)

(s, 2)

(s, 3)

t1

t2

t3

(s, 1) ∈ N

index((s, 1)) = 1 term((s, 1)) = +t1

uns_term((s, 1)) = t1

(11)

### Definitions

s n1

n3

n5

n2

n4

n6

s0 ⇒⊆ N × N

→⊆ N × N

⇒ ∪ → is the edge relation in a directed graph

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

(12)

### Bundles

Definition Let C be a set of edges and NC be corresponding nodes. This graph is a bundle if:

C is finite and acyclic

If n2 ∈ NC and term(n2) is negative, then there is a unique n1 such that n1 → n2 ∈ C

If n2 ∈ NC and n1 ⇒ n2 then n1 ⇒ n2 ∈ C

Summary: Bundles are causally well-founded strand spaces

(13)

### Well-founded Partial Order

n1

n3

n5

n2

n4

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).

(14)

### A Simple Proof

n1

n3

n5

n2

n4

n6

Lemma 2.7

Let C be a bundle. If n is a C-minimal element of NC then term(n) is positive.

(15)

### A Simple Proof

n1

n3

n5

n2

n4

n6

Lemma 2.7

Let C be a bundle. If n is a C-minimal element of NC then term(n) is positive.

Also holds for subsets, S, of NC whenever both n1 and n are in S for all

(16)

### Penetrator Strands

M

◦ T

for T ∈ T

F

◦ t

T

t t t

C

t1

t2 t1 t2

t1 t2

t1

t2

◦ K

for K ∈ KP

K t {t}K

K1 {t}K

t

(17)

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

(18)

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)

(19)

### 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 Σ

(20)

### NSL-spaces

Definition An NSL-space consists only of

Init[A, B, Na, Nb]-strands, Resp[A, B, Na, Nb]-strands, and penetrator strands.

◦ {Na A}KB

{Na Nb B}KA

{Na A}KB

{Na Nb B}KA

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

(21)

### 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]

(22)

### 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]

(23)

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, Na, Nb] in C 3. Na 6= Nb and Nb is uniquely originating in C

then there is a strand Init[A, B, Na, Nb] in C. Proof strategy

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

Show that Nb is manipulated by a regular strand Show that this strand is Init[A, B, Na, Nb]

(24)

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, Na, Nb] in C 2. KA1 6∈ KP

3. Na 6= Nb and Nb is uniquely originating in C then there is a strand Init[A, B, Na, Nb] in C.

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

Show that Nb is manipulated by a regular strand Show that this strand is Init[A, B, Na, Nb]

(25)

### Authentication

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

1. there is a strand Resp[A, B, Na, Nb] in C 2. KA1 6∈ KP

3. Na 6= Nb and Nb is uniquely originating in C then there is a strand Init[A, B, Na, Nb] in C.

Proof strategy

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

Show that N is manipulated by a regular strand

(26)

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

### Authentication of NSL

n0

n3

{Na A}KB

{Na Nb B}KA

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

(27)

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

### Authentication of NSL

n0

n3

{Na A}KB

{Na Nb B}KA

{Nb}KB

{n ∈ C | Nb @ term(n)

{Na Nb B}KA 6@ term(n)}

has a minimal element, n2, which is regular and positive

n2

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

(28)

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

### Authentication of NSL

n0

n3

{Na A}KB

{Na Nb B}KA

{Nb}KB n2

. . . Nb . . . n1 {Na Nb B}KA

Some node n1 precedes n2

and {Na Nb B}KA @ term(n1)

...

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

(29)

### Authentication of NSL

n0

n3

{Na A}KB

{Na Nb B}KA

{Nb}KB n2

. . . Nb . . . n1 {Na Nb B}KA

Can only be a regular initiator strand:

◦ {Na A}KA

(30)

### Summary of Authentication Proof

Proof strategy

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

Show that Nb is manipulated by a regular strand Show that this strand is Init[A, B, Na, Nb]

In retrospect

The difficult part was establishing that there was a regular strand

The rest was just reading off parameters

(31)

### 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.

(32)

◦ {Na A}KB

{Na Nb B}KA

{Nb}KB

{Na A}KB

{Na Nb B}KA

{Nb}KB

(33)

### 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, Na, Nb] in C 2. KA1 6∈ KP and KB1 6∈ KP; and

3. Na 6= Nb and Nb is uniquely originating in C

Then for all nodes m ∈ C such that Nb @ term(m),

either {Na Nb B}KA @ term(m) or {Nb}KB @ term(m). In particular, Nb 6= term(m).

(34)

### 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

Referencer

RELATEREDE DOKUMENTER

We have seen that these sets are power closed and root closed, where a subset of a ring is said to be root closed if whenever it contains a positive power of an element, it

As IOSS is strongly related to the estimation of internal variables of a system, they also intro- duce a more constraining notion called i-IOSS (“i” for “incre- mental”), which

A protocol specification written in AnB-API has six sections containing the protocol name, types, sets and facts used in the subprotocols section, the sub- protocols section

Brief run-through of the test protocol for FHIR HospitalNotification (receiving parties).. Test protocols - status.. Test protocol

The security of the Cinema System is provided by means of an authentication protocol presented in section 5.4.2 combined with use of cryptography for en- crypting user sensitive

As we have updated the protocol model with message reception and agent’s knowledge (see section 4.5), the theorems and their proofs are also adjusted. Similarly, each lemma

IEC 61850 is not just a protocol that can exchange a block of data from A to B – it is also an Information Model, which defines a unique naming convention for all the building

The thesis have given major contribution in embedded IoT security framework, AES-GCM based embedded security protocol, taxonomy of different IoT security