What are Security Protocols?Example: Needham Schroeder SKNSSK: The protocolIn Englishldots A ``more realistic" NSSKNSPK (1978)NSPK: Undesirable RunDiagnosis of a FailureConclusionsWhy are Security Protocols Hard?Case Study: WMFWMF: An Attack on WMFAnother Attack on WMFWoo-Lam ProtocolAnd an AttackWhat About NSSK?StrandsStrand ExampleMessages and TermsSubterms and OriginationBundlesA BundleThe Power of the PenetratorPenetrator's StrandsForming Penetrator's Strand in NSPKFormal AnalysisofSecurity ProtocolsInstructors. Amir Pnueli and Lenore ZuckContact. {amir,zuck}@cs.nyu.eduOffice Hours. Tuesday 4-5Requirements. Attendance; 2-3 assignments;Textbooks. NoneNYU G22.3033-013 – p.1What are Security Protocols?Security Protocols are:short conventional sequences of messagesuse cryptographyThe goals of security protocols include:creating secure channelsagreeing on a new shared secretauthenticationThey are frequently wrongNYU G22.3033-013 – p.2Example: Needham Schroeder SKOne of the earliest protocolsForms the basis of the Kerberos authenticationprotocol;Uses purely symmetric encryption algorithmsEnables A and B to set up a secure channel ofusingTA and B share a private, long-term key with TNYU G22.3033-013 – p.3NSSK: The protocolAA·B·NaI T•wwJ{|B·Na·k·{|k·A|}Kb|}Ka•wwB J{|k·A|}Kb•ww•ww{|Nb|}kI •ww•wwJ{|Nb− 1|}k•wwNYU G22.3033-013 – p.4In English...A informs T she wants to communicate with B andsupplies afresh nonce; Intruder may learn that Awishes to communicate with B but cannot altermessage effectivelyT sends A an encrypted message that includes herrequest, thenew key k, and an encryptedmessage,Tb, to B that includes the new sessionkeykA sends B the encrypted message TbB sends A a fresh nonce encrypted with kA decrements B’s nonce, encrypts it with k andsends it to B (So that the B is assured A generatedmessage)NYU G22.3033-013 – p.5A “more realistic" NSSKAA·B·NaIA·B·NaI T•wwJ{|B·Na·k·Tb|}KaJ{|B·Na·k·Tb|}Ka•wwB JTbJTb•ww•ww{|Nb|}kI{|Nb|}kI •ww•wwJ{|Nb−1|}kJ{|Nb−1|}k•wwWhere Tb= {|k·A|}Kb.NYU G22.3033-013 – p.6NSPK (1978)A{|Na·A|}KBI{|Na·A|}KBI B•wwJ{|Na·Nb|}KAJ{|Na·Nb|}KA•ww•ww{|Nb|}KBI{|Nb|}KBI •wwIntended Run:A{|Na·A|}KBI B•wwJ{|Na·Nb|}KA•ww•ww{|Nb|}KBI •wwNYU G22.3033-013 – p.7NSPK: Undesirable RunA{|Na·A|}KPI P•ww{|Na·A|}KBI B•wwwwwwwwwJ{|Na·Nb|}KA•ww•ww{|Nb|}KPI P•ww{|Nb|}KBI •wwwwwwwwwDue to Gavin Lowe (1995)NYU G22.3033-013 – p.8Diagnosis of a FailureWho was duped?not A— She meant to share Na·Nbwith PB– Thinks he shares Na·Nbonly with ASecrecy failed: P knows valuesAuthentication failed: A had no run with BA offered P a service:gave P nonce Napromised to translate {|Na·N|}KAinto {|N|}KPBut this service was unintended!!(At least not whenN is computed by a legitimateparty andP doesn’t even know it)NYU G22.3033-013 – p.9ConclusionsSecurity Protocols are:short conventional sequences of messagesuse cryptographyThe goals of security protocols include:creating secure channelsagreeing on a new shared secretauthenticationThey are frequently wrongNYU G22.3033-013 – p.10Why are Security Protocols Hard?Attacker chooses pattern of communicationAttacker may also be a playerMay hold keysWill misuse themAttackers manipulate honest playersHonest players play by the rulesBut they may be forced to serve as oraclesProtocol may allow for unindented servicesNYU G22.3033-013 – p.11Case Study: WMFGoals. Establish a session key and authenticate Ato BAssumes A can generate good session keysAssumes clocks are synchronized (so that A’s firstmessage is not replayed)Intended Run:AA·{|τa·B·k|}Ka→ T•ww{|τt·A·k|}Kb→ BNYU G22.3033-013 – p.12WMF: An Attack on WMFIntended Run:AA·{|τa·B·k|}Ka→ T•ww{|τt·A·k|}Kb→ BUnintended Run:AA·{|τa·B·k|}Ka→ TIT{|τa·B·k|}Ka→ •wwNYU G22.3033-013 – p.13Another Attack on WMFIntruder replays messages to obtain highertimestamps:AA·{|τa·B·k|}Ka→ T•ww{|τt·A·k|}Kb→ BZBB·{|τt·A·k|}Kb→ •ww•wwwwwwwwwwwwwwww←{|τ0t·B·k|}Ka•wwZAA·{|τ0t·B·k|}Ka→ •ww•ww{|τ00t·A·k|}Kb→ •wwwwwwwwwwwwwwwwwwwwwwwwNYU G22.3033-013 – p.14Woo-Lam ProtocolGoal. A authenticate to BIntended Run:AA→ B•ww←Nb•ww•ww{|Nb|}Ka→ •ww•ww{|A·{|Nb|}Ka|}Kb→ T•ww←{|Nb|}Kb•wwNYU G22.3033-013 – p.15And an AttackPenetrator Convinces B he’s A:PA→ B•wwM→ •ww•ww←Nb•ww•ww←N0b•ww•ww{|Nb|}Km→ •ww•ww{|Nb|}Km→ •wwB•ww{|A·{|Nb|}Km|}Kb→ T•ww{|M ·{|Nb|}Km|}Kb→ •ww•ww←{|N00b|}Kb•ww•ww←{|Nb|}Kb•wwNYU G22.3033-013 – p.16What About NSSK?It too can be attackedTry to find an attack and fix the protocol so that itwithstands the attackWe’ll present an attack next week that get B tobelieve it has a key withANYU G22.3033-013 – p.17StrandsWe model the behavior of a single participants byastrandA strand consists of a sequence of nodes, eachrepresenting asend or a receive eventNodes representing send events are positiveNodes representing receive events are negativeNodes in a strand are causally related by the =⇒relation (which is acyclic)NYU G22.3033-013 – p.18Strand ExampleIn the NSPK we have for A’s strand:A+{|Na·A|}KB•w−{|Na·Nb|}KA•w+{|Nb|}KBand for B’s strand:• −{|Na·A|}KB•w+{|Na·Nb|}KA•w−{|Nb|}KBNYU G22.3033-013 – p.19Messages and TermsAtomic terms consist ofNames of participants (e.g., A, B, T)NoncesKeystimestampsetc.They form terms and messages usingconcatenation (.) and encryption with keys ({|t|}k)We assume (for now) free algebra over the atomictermsNYU G22.3033-013 – p.20Subterms and OriginationA subterm relation v on terms is the leasttransitive and reflexive relation such thatg, h v g·hand h v {|h|}kNote that k v {|h|}konly if k v hWe denote the set of subterms of the message(sent or received) at noden by TERMS(n).A term t originates at a node n if:n is a positive nodet ∈ TERMS(n)t is not a subterm of any node that ⇒-precedesnNYU G22.3033-013 – p.21BundlesA Bundle is an acyclic finite graph of nodes andedges of two types:=⇒ representing causality−→ representing well-formednessFor every negative node +m in the bundle, theremust be aunique positive node −m such that+m −→ −mFor every node n in a bundle,