# 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.