Foundations of Computer SecurityLecture 63: Protocol VerificationDr. Bill YoungDepartment of Computer SciencesUniversity of Texas at AustinLecture 63: 1 Protocol VerificationVerification of Cryptographic ProtocolsProtocols can be notoriously difficult to get correct. Flaws havebeen discovered in protocols published many years before.It would be nice to be able to reason formally about protocolcorrectness.How do you characterize what a “spy” can do? We should at leastassume that:the spy can see all messages sent;can compose messages from anything visible to it;can interject messages into the flow.Lecture 63: 2 Protocol VerificationVerificationThere are several major approaches to the verification problem:1Belief logics allow reasoning about what principals within theprotocol should be able to infer from the messages they see.Allows abstract proofs, but may miss some important flaws.2State exploration methods (model checking) treat a protocolas a finite state system and conduct an exhaustive searchchecking that all reachable states are safe.3General-purpose theorem proving uses induction over potentialtraces of protocol execution.We’re only going to cover belief logics.Lecture 63: 3 Protocol VerificationBelief LogicsA belief logic is a formal system for reasoning about beliefs. Anylogic consists of a set of logical operators and rules of inference.One trick is taking a sequence of message exchanges andgenerating a collection of belief statements.You have to postulate some reasonable initial assumptions aboutthe state of knowledge/belief of the principals.Lecture 63: 4 Protocol VerificationLessonsProtocols are crucial to the Internet; it would be great to getthem right.Reasoning rigorously about protocols requires some way offormalizing their behavior and properties.Belief logics is such an approach.Next lecture: The BAN LogicLecture 63: 5 Protocol
View Full Document
Unlocking...