Day 2 - PowerPoint PPT Presentation

day 2 l.
Skip this Video
Loading SlideShow in 5 Seconds..
Day 2 PowerPoint Presentation
Day 2

play fullscreen
1 / 41
Download
Download Presentation

Day 2

Presentation Transcript

  1. Day 2 The constraint solving algorithm

  2. Outline • Recall of Lesson 1. • The verification algorithm. • A worked example. • Remarks.

  3. Part 1 Refreshing the memory

  4. Syntax: Prolog-based • terms. • a, b, [A,b]*pk(A), … • messages are terms • variables: begin with uppercase (or _) • events • send(t) • recv(t)

  5. Specifying a Protocol: Roles • Roles are lists of events. • Variables are used as parameters. • Roles of NS: initiator(A,B,Na,Nb) = [ send([A,Na]*pk(B)), recv([Na,Nb]*pk(A)), send(Nb*pk(B))]. responder(A,B,Na,Nb) = [ recv([A,Na]*pk(B)), send([Na,Nb]*pk(A)), recv(Nb*pk(B))]).

  6. Scenarios • Used to specify a session. • E.g. • {initiator(a,B,na,Nb), responder(A,b,Na,nb), {recv(nb)} } • Scenarios allow to specify: • how many agents are present in a session • for each agent • its name • what he “knows” • a (non)-secrecy role, that can be used for checking secrecy.

  7. Originator Assumption • When putting together a scenario, make sure that if an agent has a variable (say X) as parameter THEN in the definition of the agent X must occur first in a recv event. • Recall: • initiator(A,B,Na,Nb) = [send([A,Na]*pk(B)),recv([Na,Nb]*pk(A)),send(Nb*pk(B))]. • Then, compare: • {initiator(a,B,na,Nb), responder(A,b,Na,nb), {recv(nb)} } • {initiator(a,b,na,Nb), responder(A,b,Na,nb), {recv(nb)} } • How can we analyze the first scenario?

  8. Solution • Add a recv event in the role definition. • New role definition • initiator(A,B,Na,Nb)=[recv(B), send([A,Na]*pk(B)), recv([Na,Nb]*pk(A)), send(Nb*pk(B))]. • The scenario • {initiator(a,B,na,Nb), responder(A,b,Na,nb), {recv(nb)} } • Not particularly elegant, but sound and effective.

  9. Exercise • Why is it important: • If the O.A. is not satisfied: then • the result of the analysis can be incorrect (more later) • the search space could increase dramatically (crash risks). • Apparently many • initiator(A,B,S,Na) = [recv([A,B]),send([A,Na]*pk(S))]. • Decide if the following scenarios satisfy O.A.: • { initiator(a,B,s,na) } • { initiator(a,B,s,Na) } • { initiator(A,B,S,na) } • { initiator(a,B,B,na) }

  10. Solution • yes • no • no • yes

  11. Part 2 The Verification Algorithm And the constraint solving stuff

  12. Preliminaries: Unification • a substitution is a mapping from variables to terms • {Xa}, {X  Y, Y  a} •  is a unifier of t and s iff t = s. • e.g., p(X,a), q(r(Z),W), ={X  r(Z), W  a} • or 2 ={X  r(b),W  a,Z  b} •  is more general than 2 • two terms unify if they have a unifier • then there exists a most general unifier (mgu)

  13. Constraints • A constraint is a pair: m:T • m is a message term, T is a list of terms. • is called simple if m is a variable. • intuitive meaning: “m is generable from T” • The Constraint Store (CS) is a set of constraints.

  14. the Verification Algorithm • S: scenario • CS: constraint store (initially empty) • K: intruder’s knowledge. • A step of the verification algorithm: • choose the first event e from a non-empty role of S • case 1) e = send(t) • K := K U {t}; proceed • case 2) e = recv(t) • CS := CS U {t:K } • if CS can be solved to CS’ with solution , • S := S; K:= K; CS := CS’; • proceed • otherwise, stop

  15. What is solvable? • CS can be solved to CS’ with solution  if we can apply reduction rules to CS until we obtain CS’, where • CS’ is empty or • CS’ contains only simple constraints.

  16. Synthesis reduction rules • :rewriting step yielding substitution  •  is the empty substitution • Local rules: • Pair: [m1,m2]:T  m1:T , m2:T • hash: h(m):T  m:T • penc: m*pk(a) :T  m:T, a:T • senc: m+k :T  m:T, k:T • sig: m*sk(e)  m:T • Global rule • unify: {m:T,C1,…,Cn} {C1,…,Cn} • provided that =mgu(m,t), tT

  17. Analysis reduction rules (2) • Affect the other side of the constraint. • Local rules • split: m:{[t1,t2]} T  m:{t1,t2} T • pdec: m:{t*pk(e)}  :T  m:{t}  T • sdec: m:T{t+k}  k:T{t-k}, m:T{t,k} • forget about this one • used only for constructed symmetric keys • Global rule • ksub: {m:{t*k}T, C1, …, Cn}  {m:({t*k}T), C1, …, Cn} • where =mgu(k,pk(e)), kpk(e)

  18. the Result • CS0 1 CS1 2… n CSn • each time a constraint in CS is selected and a rule is applied to it • The rewriting stops when • CSn is empty or made of simple constraints • CS is solved • the composition of the substitutions is the result of the simplification:  := 1 2 … n • a constraint is selected that cannot be simplified • CS is unsolvable • there is no result (failure)

  19. Properties • Is it Confluent? • No. • Different reduction sequences are possible: • in total: 4 sources of nondeterminism • choice of the event in the algorithm. • choice of the constraint to be reduced. • choice of the rule to be applied. • in the the analysis rules and in the unify rule there is the additional choice of the term in T to which the rule is applied. • Full backtracking to preserve completeness. • Local analysis reduction rules preserve confluence, and this can be used for optimization.

  20. Part 3 Example

  21. Example • Consider the scenario for NS with OA: {initiator(a,B,na,Nb),responder(A,b,Na,nb), {recv(nb)}} • A possible interleaving: recv([A,B]), send([a,na]*pk(B)) recv([A,Na]*pk(b)), send([Na,nb]*pk(A)) recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • We omit the events after recv(nb)

  22. Example (cont) recv([A,B]), send([a,na]*pk(B)) recv([A,Na]*pk(b)), send([Na,nb]*pk(A)) recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • find out what happens to the CS • T = {a,b,e} (intruder knowledge) • CS = {}

  23. The run (1) recv([A,B]), send([a,na]*pk(B)), recv([A,Na]*pk(b)), send([Na,nb]*pk(A)), recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • Before the step • T = {a,b,e} • CS = {} • After (T does not change) • CS = {[A,B]:{a,b,e}} • By applying pair • CS’ = {A:{a,b,e}, B:{a,b,e}}

  24. The run (2) send([a,na]*pk(B)), recv([A,Na]*pk(b)), send([Na,nb]*pk(A)), recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • Before the step • T = T0 = {a,b,e} • CS = {A:{a,b,e}, B:{a,b,e}} • After • T = T1 = {a,b,e,[a,na]*pk(B)}

  25. The run (3) recv([A,Na]*pk(b)), send([Na,nb]*pk(A)), recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • Before the step • T = T1 = {a,b,e,[a,na]*pk(B)} (T0 = {a,b,e}) • CS = {A:{a,b,e}, B:{a,b,e}} • After • CS = {A:T0, B:T0, [A,Na]*pk(b):T1} • by penc + pair • CS = {A:T0, B:T0, A:T1, Na:T1, b:T1} • by nif • CS = {A:T0, B:T0, A:T1, Na:T1}

  26. The run (4) send([Na,nb]*pk(A)), recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • Before the step • T = T1 = {a,b,e,[a,na]*pk(B)} • T0 = {a,b,e} • CS = {A:T0, B:T0, A:T1, Na:T1} • After • T = T2 = T1 U {[Na,nb]*pk(A) • T1 = {a,b,e,[a,na]*pk(B)} • T0 = {a,b,e} • CS is unchanged

  27. The run (5) recv( [na,Nb]*pk(a)), send([Nb]*pk(B)), recv(nb) ... • Before • T = T2 = T1 U {[Na,nb]*pk(A) • T1 = {a,b,e,[a,na]*pk(B)} • T0 = {a,b,e} • CS = {A:T0, B:T0, A:T1, Na:T1} • After • CS= {A:T0, B:T0, A:T1, Na:T1,[na,Nb]*pk(a):T2} • unify! (Na-> na , Nb -> nb and A-> a) • The unification has to be applied to the rest…

  28. The run (5.1) recv([na,b]*pk(a)), send([nb]*pk(B)), recv(nb) ... • After the unification: • T = T2 = T1 U {[na,nb]*pk(a) • T1 = {a,b,e,[a,na]*pk(B)} • T0 = {a,b,e} • CS= {a:T0, B:T0, a:T1, na:T1} • Unify • CS= {B:{a,b,e}, na: {a,b,e,[a,na]*pk(B)}}

  29. The run (5.2) recv([na,b]*pk(a)), send([nb]*pk(e)), recv(nb) ... • After the unification: • CS= {B:{a,b,e}, na: {a,b,e,[a,na]*pk(B)}} • ksub (unification B -> e) + split • CS= {e:{a,b,e}, na: {a,b,e,a,na}} • unify twice, with empty answer • CS = {} • T = {[na,nb]*pk(a), a,b,e,[a,na]*pk(e)}

  30. The run (5.3) send([nb]*pk(e)), recv(nb) ... • Before • CS = {} • T = {[na,nb]*pk(a), a,b,e,[a,na]*pk(e)} • After • CS = {} • T = {[na,nb]*pk(a), a,b,e,[a,na]*pk(e), [nb]*pk(e)}

  31. The run (5.4) recv(nb) ... • Before • CS = {} • T = {[na,nb]*pk(a), a,b,e,[a,na]*pk(e), [nb]*pk(e)} • After • CS = {nb:{[na,nb]*pk(a), a,b,e,[a,na]*pk(e), [nb]*pk(e)}} • pdec • CS = {nb:{[na,nb]*pk(a), a,b,e,[a,na]*pk(e),nb}} • unify (empty substitution) • CS = {} !!!

  32. The solution substitution • We ended up with an empty CS • => the system has a solution • in the process, reduction rules gave us the `solution substitution’  = {A->a,Na->na,Nb->b, B->e}

  33. Part 3 Considerations

  34. Again, the O.A. • Consider two roles: • roleA(X) = { send(X) } • roleB(Nb) = { recv(Nb) } • and scenario { roleA(X), roleB(nb) } • intruder knowledge: {a,b,e} • constraints generated: • nb : {X} • solvable, by rule (unify) • this is not what we want!

  35. Laziness • We stop simplifying a constraint when the lhs is a variable. • This enforces a call-by-need mechanism. • As long as the lhs is a variable the constraint is trivially solvable. • If subsequent unification step instantiate the lhs of a constraint, then I check further if it can be solved. • It would be silly to guess.

  36. Another Example for Laziness • Consider two roles: roleA(X,A) = { recv(X), recv(X*pk(A)) } roleB(Na,A) = { send(Na*pk(A)) } • and this scenario:{roleA(X, b), roleB(na,b)} • initial intruder knowledge: {a,b,e} • there’s only one possible order: send(na*pk(b)), recv(X), recv(X*pk(b))

  37. Another Example for Laziness • send(na*pk(b)), recv(X), recv(X*pk(b)) • two constraints are generated: • X : {a,b,e} • X*pk(b) : {a,b,e,na*pk(b)} • by rule (unify): • na : {a,b,e} • not solvable! • we did not know this after the first step.

  38. Bibliography Remark • The system is strongly based on that of Millen and Shmatikov [MS01] • Various differences: • Constraints checked “on the fly” • Consider run also with unfinished roles (very important in practice) • Few other minor things.

  39. Exercises: decide if solvable and provide a substitution • 1) • Kab : {a,b,e} • [na, Kab]+kas : {a,b,e} U {[na,a,b]+kas} • secret : {a,b,e} U {secret+Kab} • 2) • Kab : {a,b,e} • Kab+kas : {a,b,e,[na,a,b]+kas } • secret : {a,b,e,[na,a,b]+kas } U { secret+Kab } • 3) • Y : {e} • X*pk(Y) : {e, h(msg)} • h([X,Y]) : {e, h(msg)}

  40. Solutions • 1. solution: Yes. subst. = {Kab -> [a,b]} • it is a type flow attack • solution: No. (the first two already) • solution: Yes. subst: { X->h(msg), Y->e } or { X->e, Y->e }

  41. Exercise for home • Add one or more rules to the system so that it handles secret keys (signatures).