Burrows–Abadi–Needham logic is a set of rules for defining and analyzing information exchangeprotocols. Specifically, BAN logic helps its users determine whether exchanged information is trustworthy, secured against eavesdropping, or both. BAN logic starts with the assumption that all information exchanges happen on media vulnerable to tampering and public monitoring. This has evolved into the popular security mantra, "Don't trust the network." A typical BAN logic sequence includes three steps:
BAN logic uses postulates and definitions – like all axiomatic systems – to analyze authentication protocols. Use of the BAN logic often accompanies a security protocol notation formulation of a protocol and is sometimes given in papers.
Language type
BAN logic, and logics in the same family, are decidable: there exists an algorithm taking BAN hypotheses and a purported conclusion, and that answers whether or not the conclusion is derivable from the hypotheses. The proposed algorithms use a variant of magic sets.
Alternatives and criticism
BAN logic inspired many other similar formalisms, such as GNY logic. Some of these try to repair one weakness of BAN logic: the lack of a good semantics with a clear meaning in terms of knowledge and possible universes. However, starting in the mid-1990s, crypto protocols were analyzed in operational models using model checkers, and numerous bugs were found in protocols that were "verified" with BAN logic and related formalisms. In some cases a protocol was reasoned as secure by the BAN analysis but where in fact insecure. This has led to the abandonment of BAN-family logics in favor of proof methods based on standard invariance reasoning.
Basic rules
The definitions and their implications are below :
P believes X: P acts as if X is true, and may assert X in other messages.
P has jurisdiction over X: P's beliefs about X should be trusted.
P said X: At one time, P transmitted message X, although P might no longer believeX.
P sees X: P receives message X, and can read and repeat X.
K: X is encrypted with key K.
fresh: X has not previously been sent in any message.
The meaning of these definitions is captured in a series of postulates:
If P believes key, and P sees K, then P believes
If P believes and P believes fresh, then P believes.
P must believe that X is fresh here. If X is not known to be fresh, then it might be an obsolete message, replayed by an attacker.
If P believes and P believes, then P believes X
There are several other technical postulates having to do with composition of messages. For example, if P believes that Q said <X, Y>, the concatenation of X and Y, then P also believes that Q said X, and P also believes that Q said Y.
Using this notation, the assumptions behind an authentication protocol can be formalized. Using the postulates, one can prove that certain agents believe that they can communicate using certain keys. If the proof fails, the point of failure usually suggests an attack which compromises the protocol.
A very simple protocol — the Wide Mouth Frog protocol — allows two agents, A and B, to establish secure communications, using a trusted authentication server, S, and synchronized clocks all around. Using standard notation the protocol can be specified as follows: Agents A and B are equipped with keys Kas and Kbs, respectively, for communicating securely with S. So we have assumptions: Agent A wants to initiate a secure conversation with B. It therefore invents a key, Kab, which it will use to communicate with B. A believes that this key is secure, since it made up the key itself: B is willing to accept this key, as long as it is sure that it came from A: Moreover, B is willing to trust S to accurately relay keys from A: That is, if B believes that S believes that A wants to use a particular key to communicate with B, then B will trust S and believe it also. The goal is to have A reads the clock, obtaining the current time t, and sends the following message: That is, it sends its chosen session key and the current time to S, encrypted with its private authentication server key Kas. Since S believes that key, and S sees Kas, then S concludes that A actually said. Since the clocks are synchronized, we can assume Since S believes fresh and S believes A said, S believes that A actually believes that key. S then forwards the key to B: Because message 2 is encrypted with Kbs, and B believes key, B now believes that S said. Because the clocks are synchronized, B believes fresh, and so fresh. Because B believes that S's statement is fresh, B believes that S believes that . Because B believes that S is authoritative about what A believes, B believes that. Because B believes that A is authoritative about session keys between A and B, B believes key. B can now contact A directly, using Kab as a secret session key. Now let's suppose that we abandon the assumption that the clocks are synchronized. In that case, S gets message 1 from A with, but it can no longer conclude that t is fresh. It knows that A sent this message at some time in the past but not that this is a recent message, so S doesn't believe that A necessarily wants to continue to use the key Kab. This points directly at an attack on the protocol: An attacker who can capture messages can guess one of the old session keys Kab. The attacker then replays the old message, sending it to S. If the clocks aren't synchronized, S might believe this old message and request that B use the old, compromised key over again. The original Logic of Authentication paper contains this example and many others, including analyses of the Kerberos handshake protocol, and two versions of the Andrew Project RPC handshake.
