BAN logic

• BAN logic: formal ``proofs'' of security for cryptographic authentication protocols.
• Steps to use BAN logic:
  • Idealize the protocol in the language of the formal logic.
  • Identify your initial security assumptions in the language of BAN logic.
  • Use the productions and rules of the logic to deduce new predicates.
  • Interpret the statements you've proved by this process. Have you reached your goals?
  • (optional:) Trim unnecessary fat from the protocol, and repeat.
• BAN logic is primarily concerned with the beliefs of principals (more precisely, abstract statements that principals are reasonably entitled to believe or ought to believe).
• The actual details of the logic are pretty boring, and not so important to learn unless you're actually going to design a cryptographic protocol (!), I think.
• BAN logic cannot really prove the security of a protocol; it can only catch certain kinds of subtle errors, help us to reason about the protocol, and help us identify and formalize our assumptions & analysis.
• The BAN logic work spurred a whole slew of papers on the subject: some pointed out limitations of the logic, while others extended it, automated it, or applied it.
• This is, in the end, a huge success for formal methods in cryptography, I think. Most of the theoretical formal techniques of CS (such as computational complexity) haven't been very helpful in practical applications of cryptography, unfortunately. As a useful formal tool for practical protocol design, BAN logic is a welcome exception.