1、Analysis of Security Protocols (III),John C. Mitchell Stanford University,Analyzing Security Protocols,Non-formal approaches (can be useful, but no tools) Some crypto-based proofs Bellare, RogawayBAN and related logics Axiomatic semantics of protocol stepsMethods based on operational semantics Intru
2、der model derived from Dolev-Yao Protocol gives rise to set of traces Perfect encryption Possible to include known algebraic properties,Example projects and tools,Prove protocol correct Paulsons “Inductive method”, others in HOL, PVS, etc. Bolignano - Abstraction methods MITRE - Strand spaces Proces
3、s calculus approach: Abadi-Gordon spi-calculus Search using symbolic representation of states Meadows: NRL Analyzer, Millen: Interrogator Exhaustive finite-state analysis FDR, based on CSP Lowe, Roscoe, Schneider, Mur - specialized input language Clarke et al. - state search with axiomatic intruder
4、model,Explicit Intruder Method,Intruder Model,Analysis Tool,Formal Protocol,Informal Protocol Description,Gee whiz. Looks OK to me.,A notation for inf-state systems,Define protocol, intruder in minimal framework Disadvantage: need to introduce new notation,Protocol Notation,Non-deterministic infinit
5、e-state systems FactsF := P(t1, , tn)t := x | c | f(t1, , tn) States F1, , Fn Multiset of facts Includes network messages, private state Intruder will see messages, not private state,Multi-sorted first-order atomic formulas,State Transitions,TransitionF1, , Fk x1 xm. G1, , Gn What this means If F1,
6、, Fk in state , then a next state has Facts F1, , Fk removed G1, , Gn added, with x1 xm replaced by new symbols Other facts in state carry over to Free variables in rule universally quantified Pattern matching in F1, , Fk can invert functions,Finite-State Example,Predicates: State, Input Function: C
7、onstants: q0, q1, q2, q3, a, b, nil Transitions: State(q0), Input(a x) State(q1), Input(x) State(q0), Input(b x) State(q2), Input(x).,q0,q1,q3,q2,b,a,a,a,b,b,b,a,b,Existential Quantification,Natural-deduction proof ruley/x( elim) x. Summary: for proof from x., choose new symbol and proceed from y/x,
8、y not free in any other hypothesis,Infinite-State Example,Predicates: State, Input, Color Function: Constants: q0, a, b, nil, red, blue Transitions: State(q), Input(a x), Color(q,red) q. State(q), Input(x), Color(q,blue), Color(q,red) .,Input a: change color Input b: same color,Need to preserve fact
9、s explicitly,Turing Machine,Predicates Current(state,cell) - current state, tape pos. Contents(cell, symbol) - contents of tape cell Adjacent(cell, cell) - keep cells in order Constants q0, q1, q2, - finite set of states c0, ceot - initial tape cells “0”, “1”, “b” - tape symbols,Turing Machine (II),
10、Transitions Adjacent(c0, ceot) Adjacent(c, ceot) c. Adjacent(c,c), Adjacent(c,ceot)Current(qi,c), Contents(c,“0”), Adjacent(c,c) Current(qk,c), Contents(c,“1”), Adjacent(c,c)Current(qi,c), Contents(c,“1”), Adjacent(c,c) Current(qk,c),Contents(c,“0”), Adjacent(c,c),infinite linear tape,sample move ri
11、ght,sample move left,.,c,eot,c,.,c,eot,Simplified Needham-Schroeder,Predicates Ai, Bi, Ni - Alice, Bob, Network in state i Transitions x. A1(x) A1(x) N1(x), A2(x) N1(x) y. B1(x,y) B1(x,y) N2(x,y), B2(x,y) A2(x), N2(x,y) A3(x,y) A3(x,y) N3(y), A4(x,y) B2(x,y), N3(y) B3(x,y)picture next slide,A B: na,
12、 AKb B A: na, nbKa A B: nbKbAuthentication A4(x,y) B3(x,y) y=y,Sample Trace,A2(na),A1(na),A2(na),A2(na),A3(na, nb),A4(na, nb),A4(na, nb),B2(na, nb),B1(na, nb),B2(na, nb),B3(na, nb),B2(na, nb),N1(na),N2(na, nb),N3( nb),x. A1(x) A1(x) A2(x), N1(x) N1(x) y. B1(x,y) B1(x,y) N2(x,y), B2(x,y) A2(x), N2(x,
13、y) A3(x,y) A3(x,y) N3(y), A4(x,y) B2(x,y), N3(y) B3(x,y),Common Intruder Model,Derived from Dolev-Yao model 1989 Adversary is nondeterministic process Adversary can Block network traffic Read any message, decompose into parts Decrypt if key is known to adversary Insert new message from data it has o
14、bserved Adversary cannot Gain partial knowledge Guess part of a key Perform statistical tests, ,Formalize Intruder Model,Intercept and remember messagesN1(x) M(x) N2(x,y) M(x), M(y) N3(x) M(x) Send messages from “known” dataM(x) N1(x), M(x) M(x), M(y) N2(x,y), M(x), M(y) M(x) N3(x), M(x) Generate ne
15、w data as neededx. M(x)Highly nondeterministic, same for any protocol,Attack on Simplified Protocol,A2(na),A1(na),A2(na),A2(na),B1(na, nb),N1(na),x. A1(x) A1(x) A2(x), N1(x) N1(x) M(x) x. M(x) M(x) N1(x), M(x) N1(x) y. B1(x,y),M(na),M(na), M(na),N1(na),A2(na),M(na), M(na),A2(na),M(na), M(na),Continu
16、e “man-in-the-middle” to violate specification,Modeling Perfect Encryption,Encryption functions and keys For public-key encryption two key sorts: e_key, d_key predicate Key_pair(e_key, d_key) Functions enc : e_key msg - msgdec : d_key msg - msg (implicit in pattern-matching) Properties of this model
17、 Encrypt, decrypt only with appropriate keys Only produce enc(key, msg) from key and msg (!) This is not true for some encryption functions,Steps in public-key protocol,Bob generates key pair and publishes e_key u. d_key v. Bob1(u,v) Bob1(u,v) NAnnounce(u), Bob2(u,v) Alice sends encrypted message to
18、 Bob Alice1(e,d,x), NAnnounce(e) Alice2(e,d,x,e) Alice2(e,d,x,e) N1(enc(e,x,e), Alice3(u,v,x,w) Bob decrypts Bob1(u,v), N1(enc(u, x,y) z. Bob1(u,v,x,y,z),Intruder Encryption Capabilities,Intruder can encrypt with encryption key Me(k), Mdata(x) Ni(enc(k,x), Me(k), Mdata(x) Intruder can decrypt with d
19、ecryption key Nj(enc(k,x),Key_pair(k,k), Md(k), Mdata(x), . Add to previous intruder modelAssumes sorts data, e_key, d_key with typedpredicates Mdata(data), Me(e_key), Md(d_key),Intruder: power and limitations,Can find some attacks Needham-Schroeder by exhaustive search Other attacks are outside mod
20、el Interaction between protocol and encryption Some protocols cannot be modeled Probabilistic protocols Steps that require specific property of encryption Possible to prove erroneous protocol correct Requires property that crypto does not provide,Optimize Protocol + Intruder,Adversary receives all m
21、essages; no net Replace Alicei(x,y) Nj(x), Alicek(x,y) Nj(x) M(x) M(z) Nj(z), M(z) Nj(x), Bobi(w) Bobj(w,y) By Alicei(x,y) M(x), Alicek(x,y) M(z), Bobi(w) Bobj(w,y),Alices message can go to Bob or M. M can replay or send different msg,All messages go directly to M. M can forward or send different ms
22、g,Additional Optimizations,Intruder can simulate honest participants If additional independent sessions are useful for attack, then intruder can simulate these sessions Therefore - suffices to consider single initiator, single responder, and intruder (for this protocol). For decidability, bound on i
23、ntruder Lowe Suffices to bound the number of new nonces Analyze .,Analysis of Protocol+Intruder,Prove properties of protocols Unbounded # of participants, message space Prove that system satisfies specification Paulson, etc: prove invariant holds at all reachable states Spi-calculus: prove protocol
24、equivalent ideal protocol Symbolic search with pruning Search backward from error Prune search by proving forward invariants Exhaustive finite-state methods Approximate infinite-state system by finite one Search all states, perhaps with optimizations,Example description languages,First- or Higher-or
25、der Logic Define set of traces, prove protocol correct Horn-clause Logic x (A1A2 B) Symbolic search methods Process calculus FDR model checker based on CSP Spi-calculus proof methods based on pi-calculus Additional formalisms CAPSL protocol description language Millen Mur language for finite-state s
26、ystems,Paulsons Inductive Method,Define set TR of traces of protocol+intruder Similar to traces in unifying formalism Transition F1, , Fk x1 xm. G1, , Gn gives one way of extending trace Auxiliary functions mapping traces to sets Analz(trace) = data visible to intruder Synth(trace) = messages intrud
27、er can synthesize Definitions and proofs use induction Similar inductive arguments for many protocols,Symbolic Search Methods,Examples: NRL Protocol Analyzer, Interrogator Main idea Write protocol as set of Horn clauses Transition F1, , Fk x1 xm. G1, , Gn can be Skolemized and translated to Prolog c
28、lauses Search back from possible error for contradiction This is usual Prolog refutation procedure Important pruning technique Prove invariants by forward reasoning Use these to avoid searching unreachable states,Process Calculus Description,Protocol defined by set of processes Each process gives on
29、e step of one principal Can derive by translation from unifying notation F1, , Fk x1 xm. G1, , Gn is one process Replace predicates by port names Replace pattern-matching by explicit destructuring In pi-calculus, use in place of Example B1(x,y) N2(x,y), B2(x,y) b1(p). let x=fst(p) and y=snd(p) in n2
30、x,y| b2 x,y end,Spi-Calculus AG97, .,Write protocol in process calculus Express security using observ. equivalence Standard relation from programming language theoryP Q iff for all contexts C , same observations about CP and CQ Context (environment) represents adversary Use proof rules for to prove
31、security Protocol is secure if no adversary can distinguish it from an idealized version of the protocol,Finite-state methods,Two sources of infinite behavior Many instances of participants, multiple runs Message space or data space may be infinite Finite approximation Transitions: F1, , Fk x1 xm. G
32、1, , Gn choose fixed number of Skolem constants Terms: restrict repeated functions f(f(f(f(x) Can express finite-state protocol + intruder in CSP : FDR-based model checking projects Other notations: Mur project, Clarke et al., .,Security Protocols in Mur,Standard “benchmark” protocols Needham-Schroe
33、der, TMN, Kerberos Study of Secure Sockets Layer (SSL) Versions 2.0 and 3.0 of handshake protocol Include protocol resumption Discovered all known or suspected attacks Recent work on tool optimizationShmatikov, Stern, .,Malleability Dolev,Dwork,Naor,Idealized assumption If intruder produces Network(
34、enc(k,x) then either Network(enc(k,x) M (enc(k,x) (replay) M(k), M(x) M (enc(k,x) (knows parts) Not true for RSA encrypt(k,msg) = msgk mod N property encr(x*y) = encr(x) * encr(y) Model Network(enc(k,x) M () . Network (enc(k,c*x) Can send encrypted message without “knowing” messageFinite state ?,Aut
35、hentication and Secrecy for Handshake Protocols,How many protocols are there to verify? Average length 7 steps Data fields per message 5 fields Distinct ways to fill a field 50 entries Number of possible combinations 1750 protocols Research directions Get the monkeys and typewriters going Easier description and specification, faster tools Improved analysis of timestamps, . Interaction between protocol and crypto primitives,
