Fine-Grained MSR Specifications
for
Quantitative Security Analysis
Iliano Cervesato
[email protected]
ITT Industries, inc @ NRL Washington, DC
http://theory.stanford.edu/~iliano/
Security Analysis of Protocols @ DIMACS
July 9, 2004
Qualitative (Dolev-Yao) Analysis
 Classifies protocol operations in
 Possible (Dolev-Yao)
 Reception/transmission
 Crypto with key, …
 Impossible
 Guessing keys
 Breaking crypto, …
“Easy”
(polynomial)
“Hard”
(exponential)
 Security assessed only on possible ops
 “Easily” achieved by most current tools
 What next?
Quantitative Security Analysis
1/24
Analysis beyond Dolev-Yao
Data
Symbolic
Perfect
C
r
y
p
t
o
Bit-oriented
More ops
- xor
- DH, …
Type confusion
Guessing
Probabilistic
Cost-aware
Real
Quantitative Security Analysis
Crypto hybrid
- probability
- complexity
2/24
Cost-Aware Security Analysis
 Assign cost to operations
[Meadows,01]
 Including non Dolev-Yao
 Discrete logarithm, factoring, …
 (Verifiable) guessing
[Lowe,02]
 Principal subversion, …
 Applications
 Estimate actual resources needed for attacks
 Resources limitation (smart cards, PDAs, …)
 DoS resistance assessment
 Comparing attacks or protocols
Quantitative Security Analysis
3/24
Outline
 Protocol specification
 MSR  Fine-Grained MSR
 Technique applies to other languages
 Traces and Scripts
 Cost Model
 Operations  Scripts
 Cost-aware Security
 Threshold analysis
 Comparative analysis
Quantitative Security Analysis
4/24
MSR
 Executable protocol specification language
 Theoretical results
 Practice
 Decidability
 Kerberos V
 Most powerful intruder, …
 Implementation underway
 3 generations already
 MSR 1: (here)
 MSR 2: 1 + strong typing
 MSR 3: 2 + w-multisets
 Based on MultiSet Rewriting
 Foundations in (linear) logic
 Ties to Petri nets and process algebra
Quantitative Security Analysis
5/24
Multiset Rewriting …
 Multiset: set with repetitions allowed
 a,b,c  a,a,b,c,c,c
 Rewrite rule:
r: N1  N2
 Application:
state
M1

M2
M’, N1  M’, N2
Quantitative Security Analysis
6/24
… with Existentials
 msets of 1st-order atomic formulas
 Rules:
r: F(x)  n. G(x,n)
 Application
M1

M2
M’, F(t)  M’, G(t,c)
c not in M1
Quantitative Security Analysis
7/24
Traces and Scripts
 Traces
 Rewrite sequence (r1,q1),…,(rn,qn) from M0 to Mn
 Rules ri
 Substitutions qi
 Scripts
 Parametric traces
 S, (r,x)
 S1 + S 2
 !n S
Vitaly’s
symbolic traces
 Normal run: SNR
 Attack scripts: SA
Quantitative Security Analysis
8/24
MSR for Security Protocols
 Messages
A, k, n,…
{m}k, (m,m’), …
Princ., keys, nonces, …
Encryption, concat., …
N(m)
M*(t1,…,tn)
MA(t1,…,tn)
Network messages
Public data
Private data
Lv(t1,…,tn)
Local states
 Predicates
 I(m)
Quantitative Security Analysis
Intruder info.
9/24
A  B: {nA, A}kB
B  A: {nA, nB}kA
A  B: {nB}kB
Example
 Needham-Schroeder protocol
Initiator role
PrvKA(kA,k’A),
PubK*(B,kB)
L(kA,k’A,kB,nA),
N({nA,nB}kA)
Quantitative Security Analysis


nA.
PrvKA(kA,k’A),
PubK*(B,kB),
L(kA,k’A,kB,nA),
N({nA,A}kB)
N({nB}kB)
10/24
Preparing for Cost Assignment
 Isolate operations
Verification
 Success
 Failure
Construction
 Split LHS into atomic
steps
 Allow failure
 Apply rule in stages
Pre-screening
Detailed verification
Quantitative Security Analysis
11/24
Fine-Grained MSR (1)
 Rules
Clean-up
lhs  rhs else cr
 Predicates
Registers
Headers
Rv(m)
Nh(m)
 Phased execution
Select rule based only on predicates
Verify if arguments match
 Allow failure
Quantitative Security Analysis
12/24
Fine-Grained MSR (2)
 Verification rules
