Transcript ppt - Stanford Computer Security Laboratory

CS 259
Protocol Composition Logic
(PCL): Part II
Anupam Datta
Using PCL: Summary
Modeling the protocol
• Program for each protocol role
Modeling security properties
• Using PCL syntax
• Authentication, secrecy easily expressed
Proving security properties
• Using PCL proof system
• Soundness theorem guarantees that provable
properties hold in all protocol runs
Example: C. He, M. Sundararajan, A. Datta, A. Derek, J. C. Mitchell,
modular correctness proof of TLS and IEEE 802.11i, ACM CCS 2005
A
Challenge-Response programs (1)
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}};
]<
>
Challenge-Response Property (2)
Specifying authentication for Initiator
CR | true [ InitCR(A, B) ] A Honest(B) 
(
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}}})
)
Challenge-Response Proof (3)
Protocol Composition Logic: PCL
Intuition
Formalism
• Protocol programming language
• Protocol logic
– Syntax
– Semantics
• Proof System
Example
• Signature-based challenge-response
Composition
Computational Soundness
Modular Analysis / Composition
Laptop
Access
Point
Auth
Server
EAP-TLS: Certificates to Authorization (PMK)
4WAY Handshake:
PMK to Keys for data communication
Group key:
Keys for broadcast communication
Data protection:
AES based using above keys
(Shared Secret-PMK)
802.11i Key Management
20 msgs in 4 components
Goal: Divide and Conquer
Desiderata
Non-destructive combination
• Security guarantee for TLS in isolation must be
preserved when run simultaneously with 4WAY
• Formalized as parallel composition
 Additive combination
• Prove 4WAY security guarantee assuming TLS
provides shared secret. Combine with separate
proof of TLS guarantee.
• Formalized as sequential composition
Parallel Composition
Definition:
Q = Q1 | Q2 if the set of roles of Q is the
union of the set of roles of Q1 and Q2
Examples:
• On the internet many protocols run in
parallel, e.g., SSL, IKE, Kerberos
• In 802.11i, TLS, 4WAY, GroupKey can be
run in parallel
Compositional Proofs: Intuition
Protocol specific reasoning
• “if honest Bob generates a signature of the form
sigB {m, n, A},
– he sends it as part of msg2 of the protocol and
– he must have received msg1 from Alice”
• Could break: Bob’s signature from one protocol could be
used to attack another
• PCL proof system: Honesty rule
Protocol independent reasoning
• Has(A, {m,n})  Has(A, m)  Has(A, n)
• Still good: unaffected by composition
• All other axioms and proof rules for PCL
Proof Tree
Proof step might fail
Axiom
Security
property
HON rule
Other rules
Parallel Composition Theorem (1)
Honesty rule:
roles R of Q.  protocol steps A of R.
Start(X) [ ]X 
 [ A ]X 
Q |- Honest(X)  
Lemma:
Let Q = Q1 | Q2. If Q1 |-  and Q2 |- , then Q |- 
• Proof idea:
– Roles (Q) = Roles (Q1)  Roles(Q2)
Parallel Composition Theorem (2)
Theorem:
Let Q = Q1 | Q2. If Q1 |- , |- and
Q2 |-  , then Q |- , where  includes all
invariants proved using Honesty rule
• Proof idea:
– By Lemma, Q |- 
– Also, |-
– Intuitively, the old proof tree for Q1 still
works
Proof Tree
Q
|- 
Q1 |-
|-
Additional
work to prove
Bulk of
proof
reused

Q2 |- 
Axiom
Security
property

HON rule
Other rules
Example: Challenge-Response
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}};
]
Invariant proved with Honesty rule
CR |- Honest(X) 
Send(X, m’)  Contains(m’, sigx {y, x, Y})   New(X, y) 
m= X, Y, {x, sigB{y, x, Y}}  Receive(X, {Y, X, {y, Y}})
Authentication property of CR is preserved
under parallel composition with any Q which
satisfies this invariant
Parallel Composition: Big Picture
Safe Environment for Q
Q1
Q2
Q3 … Qn
Protocol Q
• Q |- Inv(Q)
• Inv(Q) |- 
• Qi |- Inv(Q)
• No explicit reasoning
about attacker
Desiderata
Non-destructive combination
• Security guarantee for TLS in isolation must be
preserved when run simultaneously with 4WAY
• Formalized as parallel composition
 Additive combination
