Design and Analysis of Security ProtocolsCourse LogisticsGradingComputer SecurityClass PollSecurity ProtocolsCorrectness vs SecuritySecurity AnalysisTheme #1: Protocols and PropertiesTheme #2: Formal Analysis MethodsVariety of Tools and TechniquesExample: Needham-SchroederNeedham-Schroeder Public-Key ProtocolWhat Does This Protocol Achieve?Anomaly in Needham-SchroederLessons of Needham-SchroederImportant Modeling DecisionsFundamental TradeoffExplicit Intruder MethodMurj [Dill et al.]Making the Model FiniteApplying Murj to Security ProtocolsNeedham-Schroeder in Murj (1)Needham-Schroeder in Murj (2)Needham-Schroeder in Murj (3)Try Playing With MurjStart Thinking About the ProjectSome IdeasWatch This SpaceDesign and Analysis of Security Protocols Vitaly ShmatikovCS 395Thttp://www.cs.utexas.edu/~shmat/courses/cs395t_fall04/Course LogisticsLectures•Monday, Wednesday 3:30-5pm •Project presentations in the last two weeksThis is a project course•The best way to understand security is by getting your hands dirty •There will be one short homework and one read-and-present a research paper assignment•Most of your work will be project, writeup and in-class presentation Please enroll!GradingHomework: 10%Read and present a research paper: 15%Project: 75%•Projects are best done individually•Two-person teams are Ok, but talk to me first•Project proposal due around 5th week of the course–More details later•I’ll provide a list of potential project ideas, but don’t hesitate to propose your ownComputer SecurityCryptographic primitivesProtocols and policiesImplementationBuilding blocksBlueprintsSystemsAlgorithmicnumber theoryComputationalcomplexityRSA, DSS, SHA-1…SSL, IPSec, access control…Firewalls, intrusiondetection…Class PollCryptography?•Public-key and symmetric encryption, digital signatures, cryptographic hash, random-number generators?•Computational complexity?Systems security?•Buffer overflows, Web security, sandboxing, firewalls, denial of service?Formal methods and verification?•Model checking, theorem proving?… this course doesn’t require any of these Security ProtocolsThe focus of this course is on secure communications…•Two or more parties•Communication over insecure network•Cryptography used to achieve some goal–Exchange secret keys, verify identity, pay for a service……and formal analysis techniques for security •Analyze protocol design assuming cryptography, implementation, underlying OS are correctLater in the course will talk about privacy protection in databases and trusted computingCorrectness vs SecurityProgram or system correctness: program satisfies specification•For reasonable input, get reasonable outputProgram or system security: program properties preserved in face of attack•For unreasonable input, output not completely disastrousMain differences•Active interference from adversary•Refinement techniques may fail–Abstraction is very difficult to achieve in security: what if the adversary operates below your level of abstraction?Security AnalysisModel systemModel adversaryIdentify security propertiesSee if properties preserved under attackResult•Under given assumptions about system, no attack of a certain form will destroy specified properties•There is no “absolute” securityTheme #1: there are manynotions of what it meansfor a protocol to be “secure”Theme #2: there are manyways of looking for security flawsTheme #1: Protocols and PropertiesAuthentication•Needham-Schroeder, KerberosKey establishment•SSL/TLS, IPSec protocols (IKE, JFK, IKEv2)Secure group protocols•Group Diffie-Hellman, CLIQUES, key trees and graphsAnonymity•MIX, Onion routing, Mixmaster and MixminionElectronic payments, wireless security, fair exchange, privacy…Some of these are excellenttopics for a project orthe paper-reading assignmentTheme #2: Formal Analysis MethodsFocus on special-purpose security applications•Some techniques are very different from those used in hardware verification•In all cases, the main difficulty is modeling the attackerSimple, mechanical models of the attackerNo cryptanalysis!•In this course, we’ll assume that cryptography is perfect•Search for design flaws, not cryptographic attacksWe’ll talk about the relationship between formal and cryptographic models late in the courseVariety of Tools and TechniquesExplicit finite-state checking•Mur model checker•There will be a small homework!Infinite-state symbolic model checking•SRI constraint solverProcess algebras•Applied pi-calculus• Secrecy• Authentication• AuthorizationProbabilistic model checking•PRISM probabilistic model checker• AnonymityGame-based verification•MOCHA model checker• FairnessExample: Needham-SchroederVery (in)famous example•Appeared in a 1979 paper•Goal: authentication in a network of workstations•In 1995, Gavin Lowe discovered unintended property while preparing formal analysis using FDR systemBackground: public-key cryptography•Every agent A has a key pair Ka, Ka-1•Everybody knows public key Ka and can encrypt messages to A with it (we’ll use {m}Ka notation)•Only A knows secret key Ka-1, therefore, only A can decrypt messages encrypted with KaA’s reasoning:• The only person who could know NonceA is the person who decrypted 1st message• Only B can decrypt message encrypted with Kb• Therefore, B is on the other end of the line B is authenticated! Needham-Schroeder Public-Key ProtocolA BA’s identityFresh random numbergenerated by AB’s reasoning:• The only way to learn NonceB is to decrypt 2nd message• Only A can decrypt 2nd message• Therefore, A is on the other endA is authenticated! Kb{ NonceB}Ka{ NonceA, NonceB }Kb{ A, NonceA }What Does This Protocol Achieve?A BKb{ NonceB}Ka{ NonceA, NonceB }Kb{ A, NonceA }Protocol aims to provide both authentication and secrecyAfter this the exchange, only A and B know Na and NbNa and Nb can be used to derive a shared keyB can’t decrypt this message,but he can replay itAnomaly in Needham-SchroederA B{ A, Na }KcC{ A, Na }Kb{ Na, Nc }Ka{ Na, Nc }Ka{ Nc }KbEvil agent B trickshonest A into revealingC’s private value NcC is convinced that he is talking to A![published by Lowe]Evil B pretendsthat he is ALessons of Needham-SchroederClassic man-in-the-middle attackExploits participants’ reasoning
View Full Document
Unlocking...