Mikael Buchholtz

Control Flow Analysis

of Security Protocols (II)

Mikael Buchholtz

02913 – F2004 – Mikael Buchholtz – p. 1

The Analysis

◦ ◦

◦

◦

◦

◦ ◦

◦

◦

· · ·

· · ·

· · ·

· · ·

· · ·

Executions

Analysis

The Analysis

Network messages: κ ∈ P (bVc ^∗ )

Variable bindings: ρ : bX c → P (bVc) Judgements

(ρ, κ) | = P

02913 – F2004 – Mikael Buchholtz – p. 3

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

Specifying the Judgements

hA, B i. 0 | (A; x). 0 (ρ, κ) | = hA, B i. 0 iff hbAc, bB ci ∈ κ

(ρ, κ) | = (A; x). 0 iff ∀V ¹ , V ² :

hV ¹ , V ² i ∈ κ ∧ V ¹ = bAc

⇒ V ² ∈ ρ(bxc)

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

Specifying the Judgements

(ρ, κ) | = hA, B i. 0 | (A; x). 0

(ρ, κ) | = hA, B i. 0 (ρ, κ) | = (A; x). 0

iff ∀V ¹ , V ² :

hV ¹ , V ² i ∈ κ ∧ V ¹ = bAc

⇒ V ² ∈ ρ(bxc)

02913 – F2004 – Mikael Buchholtz – p. 4

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

Specifying the Judgements

(ρ, κ) | = hA, B i. 0 | (A; x). 0

(ρ, κ) | = hA, B i. 0 iff hbAc, bB ci ∈ κ (ρ, κ) | = (A; x). 0

hV ¹ , V ² i ∈ κ ∧ V ¹ = bAc

⇒ V ² ∈ ρ(bxc)

Specifying the Judgements

(ρ, κ) | = hA, B i. 0 | (A; x). 0

(ρ, κ) | = hA, B i. 0 iff hbAc, bB ci ∈ κ (ρ, κ) | = (A; x). 0 iff ∀V ¹ , V ² :

hV ¹ , V ² i ∈ κ ∧ V ¹ = bAc

⇒ V ² ∈ ρ(bxc)

02913 – F2004 – Mikael Buchholtz – p. 4

Auxiliary Judgements for Terms

ρ | = E : ϑ

The term cache ϑ ∈ P (bVc) collects the possible

values that E may evaluate to.

Judgements for Terms

bnc ∈ ϑ ρ | = n : ϑ

ρ(bxc) ⊆ ϑ ρ | = x : ϑ

∧ ^k _{i =0} ρ | = E _i : ϑ _i ∧

∀V 0 , V 1 , · · · , V _k : ∧ ^k _{i =0} V _i ∈ ϑ _i ⇒ {V 1 , · · · , V _k } _V

∈ ϑ ρ | = {E 1 , · · · , E _k } _E

: ϑ

02913 – F2004 – Mikael Buchholtz – p. 6

Judgements for Communication

Output:

∧ ^k _{i =1} ρ | = E _i : ϑ _i ∧

∀V 1 , · · · , V _k : ∧ ^k _{i =1} V _i ∈ ϑ _i ⇒ hV 1 , · · · , V _k i ∈ κ ∧ (ρ, κ) | = P

(ρ, κ) | = hE 1 , · · · , E _k i. P

Input:

∧ ^j _{i =1} ρ | = E _i : ϑ _i ∧

∀hV 1 , · · · , V _k i ∈ κ : ∧ ^j _{i =1} V _i ^E ϑ _i ⇒ ∧ ^k _{i = j +1} V _i ∈ ρ(bx _i c) ∧ (ρ, κ) | = P

(ρ, κ) | = (E 1 , · · · , E _j ; x _j +1 , · · · , x _k ). P

Judgement for Decryption

ρ | = E : ϑ ∧ ∧ ^j _{i =0} ρ | = E _i : ϑ _i ∧

∀ {V 1 , · · · , V _k } _V

∈ ϑ : ∧ ^j _{i =0} V _i ^E ϑ _i ⇒

∧ ^k _{i = j +1} V _i ∈ ρ(bx _i c) ∧ (ρ, κ) | = P