• Prove 4WAY security guarantee assuming TLS
provides shared secret. Combine with separate
proof of TLS guarantee.
• Formalized as sequential composition
Example: ISO-9798-3
ga, A
A
gb, sigB {ga, gb, A}
B
sigA {ga, gb, B}
Authentication
• Similar to challenge-response
• Do we need to prove property from scratch?
Shared secret: gab
Sequential Composition
DH-Init
X, Y
new x
X, Y, gx
CR-Init
W, Z, w
ISO-Init
X, Y
new x;
send X, Y, gx, A;
receive Y, X, z, sigY{gx, z, X};
send X, Y, sigX{gx, z, Y};
send W, Z, w, A;
receive Z, W, z, sigY{w, z, W};
send W, Z, sigX{w, z, Z};
Sequential composition of
roles with term substitution
Diffie-Hellman: Property
Formula
true [ new a ] A Fresh(A, ga)
Abstract challenge response
InitACR(A, X, m) = [
send A, X, {m};
receive X, A, {x, sigX{m, x}};
send A, X, sigA{m, x}};
]
RespACR(B, n) = [
receive Y, B, {y};
send B, Y, {n, sigB{y, n}};
receive Y, B, sigY{y, n}};
]
 Free variables m and n instead of nonces
 Modal form:  [ actions ] 
•
•
•
precondition:
actions:
postcondition:
Fresh(A,m)
[ InitACR ]A
Honest(B)  Authentication
Same proof as previous lecture!
Sequencing Rule
[S]P
 [ T ] P
 [ ST ] P 
Is this rule sound?
Composition:
DH+CR = ISO-9798-3
• Additive Combination
DH post-condition matches CR precondition
Sequential Composition:
• Substitute ga for m in CR to obtain ISO.
• Apply composition rule
• ISO initiator role inherits CR authentication.
DH secrecy is also preserved
• Proved using another application of composition
rule.
• Nondestructive Combination
• DH and CR satisfy each other’s invariants
Sequential Composition: Picture

DH |- Honest(X)  …
’
CR |- Honest(X)  …
 |-  [ DH-Init ] P 
