Needham-Schroeder ’78 Dolev-Yao ’81

(1)

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

Control Flow Analysis

of Security Protocols (I)

Mikael Buchholtz

(2)

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view

of cryptography

(3)

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

(4)

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

(5)

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

Woo-Lam ’93

Lowe ’95

Language-based

Model checking of CSP

. . . LySa

(6)

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

Woo-Lam ’93

Lowe ’95

Language-based

Model checking of CSP

. . . LySa

Thayer-Herzog- Guttman ’98, ...

Strand Spaces

(7)

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

Woo-Lam ’93

Lowe ’95

Language-based

Model checking of CSP

. . . LySa

Thayer-Herzog- Guttman ’98, ...

Strand Spaces Probabalistic/complexity

theoretic view

of cryptography Herzog ’03,

Zunino-Degano ’04

(8)

Analysing a Protocol

[Bodei-Buchholtz-Degano-Nielson-Nielson ’04]

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.

(9)

L Y S A for Symmetric Cryptography

E ::= n name ( n ∈ N )

x variable (x ∈ X )

{E ¹ , · · · , E k } E

0

encryption P ::= hE 1 , · · · , E k i. P output

(E 1 , · · · , E j ; x j +1 , · · · , x k ). P input (with matching)

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

₀

ⁱⁿ P

decryption (with matching)

P 1 | P 2 parallel composition

(ν n)P introduce new name n

! P replication

(10)

The Wide-mouthed-frog Protocol

(without timestamps) [Burrows-Abadi-Needham ’89]

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

A

S ^Network

K _A

K

(11)

The Wide-mouthed-frog Protocol

(without timestamps) [Burrows-Abadi-Needham ’89]

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

A

S ^Network

A, {B, K _AB } _K A

(12)

The Wide-mouthed-frog Protocol

(without timestamps) [Burrows-Abadi-Needham ’89]

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

A

S ^Network

{A, K _AB } _K B

(13)

The Wide-mouthed-frog Protocol

(without timestamps) [Burrows-Abadi-Needham ’89]

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

A

S ^Network { mess } _K AB

(14)

Semantics

L ^Y S ^A has a reduction semantics defined by two relations

P → P ⁰ the reduction relation

P ≡ P ⁰ the structural congruence

(P → _R P ⁰ parameterised reduction relation used in

the paper )

(15)

Reduction Relation P → P ⁰

◦ ◦

◦

◦ ◦

◦

· · ·

Executions with the attacker

(16)

Reduction Relation P → P ⁰

◦ ◦

◦

◦ ◦

◦

· · ·

Executions

Executions with the attacker

(17)

Reduction Relation

P → P ⁰

(ν n)P → (ν n)P ⁰

∧ ^j _i ₌₁ E _i = E _i ⁰

hE ¹ , · · · , E k i. P | (E ₁ ⁰ , · · · , E _j ⁰ ; x j +1 , · · · , x k ). Q →

P | Q[E j +1 /x j +1 , · · · , E k /x k ]

P → P ⁰

P | Q → P ⁰ | Q

(18)

Structural Congruence

The structural congruence, P ≡ Q , brings processes

“on the right form” for the reduction relation

P ≡ Q ∧ Q → Q ⁰ ∧ Q ⁰ ≡ P ⁰

P → P ⁰

(19)

Structural Congruence

P ≡ P

P 1 ≡ P 2 ⇒ P 2 ≡ P 1

P 1 ≡ P 2 ∧ P 2 ≡ P 3 ⇒ P 1 ≡ P 3

P ¹ ≡ P ² ⇒ hE ¹ , · · · , E k i. P ¹ ≡ hE ¹ , · · · , E k i. P ² P 1 ≡ P 2 ⇒ (E 1 , · · · , E j ; x j +1 , · · · , x k ). P 1 ≡

(E 1 , · · · , E j ; x j +1 , · · · , x k ). P 2

P 1 ≡ P 2 ∧ P 3 ≡ P 4 ⇒ P 1 | P 3 ≡ P 2 | P 4

P 1 ≡ P 2 ⇒ (ν n)P 1 ≡ (ν n)P 2

P ¹ ≡ P ² ⇒ !P ¹ ≡ !P ²

P ≡ P ⇒ E {E , · · · , E ; x , · · · , x } P ≡

(20)

Structural Congruence

P 1 ≡ P 2 if P 1 and P 2 are disciplined α -equivalent

P 1 | P 2 ≡ P 2 | P 1

(P 1 | P 2 ) | P 3 ≡ P 1 | (P 2 | P 3 ) P | 0 ≡ P

(ν n) 0 ≡ 0

(ν n)(ν n ⁰ )P ≡ (ν n ⁰ )(ν n)P

(ν n)(P 1 | P 2 ) ≡ P 1 | (ν n)P 2 if n 6∈ fn(P 1 )

!P ≡ P | !P

(21)

The Semantics at Work

((ν n)hni. 0 ) | (; x). hn, xi. 0

(22)

The Semantics at Work

((ν n)hni. 0 ) | (; x). hn, xi. 0