(ρ, κ) | = decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P

02913 – F2004 – Mikael Buchholtz – p. 8

Remaining Judgements

(ρ, κ) | = 0

(ρ, κ) | = P ¹ ∧ (ρ, κ) | = P ² (ρ, κ) | = P ¹ |P ²

(ρ, κ) | = P (ρ, κ) | = (ν n)P

(ρ, κ) | = P

(ρ, κ) | =! P

Correctness

The analysis should describe all executions of a process.

This is captured by subject reduction Theorem

If (ρ, κ) | = P and P → Q then also (ρ, κ) | = Q

02913 – F2004 – Mikael Buchholtz – p. 10

Analysing a Protocol

1. Write the protocol in the process calculus L ^Y S ^A 2. Specify an attacker

3. Analyse the protocol and the attacker using control flow analysis

4. Inspect the analysis result to determine

(security) properties of the protocol.

Protocols and Attackers

Network

S M

A

B

legitimate part of the system the attacker

02913 – F2004 – Mikael Buchholtz – p. 12

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

Attackers [Dolev-Yao 1981]

An attacker can

1. Send messages

2. Receive messages (intercept messages)

3. Encrypt messages (composed from things he knows)

4. Decrypt messages (if he knows the key) 5. Generate new things

Active Attackers can only do it all

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

Attackers [Dolev-Yao 1981]

An attacker can

1. Send messages

2. Receive messages

3. Encrypt messages (composed from things he knows)

4. Decrypt messages (if he knows the key) 5. Generate new things

Passive attackers can only do 2. and 4.

Active Attackers can only do it all

02913 – F2004 – Mikael Buchholtz – p. 13

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

The Attacker Formula F _RM ^DY

(1) ∀hV 1 , · · · , V _k i ∈ κ : ∧ ^k _{i =1} V _i ∈ ρ(z ^• ) (2)

∧ _{k ∈A}

Enc

∀{V 1 , · · · , V _k } _V

∈ ρ(z • ) :

