Transcript POPL 01 Talk - Stanford University

Probabilistic Polynomial-Time
Process Calculus for Security
Protocol Analysis
John Mitchell
Stanford University
P. Lincoln, M. Mitchell,
A. Ramanathan, A. Scedrov, V. Teague
Outline
Some discussion of protocols
Goals for process calculus
Specific process calculus
•
•
•
•
•
Probabilistic semantics
Complexity – probabilistic poly time
Asymptotic equivalence
Pseudo-random number generators
Equational properties and challenges
Protocol Security
Cryptographic Protocol
• Program distributed over network
• Use cryptography to achieve goal
Attacker
• Intercept, replace, remember messages
• Guess random numbers, do computation
Correctness
• Attacker cannot learn protected secret
or cause incorrect protocol completion
IKE subprotocol from IPSEC
m1
A, (ga mod p)
A
B, (gb mod p), signB(m1,m2)
m2
signA(m1,m2)
B
Result: A and B share secret gab mod p
Analysis involves probability, modular exponentiation, digital
signatures, communication networks, …
Simpler: Challenge-Response
Alice wants to know Bob is listening
• Send “fresh” number n, Bob returns f(n)
• Use encryption to avoid forgery
Protocol
• Alice  Bob: { nonce }K
• Bob  Alice: { nonce * 5 }K
Can Alice be sure that
– Message is from Bob?
– Message is in response to one Alice sent?
Important Modeling Decisions
How powerful is the adversary?
• Simple replay of previous messages
• Decompose, reassemble and resend
• Statistical analysis, timing attacks, ...
How much detail in model of crypto?
• Assume perfect cryptography
• Include algebraic properties
– encr(x*y) = encr(x) * encr(y) for
RSA encrypt(k,msg) = msgk mod N
Standard analysis methods
Finite-state analysis
Logic based models
Easy
• Symbolic search of protocol runs
• Proofs of correctness in formal logic
Consider probability and complexity
• More realistic intruder model
• Interaction between protocol and
cryptography
Hard
High
Hand proofs


Poly-time calculus
Spi-calculus
Athena Paulson
 NRL
Bolignano
BAN logic

Low
Sophistication of attacks
Comparison
FDR

Low
High
Protocol complexity
Murj

Outline
Some discussion of protocols
Goals for process calculus
Specific process calculus
•
•
•
•
•
Probabilistic semantics
Complexity – probabilistic poly time
Asymptotic equivalence
Pseudo-random number generators
Equational properties and challenges
Language Approach
[Abadi, Gordon]
Write protocol in process calculus
Express security using observational equivalence
• Standard relation from programming language theory
P  Q iff for all contexts C[ ], same
observations about C[P] and C[Q]
• Context (environment) represents adversary
Use proof rules for  to prove security
• Protocol is secure if no adversary can distinguish it
from some idealized version of the protocol
Great general idea; application is complicated
Probabilistic Poly-time Analysis
Add probability, complexity
Probabilistic polynomial-time process calc
• Protocols use probabilistic primitives
– Key generation, nonce, probabilistic encryption, ...
• Adversary may be probabilistic
Express protocol and spec in calculus
Security using observational equivalence
• Use probabilistic form of process equivalence
Secrecy for Challenge-Response
Protocol P
A  B: { i } K
B  A: { f(i) } K
“Obviously’’ secret protocol Q
A  B: { random_number } K
B  A: { random_number } K
Analysis: P  Q reduces to crypto condition
related to non-malleability [Dolev, Dwork, Naor]
– Fails for RSA encryption if f(i) = 2i
Specification with Authentication
Protocol P
A  B: { random i } K
B  A: { f(i) } K
A  B: “OK”
if f(i) received
“Obviously’’ authenticating protocol Q
A  B: { random i } K
public channel
private channel
B  A: { random j } K i , j
public channel
A  B: “OK”
private channel
if private i, j match public msgs
Nondeterminism vs encryption
Alice encrypts msg and sends to Bob
•
A  B: { msg } K
Adversary uses nondeterminism
• Process E0 c0 | c0 | … | c0
• Process E1 c1 | c1 | … | c1
• Process E
c(b1).c(b2)...c(bn).decrypt(b1b2...bn, msg)
In reality, at most 2-n chance to guess n-bit key
Semantics
Nondeterministic
Probabilistic Semantics
Semantics
0.2
0.5
0.5
0.2
0.3
0.2
0.5
0.5
0.3
0.5
0.5
0.2
0.3
0.3
0.2
0.5
0.2
0.3
0.5
0.5
Prove initial results for arbitrary scheduler
Methodology
 Define general system
