View Full Document


Unformatted text preview:

18739A Foundations of Security and Privacy Logics for Security Protocols Anupam Datta Fall 2007 08 Protocol Analysis Techniques Crypto Protocol Analysis Formal Models Model Checking Protocol Logics Murphi AVISPA BAN PCL Dolev Yao perfect cryptography Computational Models Random oracle Probabilistic process calculi Probabilistic I O automata Process Calculi Inductive Proofs Applied calculus Paulson MSR Inductive Method Pros Cons uAdvantages Reason about infinite runs message spaces Trace model close to protocol specification Can prove protocol correct uDisadvantages Does not always give an answer Failure does not always yield an attack Still trace based properties only Labor intensive Must be comfortable with higher order logic Proofs are very long 4000 steps for Otway Rees session key secrecy Protocol Logics uBAN Logic A Logic of Authentication by Michael Burrows Martin Abadi Roger Needham 1989 uHistorically the first logic for reasoning about security protocols uSyntax and proof system axioms and rules for proving authentication properties semantics added in a later paper BAN Logic 1 uAdvantages Proofs are relatively short 2 3 pages cf Paulson s inductive proofs Proofs follow protocol design intuition cf model checking low level theorem proving Relatively easy to use Still taught widely in security courses No explicit reasoning about traces and intruder cf Paulson s inductive proofs BAN Logic 2 uDisadvantages Not sound wrt now accepted model of protocol execution and attack Protocols proved secure may be insecure e g NS was proved secure using BAN Protocols are modeled using logical formulas idealization step as opposed to state machines or programs Many uses of non standard logical concepts Jurisdiction control belief messages propositions Only authentication properties not secrecy Applicable to restricted classes of protocols See Harper s slides on BAN from 15 819 linked from course web page Today uProtocol Composition Logic PCL Developed over the last few years

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...

Join to view Logics for Security Protocols and access 3M+ class-specific study document.

We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Logics for Security Protocols and access 3M+ class-specific study document.


By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?