V 0 E ρ(z ^• ) ⇒ (∧ ^k _{i =1} V _i ∈ ρ(z ^• ) (3)

∧ _{k ∈A}

Enc

∀V 0 , · · · , V _k : ∧ ^k _{i =0} V _i ∈ ρ(z • ) ⇒

{V 1 , · · · , V _k } _V

∈ ρ(z ^• ) (4)

∧ _k ∈A

∀V 1 , · · · , V _k : ∧ ^k _{i =1} V _i ∈ ρ(z • ) ⇒ hV 1 , · · · , V _k i ∈ κ

(5) {n ^• }

∪bN ^f c

⊆ ρ(z ^• )

A ^κ arity of communications N ^f free names

A ⁺ _Enc arity of encryption/decryption

The Attacker Formula F _RM ^DY

(1) ∧ _k ^∈A

∀hV 1 , · · · , V _k i ∈ κ : ∧ ^k _{i =1} V _i ∈ ρ(z ^• ) (2) ∧ _{k ∈A}

Enc

∀{V 1 , · · · , V _k } _V

∈ ρ(z • ) :

V 0 E ρ(z ^• ) ⇒ (∧ ^k _{i =1} V _i ∈ ρ(z ^• ) (3) ∧ _{k ∈A}

Enc

∀V 0 , · · · , V _k : ∧ ^k _{i =0} V _i ∈ ρ(z • ) ⇒

{V 1 , · · · , V _k } _V

∈ ρ(z ^• )

(4) ∧ _k ∈A

∀V 1 , · · · , V _k : ∧ ^k _{i =1} V _i ∈ ρ(z • ) ⇒ hV 1 , · · · , V _k i ∈ κ (5) {n ^• } ∪ bN ^f c ⊆ ρ(z ^• )

A ^κ arity of communications N ^f free names A ⁺ _Enc arity of encryption/decryption

02913 – F2004 – Mikael Buchholtz – p. 14

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

The Analysis

Executions with the attacker

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

The Analysis

Executions with the attacker

Program Attacker

02913 – F2004 – Mikael Buchholtz – p. 15

The Analysis of the Attacker

Executions with the attacker

Program Attacker

x ¹ x ²

x ³

z ^•

The Analysis of the Attacker

Executions with the attacker

Program Attacker

02913 – F2004 – Mikael Buchholtz – p. 15

Correctness

The Dolev-Yao formula covers all attackers Q that may be placed in parallel with a protocol P i.e. as

P | Q

Let Q be identical to Q except that

bound names in Q have canonical name n _•

bound variables in Q have canonical variable z _•

Correctness

Theorem

If (ρ, κ, ψ ) satisfies F RM ^DY then (ρ, κ) | = Q for all attackers Q .

and also Theorem

There exists an attacker Q ^hard such that the formula (ρ, κ) | = Q ^hard is equivalent to the formula F RM ^DY .

02913 – F2004 – Mikael Buchholtz – p. 17

Security properties

confidentiality , integrity, availability, authentication ,

forward secrecy, freshness, anonymity, privacy, key

safety, non-repudiation,...

Security properties

confidentiality, integrity, availability, authentication, forward secrecy, freshness, anonymity, privacy, key safety, non-repudiation,...

02913 – F2004 – Mikael Buchholtz – p. 18

Confidentiality

Definition A protocol P preserves confidentiality of a value V if there does not exist an execution in

which the attacker learns V . The analysis

covers every execution

represents the attackers knowledge in ρ(z _• ) so, if bV c 6∈ ρ(z _• ) then V is kept confidential

(In the LySatool: the grammar starting with l _• rules.

This is printed at the top of the HTML output).

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

Authentication

The right principals should work together, or

Messages should only go to the right principals Idea: Focus on something that the attacker

cannot access freely: encrypted values

02913 – F2004 – Mikael Buchholtz – p. 20

Authentication

The right principals should work together, or

Messages should only go to the right principals ...but, the attacker can get hold of any message Idea: Focus on something that the attacker

cannot access freely: encrypted values

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

Destination and Origin

hA, B, Ai. (B, A; x).

(ν mess )hA, B, {| mess |} _x i. 0

|

(ν ± KB )(A, B, A; ). hB, A, KB ⁺ i.

(A, B ; y). decrypt y as {| ; ym |} _KB

b [ orig {a} ]

in 0 E ::= {E 1 , · · · , E _k } _E

| {|E 1 , · · · , E _k |} ^` _E

[ dest L] | . . .

P ::= decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P |

decrypt E as {|E 1 , · · · , E _j ; x _j +1 , · · · , x _k |} ^` _E

[ orig L] in P . . .

02913 – F2004 – Mikael Buchholtz – p. 21

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

Destination and Origin

hA, B, Ai. (B, A; x).

(ν mess )hA, B, {| mess |} ^a _x i. 0

|

(ν ± KB )(A, B, A; ). hB, A, KB ⁺ i.

(A, B ; y). decrypt y as {| ; ym |} ^b _KB

[ orig {a} ]

in 0 E ::= {E 1 , · · · , E _k } _E

| {|E 1 , · · · , E _k |} ^` _E

[ dest L] | . . .

P ::= decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P |

decrypt E as {|E 1 , · · · , E _j ; x _j +1 , · · · , x _k |} ^` _E

[ orig L] in P . . .

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

Destination and Origin

hA, B, Ai. (B, A; x).

(ν mess )hA, B, {| mess |} ^a _x [ dest {b} ]i. 0

|

(ν ± KB )(A, B, A; ). hB, A, KB ⁺ i.

(A, B ; y). decrypt y as {| ; ym |} ^b _KB

in 0 E ::= {E 1 , · · · , E _k } _E

| {|E 1 , · · · , E _k |} ^` _E

[ dest L] | . . .

P ::= decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P |

decrypt E as {|E 1 , · · · , E _j ; x _j +1 , · · · , x _k |} ^` _E

[ orig L] in P . . .

02913 – F2004 – Mikael Buchholtz – p. 21

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

Destination and Origin

hA, B, Ai. (B, A; x).

(ν mess )hA, B, {| mess |} ^a _x [ dest {b} ]i. 0

|

(ν ± KB )(A, B, A; ). hB, A, KB ⁺ i.

(A, B ; y). decrypt y as {| ; ym |} ^b _KB

[ orig {a} ] in 0 P ::= decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P |

decrypt E as {|E 1 , · · · , E _j ; x _j +1 , · · · , x _k |} ^` _E

[ orig L] in P . . .

Destination and Origin

hA, B, Ai. (B, A; x).

(ν mess )hA, B, {| mess |} ^a _x [ dest {b} ]i. 0

|

(ν ± KB )(A, B, A; ). hB, A, KB ⁺ i.

(A, B ; y). decrypt y as {| ; ym |} ^b _KB

[ orig {a} ] in 0

E ::= {E 1 , · · · , E _k } _E

| {|E 1 , · · · , E _k |} ^` _E

[ dest L] | . . . P ::= decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P |

decrypt E as {|E 1 , · · · , E _j ; x _j +1 , · · · , x _k |} ^` _E

[ orig L] in P . . .

02913 – F2004 – Mikael Buchholtz – p. 21

Reference Monitor Semantics

P → ^RM P ⁰ checks annotations where

values carry around the annotations bbE cc removes annotations, e.g.

bb{A, B } ^a _k [ dest {b}]cc = bb{A, B } ^c _k [ dest {d}]cc In the paper the standard semantics and the

reference monitor semantics are joined into one

parameterised semantics P → _R P ⁰

Reference Monitor Semantics

∧ ^j _{i =0} bbE _i cc = bbE _i ⁰ cc ∧ ` ∈ L <sup>0</sup> ∧ ` ⁰ ∈ L decrypt {E 1 , · · · , E _k } ^` _E

[ dest L]

as {E ₁ ⁰ , · · · , E _j ⁰ ; x _j +1 , · · · , x _k } ^` _E

0

[ orig L ⁰ ] in P

→ ^RM P [E _j +1 /x _j +1 , · · · , E _k /x _k ]

The reference monitor semantics aborts the execution of P whenever

P → ^∗ Q → Q ⁰ P → ^∗ RM Q6→ RM

02913 – F2004 – Mikael Buchholtz – p. 23

Reference Monitor Analysis

ρ, κ | = ^RM P : ψ

collects potential breaches of annotations in ψ . (a, b) ∈ ψ

reads

Something encrypted at a was unintentionally

decrypted at b

Reference Monitor Analysis

ρ | = E : ϑ ∧ ∧ ^j _{i =0} ρ | = E _i : ϑ _i ∧

∀ {V 1 , · · · , V _k } ^` _V

[ dest L] ∈ ϑ : ∧ ^j _{i =0} V _i ^E ϑ _i ⇒

∧ ^k _{i = j +1} V _i ∈ ρ(bx _i c) ∧

` <sup>0</sup> 6∈ L ∨ ` 6∈ L ⁰ ⇒ (`, ` ⁰ ) ∈ ψ ∧ (ρ, κ) | = P : ψ

(ρ, κ) | = decrypt E as {E 1 , · · · , E _j ; x _j +1 , · · · , x _k } _E

in P : ψ

02913 – F2004 – Mikael Buchholtz – p. 25

Correctness of Reference Monitor Analysis

The analysis should track the reference monitor This is captured by

Theorem

If (ρ, κ) | = P : ψ then the reference monitor cannot abort the execution of P .

That is, ψ = ∅ means that we are happy

Main Theorem (of the paper)

Definition

P guarantees dynamic authentication if P | Q cannot abort regardless of the choice of the attacker Q .

Definition

P guarantees static authentication if (ρ, κ) | = P : ψ and (ρ, κ, ∅) satisfies the formula F RM ^DY .

Theorem

If P guarantees static authentication then P guarantees dynamic authentication.

02913 – F2004 – Mikael Buchholtz – p. 27

Analysing a Protocol

1. Write the protocol in the process calculus L ^Y S ^A (which has a formal semantics P → P ⁰ )

2. Specify an attacker

3. Analyse the protocol and the attacker using control flow analysis ( (ρ, κ) | = P : ψ )

4. Inspect the analysis result to determine security

properties of the protocol.

Assignment 1

Assignment 1 is on the web-page

Its about analysing protocols using the LySatool.

Due Thursday 10, March

Hand-in short reports in groups of no more than two people.

02913 – F2004 – Mikael Buchholtz – p. 29