Lecture 6 A. Pnueli and L. ZuckFinitary Encoding of ProtocolsWe will present an approach which will enable the encoding of security protocols ina way that will enable their model-checking on a state-based model checker suchas TLV.The approach will be illustrated on the NSPK protocol. Recall its (partial) Casperdefinition:# VariablesAlice, Bob, Carol : AgentNa, Nb, Nc : NoncePK : Agent -> PublicKeySK : Agent -> SecretKeyInverseKeys = (PK, SK)#ProcessesINITIATOR(A,Na) knows PK, SK(A)RESPONDER(B,Nb) knows PK, SK(B)INTRUDER (C,Nc) knows PK, SK(C)#Protocol description0. -> A : B1. A -> B : {na, A}{PK(B)}2. B -> A : {na, nb}{PK(A)}3. A -> B : {nb}{PK(B)}Formal Analysis of Security Protocols, NYU, Spring, 2003 40Lecture 6 A. Pnueli and L. ZuckData Types and the InitiatorObserving the protocol, we identify 3 types of messages. Consequently, we definedatatype message = { h1, PublicKey, Nonce, Agenti |h2, PublicKey, Nonce, Noncei |h3, PublicKey, Noncei }We now encode the protocol for Alice, serving as the initiator. We use an extendeddialect of SPL, inspired by the pattern matching constructs of CSP.Alice ::p : Agentmy nonce, his nonce : Nonce`0: p :∈ {B, C}; my nonce := if p = B then Nab else Nac`1: media ⇐h1, PK [p] , my nonce, Ai`2: media ⇒h2, PK [A], my nonce, ?his noncei`3: media ⇐h3, PK [p] , his noncei`4:Next, we encode the protocol for Bob, serving as the responder.Bob ::p : Agentmy nonce, her nonce : Noncem0: media ⇒h1, PK [B], ?her nonce, ?pim1: my nonce := if p = A then Nba else Nbcm2: media ⇐h2, PK [p], her nonce, my nonceim3: media ⇒h3, PK [B], my nonceim4:Formal Analysis of Security Protocols, NYU, Spring, 2003 41Lecture 6 A. Pnueli and L. ZuckThe IntruderFinally, we present the code for the intruder.Carol ::p, q : Agentn, n1, n2: NonceK : set of Nonce where K = {Nc}loop forever domedia ⇒h1, PK [C], ?n, ?pi; K := K ∪ {n}ormedia ⇒h2, PK [C], ?n1, ?n2i; K := K ∪ {n1, n2}ormedia ⇒h3, PK [C], ni; K := K ∪ {n}orORp∈AgentORq∈Agent,n∈Kmedia ⇐h1, PK [p], n, qiorORn1,n2∈Kmedia ⇐h2, PK [p], n1, n2iorORn∈Kmedia ⇐h3, PK [p], niFormal Analysis of Security Protocols, NYU, Spring, 2003 42Lecture 6 A. Pnueli and L. ZuckNow in SMV-- Needham Schroeder 3. Revised March 4. 03MODULE mainDEFINEag_A := 1; ag_B := 2; ag_C := 3;Nab := 1; Nac := 2; Nba := 3; Nbc := 4; Nc := 5;VARmestype : 0..3;pk : 1..3;f1 : 1..5;f2 : 1..5;K : array 1..5 of boolean;Alice : process Initiator(mestype,pk,f1,f2);Bob : process Responder(mestype,pk,f1,f2);Carol : process Intruder (mestype,pk,f1,f2,K);Id : process Idle;ASSIGNinit(mestype) := 0;init(K[Nab]) := 0;init(K[Nac]) := 0;init(K[Nba]) := 0;init(K[Nbc]) := 0;init(K[Nc]) := 1;Formal Analysis of Security Protocols, NYU, Spring, 2003 43Lecture 6 A. Pnueli and L. ZuckMODULE IdleMODULE Initiator(mestype,pk,f1,f2)DEFINEag_A := 1; ag_B := 2; ag_C := 3;Nab := 1; Nac := 2; Nba := 3; Nbc := 4; Nc := 5;VARloc : 0..4;p : 1..3;mine: 1..5;his : 1..5;ASSIGNinit(loc) := 0;next(loc) := caseloc=0 : 1;loc=1 & mestype=0 : 2;loc=2 & mestype=2 & pk=1 & f1=mine : 3;loc=3 & mestype=0 : 4;1 : loc;esac;next(p) := caseloc=0 & next(loc)=1 : {ag_B,ag_C};1 : p;esac;Formal Analysis of Security Protocols, NYU, Spring, 2003 44Lecture 6 A. Pnueli and L. Zucknext(mine) := caseloc != 0 | next(loc) != 1 : mine;next(p)=ag_B : Nab;1 : Nac;esac;next(mestype) := caseloc=1 & next(loc)=2 : 1;loc=2 & next(loc)=3 : 0;loc=3 & next(loc)=4 : 3;1 : mestype;esac;next(pk) := caseloc=1 & next(loc)=2 : p;loc=3 & next(loc)=4 : p;1 : pk;esac;next(f1) := caseloc=1 & next(loc)=2 : mine;loc=3 & next(loc)=4 : his;1 : f1;esac;next(f2) := caseloc=1 & next(loc)=2 : ag_A;1 : f2;esac;Formal Analysis of Security Protocols, NYU, Spring, 2003 45Lecture 6 A. Pnueli and L. Zucknext(his) := caseloc=2 & next(loc)=3 : f2;1 : his;esac;Formal Analysis of Security Protocols, NYU, Spring, 2003 46Lecture 6 A. Pnueli and L. ZuckResponderMODULE Responder(mestype,pk,f1,f2)DEFINEag_A := 1; ag_B := 2; ag_C := 3;Nab := 1; Nac := 2; Nba := 3; Nbc := 4; Nc := 5;VARloc : 0..3;p : 1..3;mine : 1..5;hers : 1..5;ASSIGNinit(loc) := 0;next(loc) := caseloc=0 & mestype=1 & pk=2 & f2 in {ag_A,ag_C} : 1;loc=1 & mestype=0 : 2;loc=2 & mestype=3 & pk=2 & f1=mine : 3;1 : loc;esac;next(mestype) := caseloc=0 & next(loc)=1 : 0;loc=1 & next(loc)=2 : 2;loc=2 & next(loc)=3 : 0;1 : mestype;esac;Formal Analysis of Security Protocols, NYU, Spring, 2003 47Lecture 6 A. Pnueli and L. Zucknext(pk) := caseloc=1 & next(loc)=2 : p;1 : pk;esac;next(f1) := caseloc=1 & next(loc)=2 : hers;1 : f1;esac;next(f2) := caseloc=1 & next(loc)=2 : mine;1 : f2;esac;next(hers) := caseloc=0 & next(loc)=1 : f1;1 : hers;esac;next(p) := caseloc=0 & next(loc)=1 & f2<4 : f2;1 : p;esac;next(mine) := caseloc != 0 | next(loc) != 1 : mine;next(p)=ag_A : Nba;1 : Nbc;esac;Formal Analysis of Security Protocols, NYU, Spring, 2003 48Lecture 6 A. Pnueli and L. ZuckIntruderMODULE Intruder (mestype,pk,f1,f2,K)DEFINEag_A := 1; ag_B := 2; ag_C := 3;Nab := 1; Nac := 2; Nba := 3; Nbc := 4; Nc := 5;c1 := casec_n1=1 & K[1] : 1;c_n1=2 & K[2] : 2;c_n1=3 & K[3] : 3;c_n1=4 & K[4] : 4;1 : 5;esac;c2 := casec_n2=1 & K[1] : 1;c_n2=2 & K[2] : 2;c_n2=3 & K[3] : 3;c_n2=4 & K[4] : 4;1 : 5;esac;rand_agent := casec_n2 < 4 : c_n2;1 : 1;esac;Formal Analysis of Security Protocols, NYU, Spring, 2003 49Lecture 6 A. Pnueli and L. ZuckVARc_n1 : 1..5;c_n2 : 1..5;spy1 : process Spy1(mestype,pk,f1,f2,K,ag_C);spy2 : process Spy2(mestype,pk,f1,f2,K,ag_C);spy3 : process Spy3(mestype,pk,f1,f2,K,ag_C);reset : process Reset(mestype);fake1 : process Fake(1,mestype,pk,f1,f2,c1,rand_agent);fake2 : process Fake(2,mestype,pk,f1,f2,c1,c2);fake3 : process Fake(3,mestype,pk,f1,f2,c1,3);MODULE Spy1(mestype,pk,f1,f2,K,ag_C)DEFINEcond := mestype=1 & pk=ag_C;VARupdate : Update(cond,f1,K);MODULE Spy2(mestype,pk,f1,f2,K,ag_C)DEFINEcond := mestype=2 & pk=ag_C;VARupdate2 : Update2(cond,f1,f2,K);MODULE Spy3(mestype,pk,f1,f2,K,ag_C)DEFINEcond := mestype=3 & pk=ag_C;VARupdate : Update(cond,f1,K);Formal Analysis of