Transcript Document

Abstraction and Refinement in
Protocol Derivation
Anupam Datta
John C. Mitchell
Ante Derek
Dusko Pavlovic
Stanford University Kestrel Institute
CSFW June 28, 2004
Project Goals

Protocol derivation


Build security protocols by combining and
refining parts from basic protocols.
Proof of correctness

Prove protocols correct using logic that
follows steps of derivation.
Outline


Background

Derivation System

Compositional Logic
[CSFW01,CSFW03]
Abstraction and Refinement



[CSFW03]
Methods
Applications
Conclusions and Future Work
Example

Construct protocol with properties:




Shared secret
Authenticated
Identity Protection
Design requirements for IKE, JFK, IKEv2
(IPSec key exchange protocol)
Component 1
Diffie Hellman
A  B: ga
B  A: gb



Shared secret (with someone)
 A deduces:
Knows(Y, gab)  (Y = A) ۷ Knows(Y,b)
Authenticated
Identity Protection
Component 2
Challenge-Response
A  B: m, A
B  A: n, sigB {m, n, A}
A  B: sigA {m, n, B}



Shared secret
Authenticated
 A deduces: Received (B, msg1) Λ Sent (B,
msg2)
Identity Protection
m := ga
Composition
ISO-9798-3
A  B: ga, A
B  A: gb, sigB {ga, gb, A}
A  B: sigA {ga, gb, B}



Shared secret: gab
Authenticated
Identity Protection
n := gb
Refinement
Encrypt Signatures
A  B: ga, A
B  A: gb, EK {sigB {ga, gb, A}}
A  B: EK {sigA {ga, gb, B}}



Shared secret: gab
Authenticated
Identity Protection
Outline


Background

Derivation System

Compositional Logic
Abstraction and Refinement



Methods
Applications
Conclusions and Future Work
Challenge-Response: Proof Idea
m, A
n, sigB {m, n, A}
A
B
sigA {m, n, B}

Alice reasons: if Bob is honest, then:


only Bob can generate his signature. [protocol independent]
if Bob generates a signature of the form sigB {m, n, A},



he sends it as part of msg 2 of the protocol and
he must have received msg1 from Alice. [protocol specific]
Alice deduces:
Received (B, msg1) Λ Sent (B, msg2)
Formalism

Cord calculus


Protocol logic


Protocol programming language
Expressing protocol properties
Proof system

Proving protocol properties
Symbolic (“Dolev-Yao”) model
Challenge-Response as Cords
m, A
A
n, sigB {m, n, A}
B
sigA {m, n, B}
InitCR(A, X) = [
new m;
send A, X, m, A;
receive X, A, x, sigX{m, x, A};
send A, X, sigA{m, x, X};
]
RespCR(B) = [
receive Y, B, y, Y;
new n;
send B, Y, n, sigB{y, n, Y};
receive Y, B, sigY{y, n, B};
]
Correctness of CR
InitCR(A, X) = [
new m;
send A, X, {m, A};
receive X, A, {x, sigX{m, x, A}};
send A, X, sigA{m, x, X}};
]
RespCR(B) = [
receive Y, B, {y, Y};
new n;
send B, Y, {n, sigB{y, n, Y}};
receive Y, B, sigY{y, n, B}};
]
CR |- [ InitCR(A, B) ] A Honest(B)  ActionsInOrder(
Send(A, {A,B,m}),
Receive(B, {A,B,m}),
Send(B, {B,A,{n, sigB {m, n, A}}}),
Receive(A, {B,A,{n, sigB {m, n, A}}})
)
Proof System

Sample Axioms:

Reasoning about possession:



Has(A, {m}K)  Has(A, K)  Has(A, m)
Has(A, {m,n})  Has(A, m)  Has(A, n)
Reasoning about crypto primitives:


