Burrows-Abadi-Needham logic

Burrows-Abadi-Needham logic (also known as the BAN logic) uses postulates

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

and definitions -- like all axiomatic systems -- to analyze

Related Topics:
Definition - Axiomatic system

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

authentication protocols. Use of the BAN logic often accompanies a security protocol notation formulation of a protocol and is sometimes given in papers.

Related Topics:
Authentication - Protocols - Security protocol notation

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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 (Monniaux, 1999).

Related Topics:
Decidable - Magic set

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The definitions and their implications are below (P and Q are network agents, X is a message,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

and K is an encryption key):

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• 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 (and believed) message X, although P might no longer believe X.
• P sees X: P receives message X, and can read and repeat X.
• {X}_K: X is encrypted with key K.
• fresh(X): X was sent recently.
• key(K, P<->Q): P and Q may communicate with shared key K

The meaning of these definitions is captured in a series of postulates:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• If P believes key(K, P<->Q), and P sees {X}_K, then P believes (Q said X)
• If P believes (Q said X) and P believes fresh(X), then P believes (Q believes X).

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 (Q has jurisdiction over X) and P believes (Q believes X), 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 >, 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.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

 
Burrows-Abadi-Needham logic: The Wide Mouth Frog protocol ►