Transcript Adventures in Computer Security

Security Analysis of Network Protocols:
Logical and Computational Methods
John Mitchell
Stanford University
ICALP and PPDP, 2005
Outline
Protocols
• Some examples, some intuition
Symbolic analysis of protocol security
• Models, results, tools
Computational analysis
• Communicating Turing machines, composability
Combining symbolic, computational analysis
• Some alternate approaches
• Protocol Composition Logic (PCL)
• Symbolic and computational semantics
Many Protocols
Authentication
• Kerberos
Key Exchange
• SSL/TLS handshake, IKE, JFK, IKEv2,
Wireless and mobile computing
• Mobile IP, WEP, 802.11i
Electronic commerce
• Contract signing, SET, electronic cash, …
Mobile IPv6 Architecture
Mobile Node (MN)
IPv6
Direct connection via
binding update
Corresponding Node (CN)
Home Agent (HA)
 Authentication is a
requirement
 Early proposals weak
802.11i Wireless Authentication
Supplicant
UnAuth/UnAssoc
Auth/Assoc
802.1X UnBlocked
Blocked
No Key
PTK/GTK
802.11 Association
EAP/802.1X/RADIUS Authentication
MSK
4-Way Handshake
Group Key Handshake
Data Communication
IKE subprotocol from IPSEC
m1
A, (ga mod p)
A
B, (gb mod p), signB(m1,m2)
m2
signA(m1,m2)
Result: A and B share secret gab mod p
Analysis involves probability, modular exponentiation,
complexity, digital signatures, communication networks
B
Needham-Schroeder Protocol
{ A, NonceA }
A
Kb
{ NonceA, NonceB } K
{ NonceB} Kb
a
B
Result: A and B share two private numbers
not known to any observer without Ka-1, Kb-1
Anomaly in Needham-Schroeder
[Lowe]
{ A, Na } Ke
A
E
{ Na, Nb } Ka
{ Nb } Ke
Evil agent E tricks
honest A into revealing
private key Nb from B.
Evil E can then fool B.
{ Na, Nb }
{ A, Na }
Ka
B
Kb
Run of a protocol
Initiate
A
Respond
B
Attacker
C
D
Correct if no security violation in any run
Protocol analysis methods
Cryptographic reductions
• Bellare-Rogaway, Shoup, many others
• UC [Canetti et al], Simulatability [BPW]
• Prob poly-time process calculus [LMRST…]
Symbolic methods
• Model checking
– FDR [Lowe, Roscoe, …], Murphi [M, Shmatikov, …],
• Symbolic search
– NRL protocol analyzer [Meadows]
• Theorem proving
– Isabelle [Paulson …], Specialized logics [BAN, …]
See papers in PPDP, ICALP proceedings for references
“The” Symbolic Model
Messages are algebraic expressions
• Nonce, Encrypt(K,M), Sign(K,M), …
Adversary
• Nondeterministic
• Observe, store, direct all communication
– Break messages into parts
– Encrypt, decrypt, sign only if it has the key
• Example: K1, Encrypt(K1, “hi”) 
 K1, Encrypt(K1, “hi”)  “hi”
– Send messages derivable from stored parts
Many formulations
 Word problems [Dolev-Yao, Dolev-Even-Karp, …]
• Each protocol step is symbolic function from input message to
output message; cancellation law dkekx = x
 Rewrite systems [CDLMS]
• Each protocol step is symbolic function from state and input
message to state and output message
 Logic programming [Meadows NRL Analyzer]
• Each protocol step can be defined by logical clauses
• Resolution used to perform reachability search
 Constraint solving [Amadio-Lugiez, … ]
• Write set constraints defining messages known at step i
 Strand space model [MITRE]
• Partial order (Lamport causality), reasoning methods
 Process calculus [CSP, Spi-calculus, applied , …)
