Lecture 4 A. Pnueli and L. ZuckApplying Formal Methods to Analysis of Security ProtocolsThe principles are quite straightforward:• Model the pariticipants in the protocol, including the Intruder, as processes ina reactive concurrent system.• Formulate the security goals as a specification the systems should satisfy.• Apply available verification techniques, i.e., model checking and deductiveverification, to establish that the protocol meets its goals or, alternately, toidentify counter-examples which should be interpreted as successful attacks onthe protocol.This approach is based on the reduction of the security problem to a generalverification problem of reactive systems.As is often the case, success largely depends on the details of the reduction.Formal Analysis of Security Protocols, NYU, Spring, 2003 1Lecture 4 A. Pnueli and L. ZuckIn View of this ReductionWe have as many different suggestions for formal analysis of security as there aredifferent models forconcurrency, specifications of reactive systems, and differentverification methods.Among these approaches, we find methods based onCSP, CCS, Petri-Nets, LTL,CTL, IO-Automata, ASM, Logics of Knowledge, Linear Logic.We will rely in part on a textbook:Modelling and Analysis of Security Protocolsby P. Ryan and S. Schneider from Addison Wesley. This book is based on theconcurrency model ofCSP language and its implementation by the FDR modelchecker.Following the organization of this text, we will try to develop our own version,based on appropriate extensions ofSPL and the TLV model checker.Formal Analysis of Security Protocols, NYU, Spring, 2003 2Lecture 4 A. Pnueli and L. ZuckExample: The Yahalom ProtocolConsider the following protocol:AA · Na{|A · K|}KBJ· {|Nb|}K{|B · K · Na· Nb|}KAJ· {|A · K|}KBJBB · {|A · Na· Nb|}KBJJThe protocol is believed to be correct, but its verification is far from trivial. Thehardest part is to prove thatNbremains secret.Formal Analysis of Security Protocols, NYU, Spring, 2003 3Lecture 4 A. Pnueli and L. ZuckMessage Passing in SPLIn addition to communication by shared variables, SPL also provides the alternatemechanism ofmessage passing. We allow three types of channels, distinguished bytheir declarations:hidentifieri: channel of htypei — Synchronous message passing.Zero buffering. Both sender and receiver are blocked until both are ready.hidentifieri: channel[1..N ] of htypei — Asynchronous message passing.Bounded buffering up to size N. Sender is blocked on a full buffer.Receiver is blocked on an empty buffer.hidentifieri: channel[1..] of htypei — Asynchronous message passing withunbounded buffering. Sender is never blocked.Receiver is blocked on an empty buffer.Commands:α ⇐ e — Send the value of expression e on channel α.α ⇒ x — Receive a message from channel α and store it in variable x.Formal Analysis of Security Protocols, NYU, Spring, 2003 4Lecture 4 A. Pnueli and L. ZuckExample: Mutual Exclusion with Message PassingP1P2Aαβα, β : channel[1..] of booleanP1::loop forever do`0: noncritical`1: α ⇒`2: critical`3: β ⇐ 1P2::loop forever dom0: noncriticalm1: α ⇒m2: criticalm3: β ⇐ 1A ::loop forever dok0: α ⇐ 1k1: β ⇒Formal Analysis of Security Protocols, NYU, Spring, 2003 5Lecture 4 A. Pnueli and L. ZuckThe fds Semantics of Message PassingConsider first the semantics of asynchronous message passing, where the channelhas a buffer boundN, 0 < N ≤ ∞. We assume that channel α is implemented asalist of messages.• The statement S = [α ⇒ x] in process Picontributes the disjunctπi= pre(S) ∧ π0i= post(S) ∧ |α| > 0 ∧(x0, α0) = (hd(α), tl (α)) ∧ pres (V − {πi, x, α})to the transition relation, and the compassion requirement(πi= pre(S) ∧ |α| > 0, πi= post (S))•The statement S = [α ⇐ e] in process Picontributes the disjunctπi= pre(S) ∧ π0i= post(S) ∧ |α| < N ∧ α0= α • e ∧ pres(V − {πi, α})to the transition relation, and the compassion requirement(πi= pre(S) ∧ |α| < N, πi= post(S))Formal Analysis of Security Protocols, NYU, Spring, 2003 6Lecture 4 A. Pnueli and L. ZuckSynchronous Message PassingLet α be a synchronous channe, i.e. declared as α: channel of . . ..Every pair of statmentsSi= [α ⇐ e] in process Piand Sj= [α ⇒ x] in processPj, where i 6= j contributes the disjunctπi= pre(Si) ∧ πj= pre(Sj) ∧ π0i= post (Si) ∧ π0j= post(Sj)∧ x0= e ∧ pres (V − {πi, πj, x})to the transition relation, and the compassion requirement(πi= pre(Si) ∧ πj= pre(Sj), πi= post(Si) ∧ πj= post(Sj))to the compassion set.Formal Analysis of Security Protocols, NYU, Spring, 2003 7Lecture 4 A. Pnueli and L. ZuckThe Needham Schroeder Public Key ProtocolFollowing is a diagram for the NSPK protocol.A B{|Na· A|}KBB · {|Na· Nb|}KA{|Nb|}KBFormal Analysis of Security Protocols, NYU, Spring, 2003 8Lecture 4 A. Pnueli and L. ZuckRepresentation in CasperThe system endorsed inModelling and Analysis of Security Protocolsby P. Ryan and S. Schneider from Addison Wesley. Consists of two components:1. A compiler, calledCasper which accepts as input an abstract (yet more detailed)description of the protocol and participants, and translates it into theCSPlanguage.2. The FDR2 (Failures-Divergence Refinement Ver. 2) model checker which checkswhether one finite-stateCSP system refines another.We found theCasper input language a very useful vehicle for describing securityprotocols. We will illustrate its use on theNSPK protocol.Formal Analysis of Security Protocols, NYU, Spring, 2003 9Lecture 4 A. Pnueli and L. ZuckNSPK Protocol in Casper#Free variablesA, B : Agentna, nb : NoncePK : Agent -> PublicKeySK : Agent -> SecretKeyInverseKeys = (PK, SK)#ProcessesINITIATOR(A,na) knows PK, SK(A)RESPONDER(B,nb) knows PK, SK(B)#Protocol description0. -> A : B1. A -> B : {na, A}{PK(B)}2. B -> A : {na, nb}{PK(A)}3. A -> B : {nb}{PK(B)}#SpecificationSecret(A, na, [B])Secret(B, nb, [A])Agreement(A,B,[na,nb])Agreement(B,A,[na,nb])Formal Analysis of Security Protocols, NYU, Spring, 2003 10Lecture 4 A. Pnueli and L. Zuck#Actual variablesAlice, Bob, Mallory : AgentNa, Nb, Nm : Nonce#Functionssymbolic PK, SK#SystemINITIATOR(Alice, Na)RESPONDER(Bob, Nb)#Intruder InformationIntruder = MalloryIntruderKnowledge = {Alice, Bob, Mallory, Nm, PK, SK(Mallory)}Formal Analysis of Security