•
•
•
Process calculus
Probabilistic semantics
Asymptotic observational equivalence
 Apply to protocols
•
•
Protocols have specific form
“Attacker” is context of specific form
–
Induces coarser observational equivalence
This talk: general calculus and properties
Outline
Some discussion of protocols
Goals for process calculus
Specific process calculus
•
•
•
•
•
Probabilistic semantics
Complexity – probabilistic poly time
Asymptotic equivalence
Pseudo-random number generators
Equational properties and challenges
Technical Challenges
Language for prob. poly-time functions
• Extend work of Cobham, Cook, Hofmann
Replace nondeterminism with probability
• Otherwise adversary is too strong ...
Define probabilistic equivalence
• Related to poly-time statistical tests ...
Syntax
Bounded -calculus with integer terms
P :: = 0
|
cq(|n|) T
|
cq(|n|) (x). P
|
cq(|n|) . P
|
[T=T] P
|
P|P
|
! q(|n|) . P
send up to q(|n|) bits
receive
private channel
test
parallel composition
bounded replication
Terms may contain symbol n; channel width
and replication bounded by poly in |n|
Probabilistic Semantics
Basic idea
• Alternate between terms and processes
– Probabilistic evaluation of terms (incl. rand)
– Probabilistic scheduling of parallel processes
Two evaluation phases
• Outer term evaluation
– Evaluate all exposed terms, evaluate tests
• Communication
– Match send and receive
– Probabilistic if multiple send-receive pairs
Scheduling
Outer term evaluation
• Evaluate all exposed terms in parallel
• Multiply probabilities
Communication
•
•
•
•
E(P) = set of eligible subprocesses
S(P) = set of schedulable pairs
Prioritize – private communication first
Choose highest-priority communication
with uniform (or other) probability
Example
Process
• crand+1 | c(x).dx+1 | d2 | d(y). ex+1
Outer evaluation
• c1 | c(x).dx+1 | d2 | d(y). ex+1
• c2 | c(x).dx+1 | d2 | d(y). ex+1
Communication
• c1 | c(x).dx+1 | d2 | d(y). ex+1
Choose according to probabilistic scheduler
Each
prob ½
Example (again)
crand+1 | c(x).dx+1 | d2 | d(y). ex+1
Outer
Eval
Each with prob 0.5
c2 | c(x).dx+1 | d2 | d(y). ex+1
c1 | c(x).dx+1 | d2 | d(y). ex+1
Comm
Step
Choose according to probabilistic scheduler
Complexity results
Polynomial time
• For each process P, there is a poly q(x)
such that
– For all n
– For all probabilistic schedulers
– All minimal evaluation contexts C[ ]
eval of C[P] halts in time q(|n|+|C[]|)
• Minimal evaluation context
– C[ ] = c(x).d(y)…[ ] | c20 | d7 | e492 | …
Complexity: Intuition
Bound on number of communications
• Count total number of inputs, multiplying
by q(|n|) to account for ! q(|n|) . P
Bound on term evaluation
• Closed T evaluated in time qT(|n|)
Bound on time for each comm step
• Example: cm | c(x).P  [m/x]P
• Substitution bounded by orig length of P
– Size of number m is bounded
– Previous steps preserve # occurr of x in P
Outline
Some discussion of protocols
Application of process calculus
Specific process calculus
•
•
•
•
•
Probabilistic semantics
Complexity – probabilistic poly time
Asymptotic equivalence
Pseudo-random number generators
Equational properties and challenges
Problem:
How to define process equivalence?
Intuition
• | Prob{ C[P]  “yes” } - Prob{ C[Q]  “yes” } | < 
Difficulty
• How do we choose ?
– Less than 1/2, 1/4, … ?
(not equiv relation)
– Vanishingly small ? As a function of what?
Solution
• Use security parameter
– Protocol is family { Pn }
n>0
indexed by key length
• Asymptotic form of process equivalence
Probabilistic Observational Equiv
Asymptotic equivalence within f
Process, context families { Pn } n>0 { Qn } n>0 { Cn } n>0
P f Q if  contexts C[ ].  obs v. n0 .  n> n0 .
| Prob[Cn[Pn]  v] - Prob[Cn[Qn]  v] | < f(n)
Asymptotically polynomially indistinguishable
P  Q if P f Q for every polynomial f(n) = 1/p(n)
Final def’n gives robust equivalence relation
Outline
Some discussion of protocols
Application of process calculus
Specific process calculus
•
•
•
•
•
Probabilistic semantics
Complexity – probabilistic poly time
Asymptotic equivalence
Pseudo-random number generators
Equational properties and challenges
Compare with standard crypto
Sequence generated from random seed
Pn: let b = nk-bit sequence generated from n random bits
in PUBLIC b end
Truly random sequence
Qn: let b = sequence of nk random bits
in PUBLIC b end
P is crypto strong pseudo-random generator
PQ
Equivalence is asymptotic in security parameter n
Desired equivalences