• Each protocol step is process that reads, writes on channel
• Spi-calculus: use  for new values, private channels, simulate crypto
Complexity results
(see [Cortier et al])
Bounded # of
sessions
Unbounded number of sessions
Without nonces
With nonces
Co-NP complete
General:
undecidable
General:
undecidable
Bounded msg length: Bounded msg length:
DEXP-time complete undecidable
Tagged: exptime
Tagged: decidable
One-copy:
DEXP-time complete
Ping-pong protocols: Ptime
Additional results for variants of basic model (AC, xor, modular exp, …)
Many protocol case studies
Murphi [Shmatikov, He, …]
• SSL, Contract signing, 802.11i, …
Meadows NRL tool
• Participation in IETF, IEEE standards
• Many important examples
Paulson inductive method; Scedrov et al
• Kerberos, SSL, SET, many more
Protocol logic
• BAN logic and successors (GNY, SvO, …)
• DDMP …
Computational model I
“Alice”
oracle tape
“Bob”
oracle tape
Adversary
input tape
work tape
[Bellare-Rogaway, Shoup, …]
Computational model II
Turing machine
Adversary
Turing
machine
Turing
machine
Turing
machine
[Canetti, …]
Computational security: encryption
Passive adversary
• Semantic security
Chosen ciphertext attacks (CCA1)
• Adversary can ask for decryption before
receiving a challenge ciphertext
Chosen ciphertext attacks (CCA2)
• Adversary can ask for decryption before
and after receiving a challenge
ciphertext
Passive Adversary
m0, m1
Challenger
E(mi)
guess 0 or 1
Attacker
Chosen ciphertext CCA1
c
D(c)
m0, m1
Challenger
E(mi)
guess 0 or 1
Attacker
Chosen ciphertext CCA2
c
D(c)
m0, m1
Challenger
E(mi)
c  E(mj)
D(c)
guess 0 or 1
Attacker
Slide: R Canetti
Protocol security
Z
input
Protocol execution
P1

P3
input
P2
P1
P2
S
A
P4
attacker
P4
P3
simulator
F
output
output
Z
Ideal functionality
Slide: Y Lindell
Universal composability
also “reactive simulatability” [BPW], … see [DKMRS]
For every real
adversary A
Protocol
interaction

