BAN logic

   * BAN logic: formal ``proofs'' of security for cryptographic
     authentication protocols.
   * Steps to use BAN logic:
        o Idealize the protocol in the language of the formal logic.
        o Identify your initial security assumptions in the language of BAN
          logic.
        o Use the productions and rules of the logic to deduce new
          predicates.
        o Interpret the statements you've proved by this process. Have you
          reached your goals?
        o (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.