≡ ((ν m)hmi. 0 ) | (; x). hn, xi. 0

≡ (ν m)(hmi. 0 | (; x). hn, xi. 0 )

(23)

The Semantics at Work

((ν n)hni. 0 ) | (; x). hn, xi. 0

≡ ((ν m)hmi. 0 ) | (; x). hn, xi. 0

≡ (ν m)(hmi. 0 | (; x). hn, xi. 0 )

→ (ν m)( 0 | hn, mi. 0 )

(24)

The Semantics at Work

((ν n)hni. 0 ) | (; x). hn, xi. 0

≡ ((ν m)hmi. 0 ) | (; x). hn, xi. 0

≡ (ν m)(hmi. 0 | (; x). hn, xi. 0 )

→ (ν m)( 0 | hn, mi. 0 )

≡ 0 | (ν m)hn, mi. 0

≡ (ν m)hn, mi. 0

(25)

Algebraic View of Cryptography

[Dolev-Yao ’81]

For example, to model

encrypt as E _K (P ) and decrypt as D _K (C ) such

that D _K (E _K (m)) = m and nothing else

(26)

Symmetric Cryptography in L Y S A

Encryption:

{E ¹ , · · · , E _k } _E 0

Decryption:

decrypt E as {E ¹ , · · · , E _j ; x _j ⁺¹ , · · · , x _k } _E ₀ in P Semantics models perfect cryptography:

∧ ^j _i ₌₀ E _i = E _i ⁰

decrypt {E ¹ , · · · , E k } E

0

as {E ₁ ⁰ , · · · , E _j ⁰ ; x j +1 , · · · , x k } _E

0

in P

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

(27)

Asymmetric Cryptography in L Y S A

Keys:

(ν _± m)P introduces two keys m ⁺ , m ⁻ in P

Encryption:

{|E ¹ , · · · , E _k |} _E 0

Decryption:

decrypt E as {|E ¹ , · · · , E _j ; x _j ⁺¹ , · · · , x _k |} _E ₀ in P

(28)

Asymmetric Cryptography in L Y S A

Decryption with private key:

∧ ^j _i ₌₁ E i = E _i ⁰

decrypt {|E ¹ , · · · , E _k |} m

⁺

as {|E ₁ ⁰ , · · · , E _j ⁰ ; x _j +1 , · · · , x _k |} _m

−

in P

→ P [E j +1 /x j +1 , · · · , E k /x k ] Signature validation public key:

∧ ^j _i ₌₁ E i = E _i ⁰

decrypt {|E 1 , · · · , E _k |} _m

⁻

as {|E ₁ ⁰ , · · · , E _j ⁰ ; x _j +1 , · · · , x _k |} _m

⁺

in P

→ P [E j +1 /x j +1 , · · · , E k /x k ]

(29)

Asymmetric Cryptography in L Y S A

E ::= . . . . . .

m ⁺ , m ⁻ public and private keys {|E ¹ , · · · , E k |} _E

₀

asymmetric encryption

P ::= . . . . . .

(ν ^± m)P key pair creation

decrypt E as {|E ¹ , · · · , E j ; x j +1 , · · · , x k |} _E

₀

in

asymmetric decryption

(30)

The Analysis

◦ ◦

◦

◦ ◦

◦

· · ·

Executions

(31)

The Analysis

◦ ◦

◦

◦ ◦

◦

· · ·

Executions

Analysis

(32)

The Analysis

◦ ◦

◦

◦ ◦

◦

· · ·

Executions

Analysis

(33)

Analysis Components

Network messages: Variable bindings:

κ ∈ P (V ^∗ ) ρ : X → P (V )

where values from V are variable-free terms i.e.

V ::= n | {V ¹ , · · · , V _k } _V 0 | {|V ¹ , · · · , V _k |} _V 0

Example

hA, B, { mess } _K i. 0 | (A, B ; x). 0

hA, B, { } i ∈ κ

(34)

Analysis Judgements

ρ, κ | = P

reads: “ ρ and κ are valid analysis estimates for P ”

Example

P ¹ ^def = hAi. 0 | (; x). 0 P ² ^def = hA, B i. 0 | (B ; x). 0 κ _a = {hA, B i}

ρ _a = [x 7→ ∅]

κ _b = {hAi}

ρ _b = [x 7→ {A}]

κ _c = {hAi, hB i}

ρ _c = [x 7→ {A, B }]

(35)

Analysing Restriction

!(ν n)hni. 0

≡ (ν m)hmi. 0 | (ν o)hoi. 0 | (ν p)hpi. 0 | (ν q )hq i. 0 | (ν r)hri. 0 | . . . |

!(ν n)hni. 0

Each name, n , is assigned a canonical name bnc The semantics uses disciplined α -equivalence:

(ν n)P is α -equivalent to (ν n ⁰ )P ⁰ and bnc = bn ⁰ c

For example

bmc = boc = bpc = bq c = brc = . . . = bnc

(36)

Analysing Restriction

!(ν n)hni. 0 ≡ (ν m)hmi. 0 | (ν o)hoi. 0 | (ν p)hpi. 0 | (ν q )hq i. 0 | (ν r )hri. 0 | . . . |