there exists an
adversary S
Trusted party
REAL
IDEAL
Can we have best of both worlds?
Symbolic model
[NS78,DY84,…]
Complexity-theoretic
model [GM84,…]
Attacker actions
- Fixed set of actions,
nondeterminism
(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
Some relevant approaches
Simulation framework
• Backes, Pfitzmann, Waidner
Correspondence theorems
• Micciancio, Warinschi
Kapron-Impagliazzo logics
Abadi-Rogaway passive equivalence
 (K2,{01}K3) ,  {({101}K2,K5 )}K2, {{K6}K4}K5  
 …
(K2,  ) ,  {({101}K2,K5 )}K2, {  }K5  
 …
(K1,  ) ,  {({101}K1,K5 )}K1, {  }K5  
  (K1,{K1}K7) ,  {({101}K1,K5 )}K1, {{K6}K7}K5  
Proposed as start of larger plan for computational soundness
[Abadi-Rogaway00, …, Adao-Bana-Scedrov05]
Symbolic methods  comp’l results
 Pereira and Quisquater, CSFW 2001, 2004
• Studied authenticated group Diffie-Hellman protocols
• Found symbolic attack in Cliques SA-GDH.2 protocol
• Proved no protocol of certain type is secure, for >3
participants
 Micciancio and Panjwani, EUROCRYPT 2004
• Lower bound for class of group key establishment
protocols using purely Dolev-Yao reasoning
– Model pseudo-random generators, encryption symbolically
• Lower bounds is tight; matches a known protocol
Rest of talk: Protocol composition logic
Protocol
Honest Principals,
Attacker
Private
Data
 Alice’s information
Logic now has
symbolic and
computational
semantics
• Protocol
• Private data
• Sends and receives
Example
{ A, Noncea }
A
{ Noncea, … }
Kb
K
a
B
Alice assumes that only Bob has Kb-1
 Alice generated Noncea and knows that
some X decrypted first message
 Since only X knows Kb-1, Alice knows X=Bob
More subtle example: Bob’s view
{ A, Noncea }
A
Kb
{ Noncea, B, Nonceb }
{ Nonceb}
K
a
B
Kb
 Bob assumes that Alice follows protocol
 Since Alice responds to second message,
Alice must have sent the first message
Execution model
Protocol
• “Program” for each protocol role
Initial configuration
• Set of principals and key
• Assignment of 1 role to each principal
Run
A
B
C
Position in run
x {x}B
({x}B) decr ({z}B)
z
{z}B
Formulas true at a position in run
Action formulas
a ::= Send(P,m) | Receive (P,m) | New(P,t)
| Decrypt (P,t) | Verify (P,t)
Formulas
 ::= a | Has(P,t) | Fresh(P,t) | Honest(N)
| Contains(t1, t2) |  | 1 2 | x 
|  | 
Example
After(a,b) = (b  a)
Notation in papers varies slightly …
Modal Formulas
 After actions, condition
[ actions ] P 
where P = princ, role id
 Before/after assertions
 [ actions ] P 
 Composition rule
[S]P  [T]P
 [ ST ] P 
Logic formulated: [DMP,DDMP]
Related to: BAN, Floyd-Hoare, CSP/CCS, temporal logic, NPATRL
Example: Bob’s view of NSL
Bob knows he’s talking to Alice
[ receive encrypt( Key(B), A,m );
new n;
msg1
send encrypt( Key(A), m, B, n );
receive encrypt( Key(B), n )
]B
msg3
Honest(A)  Csent(A, msg1)  Csent(A, msg3)
where Csent(A, …)  Created(A, …)  Sent(A, …)
Proof System
Sample Axioms:
• Reasoning about possession:
– [receive m ]A Has(A,m)
– Has(A, {m,n})  Has(A, m)  Has(A, n)
• Reasoning about crypto primitives:
– Honest(X)  Decrypt(Y, enc(X, {m}))  X=Y
– Honest(X)  Verify(Y, sig(X, {m})) 
 m’ (Send(X, m’)  Contains(m’, sig(X, {m}))
Soundness Theorem:
• Every provable formula is valid in symbolic model
Modal Formulas
 After actions, condition
[ actions ] P 
where P = princ, role id
 Before/after assertions
 [ actions ] P 
 Composition rule
[S]P  [T]P
 [ ST ] P 
Application DH + CR = ISO 9798-3
Initiator role of DH
[ new a ] I Fresh(I, ga)  HasAlone(I, a)
Initiator role of CR
Fresh(I, m) [send … receive … B… send]
Honest(B)  ActionsInOrder(…)
Combination
• Substitute ga for m in CR
• Apply composition rule, persistence
• Obtain assertion about ISO initiator
Additional issues
Reasoning about honest principals
• Invariance rule, called “honesty rule”
Preserve invariants under composition
• If we prove Honest(X)   for protocol 1
and compose with protocol 2, is formula
still true?
Composing protocols

DH  Honest(X)  …
’
CR  Honest(X)  …
 |- Secrecy
’ |- Authentication
’ |- Secrecy
’ |- Authentication
’ |- Secrecy  Authentication [additive]
[nondestructive]
=
DH  CR  ’
ISO  Secrecy  Authentication
Main results in ICALP Proceedings
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
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
Parts of proof are similar to [Micciancio, Warinschi]
Applications of PCL
 IKE, JFK family key exchange
• IKEv2 in progress
 802.11i wireless networking
• SSL/TLS, 4way handshake, group handshake
 Kerberos v5
 GDOI
 Future work
[Cervesato et al]
[Meadows, Pavlovic]
• Use CPCL to understand computational security of these
protocols, reliance on specific crypto properties
Advantages of Computational PCL
High-level reasoning
• Prove properties of protocols without
explicit reasoning about probability,
asymptotic complexity
Sound for “real crypto”
Composability
• PCL is designed for protocol composition
Identify crypto assumptions needed
Future Work
 Investigate nature of propositional fragment
• Non-classical;  involves some conditional probability
– complexity-theoretic reductions
– connections with probabilistic logics (e.g. Nilsson86)
 Generalize reasoning about secrecy
 Extend logic
• More primitives: signature, hash functions,…
• Remove current syntactic restrictions on formulas
 Information-theoretic semantics (thanks to A Scedrov)
• Only probability; no complexity
 Other fundamental problems
• See Kapron-Impagliazzo, etc.
Conclusion
Symbolic model supports useful analysis
• Tools, case studies, high-level proofs
Computational model more “correct”
• More accurately reflects realistic attack
Two approaches can be combined
• Several current projects and approaches
• One example: computational semantics for
symbolic protocol logic
Credits
 Collaborators
• M. Backes, A. Datta, A. Derek, N. Durgin, C. He,
R. Kuesters, D. Pavlovic, A. Ramanathan, A. Roy,
A. Scedrov, V. Shmatikov, M. Sundararajan, V. Teague,
M. Turuani, B. Warinschi, …
 More information
• References in PPDP, ICALP proceedings
• Web page on Protocol Composition Logic
– http://www.stanford.edu/~danupam/logic-derivation.html
– My web site for related projects not discussed
Science is a social process