Lecture 6 A Pnueli and L Zuck Finitary Encoding of Protocols We will present an approach which will enable the encoding of security protocols in a way that will enable their model checking on a state based model checker such as TLV The approach will be illustrated on the NSPK protocol Recall its partial Casper definition Variables Alice Bob Carol Agent Na Nb Nc Nonce PK Agent PublicKey SK Agent SecretKey InverseKeys PK SK Processes INITIATOR A Na knows PK SK A RESPONDER B Nb knows PK SK B INTRUDER C Nc knows PK SK C Protocol description 0 1 2 3 A B A A B A B B na A PK B na nb PK A nb PK B Formal Analysis of Security Protocols NYU Spring 2003 40 Lecture 6 A Pnueli and L Zuck Data Types and the Initiator Observing the protocol we identify 3 types of messages Consequently we define datatype 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 extended dialect of SPL inspired by the pattern matching constructs of CSP p Agent my nonce his nonce Nonce 0 p B C my nonce if p B then Nab else Nac Alice 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 p Agent my nonce her nonce Nonce m0 media h1 PK B her nonce pi Bob m my nonce if p A then Nba else Nbc 1 m2 media h2 PK p her nonce my noncei m3 media h3 PK B my noncei m4 Formal Analysis of Security Protocols NYU Spring 2003 41 Lecture 6 A Pnueli and L Zuck The Intruder Finally we present the code for the intruder p q Agent n n1 n2 Nonce K set of Nonce where K Nc loop forever do media h1 PK C n pi K K n or media h2 PK C n1 n2i K K n1 n2 or Carol media h3 PK C ni K K n or OR media h1 PK p n qi q Agent n K or media h2 PK p n1 n2i OR n1OR n K 2 p Agent or OR media h3 PK p ni n K Formal Analysis of Security Protocols NYU Spring 2003 42 Lecture 6 A Pnueli and L Zuck Now in SMV Needham Schroeder 3 Revised March 4 03 MODULE main DEFINE ag A 1 ag B 2 ag C 3 Nab 1 Nac 2 Nba 3 Nbc 4 Nc 5 VAR mestype pk f1 f2 K Alice Bob Carol Id 0 3 1 3 1 5 1 5 array 1 5 of boolean process process process process ASSIGN init mestype init K Nab init K Nac init K Nba init K Nbc init K Nc Initiator mestype pk f1 f2 Responder mestype pk f1 f2 Intruder mestype pk f1 f2 K Idle 0 0 0 0 0 1 Formal Analysis of Security Protocols NYU Spring 2003 43 Lecture 6 A Pnueli and L Zuck MODULE Idle MODULE Initiator mestype pk f1 f2 DEFINE ag A 1 ag B 2 ag C 3 Nab 1 Nac 2 Nba 3 Nbc 4 Nc 5 VAR loc p mine his 0 4 1 3 1 5 1 5 ASSIGN init loc 0 next loc case loc 0 loc 1 loc 2 loc 3 1 esac next p case loc 0 1 esac mestype 0 mestype 2 pk 1 f1 mine mestype 0 1 2 3 4 loc next loc 1 ag B ag C p Formal Analysis of Security Protocols NYU Spring 2003 44 Lecture 6 A Pnueli and L Zuck next mine case loc 0 next loc 1 mine next p ag B Nab 1 Nac esac next mestype case loc 1 loc 2 loc 3 1 esac next pk case loc 1 loc 3 1 esac next f1 case loc 1 loc 3 1 esac next f2 case loc 1 1 esac next loc 2 next loc 3 next loc 4 next loc 2 next loc 4 p p pk next loc 2 next loc 4 mine his f1 next loc 2 ag A f2 Formal Analysis of Security Protocols NYU Spring 2003 1 0 3 mestype 45 Lecture 6 next his A Pnueli and L Zuck case loc 2 next loc 3 1 esac Formal Analysis of Security Protocols NYU Spring 2003 f2 his 46 Lecture 6 A Pnueli and L Zuck Responder MODULE Responder mestype pk f1 f2 DEFINE ag A 1 ag B 2 ag C 3 Nab 1 Nac 2 Nba 3 Nbc 4 Nc 5 VAR loc p mine hers 0 3 1 3 1 5 1 5 ASSIGN init loc 0 next loc case loc 0 mestype 1 pk 2 f2 in ag A ag C loc 1 mestype 0 loc 2 mestype 3 pk 2 f1 mine 1 esac next mestype case loc 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 1 2 3 loc 47 Lecture 6 next pk next f1 next f2 next hers A Pnueli and L Zuck case loc 1 1 esac case loc 1 1 esac case loc 1 1 esac case loc 0 1 esac next loc 2 p pk next loc 2 hers f1 next loc 2 mine f2 next loc 1 f1 hers next p case loc 0 next loc 1 f2 4 f2 1 p esac next mine case loc 0 next loc 1 mine next p ag A Nba 1 Nbc esac Formal Analysis of Security Protocols NYU Spring 2003 48 Lecture 6 A Pnueli and L Zuck Intruder MODULE Intruder mestype pk f1 f2 K DEFINE ag A 1 ag B 2 ag C 3 Nab 1 Nac 2 Nba 3 Nbc 4 Nc 5 c1 case c n1 1 c n1 2 c n1 3 c n1 4 1 esac c2 case c n2 1 c n2 2 c n2 3 c n2 4 1 esac K 1 K 2 K 3 K 4 1 2 3 4 5 K 1 K 2 K 3 K 4 1 2 3 4 5 rand agent case c n2 4 c n2 1 1 esac Formal Analysis of Security Protocols NYU Spring 2003 49 Lecture 6 VAR c n1 c n2 spy1 spy2 spy3 reset fake1 fake2 fake3 A Pnueli and L Zuck 1 5 1 5 process process process process process process process Spy1 mestype pk f1 f2 K ag C Spy2 mestype pk f1 f2 K ag C Spy3 mestype pk f1 f2 K ag C Reset mestype Fake 1 mestype pk f1 f2 c1 rand agent Fake 2 mestype pk f1 f2 c1 c2 Fake 3 mestype pk f1 f2 c1 3 MODULE Spy1 mestype pk f1 f2 K ag C DEFINE cond mestype 1 pk ag C VAR update Update cond f1 K MODULE Spy2 mestype pk f1 f2 K …
View Full Document
Unlocking...