’ |-  [ CR-Init ] P 
’ |-  [ DH-Init ] P 
’ |-  [ CR-Init ] P 
DH|- ’
CR |- ’
’ |-  [DH-Init; CR-Init] P 
Additive
ISO = DH;CR |- ’
Non-destructive
ISO |-  [ISO-Init] P 
Protocol Composition Logic: PCL
Intuition
Formalism
• Protocol programming language
• Protocol logic
– Syntax
– Semantics
• Proof System
Example
• Signature-based challenge-response
Composition
Computational Soundness
Computational PCL
Symbolic proofs about complexitytheoretic model of cryptographic
protocols
Two worlds
Symbolic model
[NS78,DY84,…]
Complexity-theoretic
model [GM84,…]
Attacker actions
-Fixed set of actions,
e.g., decryption with
known key
(ABSTRACTION)
+ Any probabilistic
poly-time computation
Security properties
-Idealized, e.g., secret
message = not
possessing atomic term
representing message
(ABSTRACTION)
+ Fine-grained, e.g.,
secret message = no
partial information
about bitstring
representation
Analysis methods
+ Successful array of
tools and techniques;
automation
- Hand-proofs are
difficult, error-prone;
no automation
Can we get the best of both worlds?
Our Approach
Protocol Composition Logic
(PCL)
Computational PCL
•Syntax
•Syntax ± 
•Proof System
•Proof System ± 
Symbolic “Dolev-Yao” model
Complexity-theoretic model
•Semantics
•Semantics
Talk so far…
Leverage PCL success…
Main Result
Computational PCL
• Symbolic logic for proving security properties
of network protocols using public-key encryption
Soundness Theorem:
• If a property is provable in CPCL, then property
holds in computational model with overwhelming
asymptotic probability.
Benefits
• Symbolic proofs about computational model
• Computational reasoning in soundness proof
(only!)
• Different axioms rely on different crypto
assumptions
ISO-9798-3 Key Exchange
ga, A
A
gb, sigB {ga, gb, A}
B
sigA {ga, gb, B}
Shared secret to be used as key:
Roughly: A, B have gab and for everyone else it is
indistinguishable from a random key gr
Central axioms
Cryptographic security property of
signature scheme
• Unforgeability (used for authentication)
Cryptographic security property of
Diffie-Hellman function
• DDH (used to prove secrecy)
CMA-Secure Signatures
mi
Sig(Y,mi)
Challenger
Sig(Y,m)
Attacker
Attacker wins
if m  mi
Attacker - any probabilistic polynomial time program;
wins if above probability is non-negligible
Decisional Diffie-Hellman
Let a, b, c be chosen at random from a group G with
generator g. Then the two distributions <ga,gb,gab>
and <ga,gb,gc> are computationally indistinguishable
(no polynomial time attacker can tell them apart)
Complete Proof
PCL  Computational PCL
Syntax, proof rules mostly the same
• But not sure about propositional connectives…
Significant difference
• Symbolic “knowledge”
– Has(X,t) : X can produce t from msgs that have been
observed, by symbolic algorithm
• Computational “knowledge”
– Possess(X,t) : can produce t by ppt algorithm
– Indistinguishable(X,t) : can distinguish from
random in ppt
• More subtle system: some axioms rely on CCA2,
some are info-theoretically true, etc.
Complexity-theoretic semantics
Q |=  if  adversary A  distinguisher D
 negligible function f
 n0 n > n0 s.t.
Fraction represents probability
[[]](T,D,f(n))|/|T| > 1 – f(n)
T(Q,A,n)
•
•
•
•
Fix protocol Q, PPT adversary A
Choose value of security parameter n
Vary random bits used by all programs
Obtain set T=T(Q,A,n) of equi-probable traces
[[]](T,D,f)
Inductive Semantics
 [[1 
2]] (T,D,) = [[1]] (T,D,)  [[2]] (T,D,)
 [[1  2]] (T,D,) = [[1]] (T,D,)  [[2]] (T,D,)
 [[ ]] (T,D,) = T - [[]] (T,D,)
Implication uses conditional probability
 [[1 
2]] (T,D,) = [[1]] (T,D,)
 [[2]] (T’,D,)
where T’ = [[1]] (T,D,)
Formula defines transformation on probability distributions over traces
Soundness of proof system
Example axiom
• Source(Y,u,{m}X)  Decrypts(X, {m}X) 
Honest(X,Y)  (Z  X,Y)  Indistinguishable(Z, u)
Proof idea: crypto-style reduction
• Assume axiom not valid:
 A  D  negligible f  n0  n > n0 s.t.
•
[[]](T,D,f)|/|T| < 1 –f(n)
• Construct attacker A’ that uses A, D to break
IND-CCA2 secure encryption scheme
• Conditional implication essential
Logic and Cryptography: Big Picture
Protocol security proofs using proof system
Axiom in proof system
Semantics and soundness theorem
Complexity-theoretic crypto definitions
(e.g., IND-CCA2 secure encryption)
Crypto constructions satisfying definitions
(e.g., Cramer-Shoup encryption scheme)
Summary: PCL
 Formalism
• Protocol programming language
• Protocol logic
– Syntax – stating security properties
– Semantics – meaning of security properties
• Proof System
– proving security properties
 Examples
• Signature-based challenge-response, ISO, 802.11i
 Composition
• Modular proofs
 Computational Soundness
• Symbolic proofs about complexity-theoretic model
Thanks
Questions?