Honest(X)  Decrypt(Y, encX{m})  X=Y
Honest(X)  Verify(Y, sigX{m}) 
 m’ (Send(X, m’)  Contains(m’, sigX{m})


Protocol-specific Rule: Honesty/Invariance rule
Soundness Theorem:
Every provable formula is valid
Outline


Background

Derivation System

Compositional Logic
Abstraction and Refinement



Methods
Applications
Conclusions and Future Work
Protocol Templates



Protocols with function variables instead of
specific cryptographic operations
Idea: One template can be instantiated to
many protocols
Advantages:
 proof reuse
 design principles/patterns
Example
Challenge-Response Template
A  B: m
B  A: n, F(B,A,n,m)
A  B: G(A,B,n,m)
A  B: m
B  A: n,EKAB(n,m,B)
A  B: EKAB(n,m)
ISO-9798-2
A  B: m
B  A: n,HKAB(n,m,B)
A  B: HKAB(n,m,A)
SKID3
Instantiations
Abstraction
A  B: m
B  A: n, sigB(n,m,A)
A  B: sigA(n,m,B)
ISO-9798-3
Extending Formalism



Language Extensions: Add function variables
to term language for cords and logic (HOL)
Semantics: Q |= φ  σQ |= σφ, for all
substitutions σ eliminating all function
variables
Soundness Theorem: Every provable formula
is valid
Abstraction-Instantiation Method(1)

Characterizing protocol concepts



Step 1: Under hypotheses about function variables
and invariants, prove security property of template
Step 2: Instantiate function variables to
cryptographic operations and prove hypotheses.
Benefit:

Proof reuse
Example
Challenge-Response Template
A  B: m
B  A: n, F(B,A,n,m)
A  B: G(A,B,n,m)
•Step 1:
•Hypotheses: Function F(B,A,n,m) can be computed only by B
or A,…
•Property: Mutual authentication
•Step 2:
•Instantiate F() to signature, keyed hash, encryption (ISO9798-2,3, SKID3)
•Satisfies hypotheses => Guarantees mutual authentication
Proof Structure
Discharge hypothesis
axiom
hypothesis
Proof
reuse
Template
Instance
Abstraction-Instantiation Method(2)

Combining protocol templates
If protocol P is a hypotheses-respecting
instance of two different templates, then it
has the properties of both.

Benefits:


Modular proofs of properties
Formalization of protocol refinements
Refinement Example Revisited
Encrypt Signatures
A  B: ga, A
B  A: gb, EK {sigB {ga, gb, A}}
A  B: EK {sigA {ga, gb, B}}
Two templates:

Template 1: authentication + shared secret
(Preserves existing properties; proof reused)

Template 2: identity protection (encryption)
(Adds new property)
Authenticated key exchange
AKE1
A  B: ga, A
B  A: gb, F(B,A,gb,ga)
A  B: G(A,B,ga,gb)
ISO-9798-3, JFKi
AKE2
A  B: ga
B  A: gb, F(B,gb,ga), F’(B,gab)
A  B: G(A,ga, gb), G’(A,gab)
STS, JFKr, IKEv2, SIGMA
•Shared secret
•Shared secret
•Stronger authentication
•Weaker authentication
•Identity protection for B
•Identity protection for A
•Non-repudiation
•Repudiability
H. Krawczyk: The Cryptography of the IPSec and IKE Protocols [CRYPTO’03]
More examples…

Authenticated Key Exchange:


Key Computation:


Template for JFKr, STS, IKE, IKEv2
Template for Diffie-Hellman, UM, MTI/A,
MQV
Combining these templates
Synthesis: STS-MQV
DH
MTI/A
authenticate
STS
protect
identities
STSP
cookie
STSPH
symmetric
hash
RFK
MTIC
MTICP
MTICPH
MTIRFK
UM
UMC
UMCP
UMCPH
UMRFK
MQV
MQVC
MQVCP
MQVCPH
MQVRFK
key
conf.
Conclusions

Abstraction-Instantiation using protocol templates:



Logical foundation:


Single proof for similar protocols from common template
Multiple protocol properties from different templates
Add function variables to protocol language and logic
Applications:




CR template: ISO-9798-2,3, SKID3
Identity protection refinement in JFK
Design principles: IKEv2, JFKi, JFKr, ISO, STS, SIGMA, IKE
Synthesis: DH-MQV + STS-JFKr
Future Work

Done:



Derivation idea successfully applied to large set of
protocol examples
Rigorous treatment of composition, refinement in
protocol logic
Work In Progress:



Tool support for derivation system and logic
Formalization of protocol transformations
More applications