P | (Q | R)  (P | Q) | R
P|QQ|P
P|0  P
P  Q  C[P]  C[Q]
P   c. ( c<1> | c(x).P)
x FV(P)
Warning: hard to get all of these…
How to establish equivalence
Labeled transition system
• Allow process to send any output, read any input
• Label with numbers “resembling probabilities”
Simulation relation
 on processes
• Relation ~
 Q and P r P’, then exists Q’
• If P ~
r
 Q’
with Q
Q’ and P’ ~
Weak form of prob equivalence
• But enough to get started …
Hold for uniform scheduler




P | (Q | R)  (P | Q) | R
P|QQ|P
P|0  P
P  Q  C[P]  C[Q]
Problem
Want this equivalence
• P  c. ( c<1> | c(x).P)
x FV(P)
Fails for general calculus, general 
• P = d(x).e<x>
• C[ ] = d.( d<1> | d(y).e<0> | [ ] )
Comparison
d.( d<1> | d(y).e<0> | c. ( c<1> | c(x).P) )
left
d.( d<1> | d(y).e<0> | d(x).e<x> )
left
e<0>
right
e<1>
P
c<1>
e<0>
c<1>
left
e<0>
Even prioritizing private channels, equivalence fails
right
e<1>
Paradox
Two processors connect by network
Each does private actions
Unrealistic interaction
• Private coin flip in Beijing does not
influence coin flip in Washington
Solutions
Modify scheduler
• Process private channels left-to-right
• Each channel: random send-receive pair
Restrict syntax of protocol, attack
• C[ P ] = C[ c. ( c<1> | c(x).P) ]
for all contexts C[ ] that
– do not share private channels
– do not bind channel names used in [ ]
Modification of scheduler more reasonable for protocols
Current State of Project
Framework for protocol analysis
• Determine crypto requirements of protocols
• Precise definition of crypto primitives
Probabilistic ptime language
Process framework
• Replace nondeterminism with rand
• Equivalence based on ptime statistical tests
Methods for establishing equivalence
• Develop probabilistic simulation technique
Examples: Diffie-Hellman, Bellare-Rogaway, …
Compositionality
Property of observational equiv
AB
CD
A|C  B|D
similarly for other process forms
Zero-Knowledge Protocol
I know a number x with Q(x)
P
Answer these questions
V
Here. Now you’ll believe me.
 Witness protection program
• Q(x) iff  w. P(x,w)
• Prove  w. P(x,w) without revealing w
Identify Friend or Foe
Sequential
M
• One
conversation at
a time
Concurrent
• Base station
proves identity
concurrently
V
A
Base
S
prover
verifiers
Are concurrent sessions still zero-k ?