!(ν n)hni. 0 Each name, n , is assigned a canonical name bnc

The semantics uses disciplined α -equivalence:

(ν n)P is α -equivalent to (ν n ⁰ )P ⁰ and bnc = bn ⁰ c

For example

bmc = boc = bpc = bq c = brc = . . . = bnc

(37)

Analysing Restriction

!(ν n)hni. 0 ≡ (ν m)hmi. 0 | (ν o)hoi. 0 | (ν p)hpi. 0 | (ν q )hq i. 0 | (ν r )hri. 0 | . . . |

!(ν n)hni. 0

Each name, n , is assigned a canonical name bnc The semantics uses disciplined α -equivalence:

(ν n)P is α -equivalent to (ν n ⁰ )P ⁰ and bnc = bn ⁰ c

For example

(38)

Canonical Names and Variables

Network messages: Variable bindings:

κ ∈ P (bVc ^∗ ) ρ : bX c → P (bVc)

Example

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 )

≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 1 )hn 1 , n 1 i. 0 | (; x 1 , y 1 ). 0 → (!(ν n)hn, ni. 0 ) | (!(; x, y). 0 )≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 2 )hn 2 , n 2 i. 0 | (; x 2 , y 2 ). 0 → . . .

but bnc = bn 1 c = bn 2 c = . . .

(39)

Canonical Names and Variables

Network messages: Variable bindings:

κ ∈ P (bVc ^∗ ) ρ : bX c → P (bVc)

Example

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) ≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 1 )hn 1 , n 1 i. 0 | (; x 1 , y 1 ). 0

→ (!(ν n)hn, ni. 0 ) | (!(; x, y). 0 )≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 2 )hn 2 , n 2 i. 0 | (; x 2 , y 2 ). 0 → . . .

but bnc = bn 1 c = bn 2 c = . . .

(40)

Canonical Names and Variables

Network messages: Variable bindings:

κ ∈ P (bVc ^∗ ) ρ : bX c → P (bVc)

Example

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) ≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 1 )hn 1 , n 1 i. 0 | (; x 1 , y 1 ). 0 → (!(ν n)hn, ni. 0 ) | (!(; x, y). 0 )

≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 2 )hn 2 , n 2 i. 0 | (; x 2 , y 2 ). 0 → . . .

but bnc = bn 1 c = bn 2 c = . . .

(41)

Canonical Names and Variables

Network messages: Variable bindings:

κ ∈ P (bVc ^∗ ) ρ : bX c → P (bVc)

Example

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) ≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 1 )hn 1 , n 1 i. 0 | (; x 1 , y 1 ). 0 → (!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) ≡

(!(ν n)hn, ni. 0 ) | (!(; x, y). 0 ) | (ν n 2 )hn 2 , n 2 i. 0 | (; x 2 , y 2 ). 0 →

Needham-Schroeder ’78 Dolev-Yao ’81

Control Flow Analysis

of Security Protocols (I)

Mikael Buchholtz

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view

of cryptography

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

Woo-Lam ’93

Lowe ’95

Language-based

Model checking of CSP

. . . LySa

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

Woo-Lam ’93

Lowe ’95

Language-based

Model checking of CSP

. . . LySa

Thayer-Herzog- Guttman ’98, ...

Strand Spaces

History of Protocol Analysis

Needham-Schroeder ’78 Dolev-Yao ’81

Algebraic view of cryptography

Millen ’84, Meadows ’89, ...

State/transition model

Burrows-Abadi-Needham ’89, ...

Modal logics

Woo-Lam ’93

Lowe ’95

Language-based

Model checking of CSP

. . . LySa

Thayer-Herzog- Guttman ’98, ...

Strand Spaces Probabalistic/complexity

theoretic view

of cryptography Herzog ’03,

Zunino-Degano ’04

Analysing a Protocol

[Bodei-Buchholtz-Degano-Nielson-Nielson ’04]

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.

L Y S A for Symmetric Cryptography

E ::= n name ( n ∈ N )

x variable (x ∈ X )

{E 1 , · · · , E k } E

encryption P ::= hE 1 , · · · , E k i. P output

(E 1 , · · · , E j ; x j +1 , · · · , x k ). P input (with matching)

decrypt E as {E 1 , · · · , E j ; x j +1 , · · · , x k } E

in P

decryption (with matching)

P 1 | P 2 parallel composition

{E ¹ , · · · , E k } E

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

ⁱⁿ P

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

S ^Network

K _A

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

S ^Network

A, {B, K _AB } _K A

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

S ^Network

{A, K _AB } _K B

1. A → S : A, {B, K _AB } _K A

2. S → B : {A, K _AB } _K B

3. A → B : { mess } _K AB

S ^Network { mess } _K AB

L ^Y S ^A has a reduction semantics defined by two relations

P → P ⁰ the reduction relation

P ≡ P ⁰ the structural congruence

(P → _R P ⁰ parameterised reduction relation used in

Reduction Relation P → P ⁰

Reduction Relation P → P ⁰