Nh(x)  R(x)
Lv(x)  R(x)
R(y), R’(opy(x))  R’’(x)
R(x), R’(x)  .
R(x)  R’(m)
…
else cr
else cr
 Construction rules
Remain the same
Quantitative Security Analysis
13/24
Fine-Grained Intruder
Dolev-Yao style
I(g), I(gx)  I(x)
 Nh(x)  I(x)
 M*(x)  I(x)
 I(y), I(opy(x))  I(x)
 I(x)  Nh(x)
 .  x. I(x)
 I(x)  I(op(x))
Subversion
Guessing
 .  X(A)
 X(A)  .
 X(A), MA(x)  X(A), I(x)
Quantitative Security Analysis
…  G(x)
…  V1(m1)
…  V2(m2)
G(x), V1(y), V2(y)  I(x)
14/24
Cost
S vt
A
 t: cost type
Time, space, energy, …
 A: principal incurring cost
 v: amount of cost
Physical measurements
0 /  (Dolev-Yao model)
Complexity classes
Quantitative Security Analysis
15/24
Assigning Cost – Basic Operations
 Network
 Storage
 Operations
 Construction
 Successful verification
 Failed verification
 Subversion
 Guessing
 Supports
very high
precision
 Difficulty
depends on
precision
 Possibly
subjective
 Various ways
Quantitative Security Analysis
16/24
Assigning Costs – Traces & Scripts
 Traces: k(T)
Add up basic costs
 Monotonic costs: time, energy, …
 Non-monotonic: space, …
 Scripts: k(S)
Interval arithmetic
 Script alternative
Quantitative Security Analysis
17/24
Quantitative Security Analysis
A model checking view
 Explicit state MC
 Direct
 Symbolic MC
 Via encoding
Quantitative Security Analysis
C  0 (Dolev-Yao)
C  k1
C  k2
18/24
Threshold Analysis
 k(SNR)  kHW/HCI ?
 Cost of normal run acceptable?
 PDAs, cell phones, …
 k(SA)  kI ?
 Cost of attack/defense acceptable?
 Cost of candidate attack vs. resources
 Non Dolev-Yao operations
 min x. k(SA(x))  kI++ ?
 Design protocol
 Fine-tuning parameters
Quantitative Security Analysis
19/24
Comparative Analysis
 k(SA1)  k(SA2) ?
 Comparing attacks
 Protocol can always be attacked
 k(SP1)  k(SP2) ?
 Comparing protocols
 kB(SA)  kI(SA) ?
 Comparing attack and defense costs
 Denial of Service
– “Tit for tat” – Carl Gunter
Quantitative Security Analysis
20/24
Typical Client/Server Exchange
Server
Client
scq
tcq
request
ssq
tsq
scc
tcc
challenge
ssc
tsc
scr
tcr
response
-(ssq+ssc)
tsr
sco
tco
ok
0
tso
 T
 B
Quantitative Security Analysis
21/24
Time DoS
1.

2.
tcq
0

q
c
tsq
tsq
tsc
 Service rate: 1/tsq
 Usually dominated by
networking costs
 Service rate
 1/(tsq + tsc)
 Attack rate
 1/tcq
3.
q
tcq
0

c

Quantitative Security Analysis
tsq
tsc
ts
r
 Service rate
 1/(tsq + tsc + tsr)
 Attack rate
Better
attack
 1/tcq
22/24
Space DDoS
tcq
0
0
0

q
c

0
ssq
tsq
ssc
tsc
-(ss
+ss
q
c)
ts
T
r
 B
 Max concurrent requests
 n(B) = B / (ssq + ssc)
B
n(B) - 1
 Optimal time-out
Space
 tmin  T
 T  (tsq + tsc)* (n(B) – 1)
 Example
ssc
 tsq + tsc = 100 ms
 tmin = 90 s
B = 1.28 Mb
T  ~16 min
ssq
1
 ssq + ssc = 128 b
Time
tsq tsc
T
tsr
 n(B) = 10,000
Quantitative Security Analysis
23/24
Conclusions
 Quantitative protocol analysis
 Cost conscious attacks (non Dolev-Yao)
 Fine-Grained specification languages (MSR)
 Related work
 C. Meadows: Cost framework for DoS
 G. Lowe: guessing attacks
 D. Tomioka, et al: cost for spi-calculus
 Future work





Attack costs: WEP
DoS aware protocols: JFK, client puzzles, bins
Protocol analysis as optimization problem
Economics of network security
Complexity-based costs and mixing probability
Quantitative Security Analysis
24/24
Descargar

Relating Strands and Multiset Rewriting For Security