BAN Logic

The belief logic of Burrows, Abadi & Needham (1990) for analysing cryptographic authentication protocols. A small modal language with operators P believes X, P sees X, P said X, P controls X, fresh(X), P shares K with Q. Inference rules (message-meaning, nonce-verification, jurisdiction) propagate beliefs as messages are received and decrypted. Verification proceeds by idealising the protocol, stating initial beliefs, and deriving the goal beliefs (typically: authenticated session-key agreement). The first widely-adopted formal method for protocol analysis; superseded by Spi Calculus / ProVerif for rigorous use, but still pedagogically dominant.

In this vault

Backlinks

Linked Pages

Mentalistic Semantics

ACL semantics in which each message commits the sender’s (and sometimes receiver’s) beliefs and intentions — powerful but unverifiable from outside.

In this vault

Needham-Schroeder Protocol

The 1978 authentication protocol family of Needham & Schroeder. Symmetric-key version uses a trusted authentication server holding long-term keys for all principals; basis of Kerberos. Public-key version uses three messages and two nonces between the principals directly. Famous as the canonical case-study for cryptographic-protocol verification: Lowe (1995/1996) found a man-in-the-middle attack on the public-key version using FDR model-checking, 17 years after publication, with a one-line fix (include responder’s identity in message 2). The story launched the modern protocol-verification field.

In this vault

Dolev-Yao Model

The standard symbolic threat model for cryptographic-protocol analysis (Dolev & Yao 1983). The attacker controls the network entirely: it can intercept, drop, modify, and inject any message; it can compose and decompose terms it observes; but it cannot break cryptographic primitives — encryption is a perfect black box. Treats messages as terms in a free algebra modulo cryptographic equations rather than as bit strings. Both BAN Logic and Spi Calculus (and ProVerif / Tamarin) adopt the Dolev-Yao threat model.

In this vault

Spi Calculus

Abadi & Gordon’s (1997) extension of the Pi-Calculus with cryptographic primitives — encryption, decryption, hashing, pairing, name-equality. Security properties (authentication, secrecy) are formalised as process equivalences: a protocol is secure iff no spi-calculus context can distinguish it from an idealised specification. The most general attacker is just an arbitrary spi process. Foundation under ProVerif / Tamarin and the applied π-calculus (Abadi & Fournet 2001).

In this vault

Crypto Protocol Verification

The formal analysis of cryptographic protocols for properties such as authentication, secrecy, key agreement, forward secrecy, and resistance to replay. Two principal traditions:

Belief-logic / symbolic — BAN Logic (Burrows, Abadi & Needham 1990) and successors (GNY, SVO): reason about agents’ beliefs as a protocol unfolds. Diagnostic; not always sound for arbitrary attackers.
Process-calculus / equivalence-based — Spi Calculus (Abadi & Gordon 1997), applied π-calculus, and the modern symbolic provers (ProVerif, Tamarin): security as observational equivalence under an arbitrary attacker context. Sound, automatable for restricted fragments.

Recent industrial use: TLS 1.3, Signal, EAP, FIDO/WebAuthn, post-quantum protocols all have machine-checked symbolic analyses by Tamarin and/or ProVerif.

In this vault

A Logic of Authentication

Reference: Burrows, M., Abadi, M. & Needham, R. (1990). A Logic of Authentication. ACM Transactions on Computer Systems, 8(1), pp. 18–36. (Earlier DEC SRC Research Report 39, 1989.) ACM DOI · Open access PDF (Stanford)

Summary

Burrows, Abadi and Needham introduce BAN logic — a belief logic for reasoning about the authentication properties of cryptographic protocols. The setting is the symbolic Dolev-Yao world: principals communicate by exchanging cryptographic messages over an untrusted network. BAN provides a small modal language whose primary modality is P believes X (“principal P believes X”) together with auxiliary operators (P sees X, P said X, P controls X, fresh(X), P has K, K is shared between P and Q). Its inference rules (the message-meaning rule, nonce-verification rule, jurisdiction rule, freshness rule, etc.) capture how beliefs propagate as messages are received and decrypted — for instance, if P believes K is a key shared with Q and P sees {X}_K and P believes X is fresh, then P may conclude that Q recently sent X. Verification proceeds by idealising the protocol (replacing each message by the abstract belief-statement it is intended to convey), making explicit assumptions about initial beliefs, and then deriving the goal beliefs (typically, that the principals share a fresh authenticated session key). The paper analyses Kerberos, the original Needham-Schroeder protocol, the Andrew Secure RPC handshake, and several others — finding errors and clarifying intended semantics. BAN was a watershed: the first widely-adopted formal method for authentication-protocol analysis. Its limitations (no explicit attacker model, the idealisation step is informal, soundness is debatable for unintended uses) drove the development of more rigorous frameworks — notably the Spi Calculus (process-calculus equivalence-based) and the symbolic provers ProVerif / Tamarin — but the belief-logic style remains in widespread teaching use as the most intuitive entry to protocol verification.

Key Ideas

Belief modalities: P |≡ X (P believes X), P ⊲ X (P sees / receives X), P |~ X (P once said X), P ⇒ X (P has jurisdiction over X — i.e. is an authority on it).
Cryptographic primitives appear in formulas: {X}_K (X encrypted with K), <X>_Y (X with secret Y), (X, Y) (concatenation), with associated extraction rules.
Inference rules as belief-derivation: e.g. message-meaning — if P believes K is shared with Q and sees {X}_K, then P believes Q once said X. Nonce-verification — if P believes Q once said X and P believes X is fresh, then P believes Q currently believes X. Jurisdiction — if P believes Q controls X and P believes Q believes X, then P believes X.
Idealisation: each protocol message is rewritten into an abstract form that makes its intended belief-meaning explicit (typically, the protocol designer has to do this — and the soundness of the analysis depends on the idealisation being faithful).
Goal beliefs: an authentication protocol is correct (in BAN) iff the participants reach the intended mutual beliefs about a fresh session key (P |≡ P ↔K Q, Q |≡ P ↔K Q, often with belief-about-belief: P |≡ Q |≡ P ↔K Q).
Found bugs in real protocols: BAN-style analysis of Needham-Schroeder shared-key protocol revealed that one party could not prove freshness of a session key — the bug Lowe later exploited symbolically.

Connections

Conceptual Contribution

Claim: Authentication properties of cryptographic protocols can be derived in a small modal belief logic whose inference rules capture how beliefs propagate when messages are received and decrypted; verifying a protocol becomes (i) idealising it as a sequence of abstract belief-statements, (ii) stating initial beliefs, and (iii) deriving the goal beliefs. This is rigorous enough to find real bugs in deployed protocols.
Mechanism: Modal language with believes / sees / said / controls / fresh / shares-key operators; ~20 inference rules covering message-meaning, nonce-verification, jurisdiction, freshness, and decomposition; idealisation step from concrete protocol messages to belief-statements; standard goal beliefs for authentication and key establishment.
Concepts introduced/used: BAN Logic, Belief Modality, Idealisation (of protocols), Nonce-Verification Rule, Jurisdiction Rule, Crypto Protocol Verification, Mentalistic Semantics (in the cryptographic setting).
Stance: foundational technical paper — the first widely-adopted formal method for cryptographic-protocol analysis.
Relates to: Conceptually parallel to the mentalistic-semantics family in the ACL literature (KQML, FIPA-ACL) — both treat communication as belief-update under explicit modal operators. BAN is exactly what one gets if one specialises mentalistic ACL semantics to cryptographic-protocol exchanges. The critique that struck mentalistic ACLs (Singh’s argument that beliefs cannot be observed by third parties) hits BAN in the same way: the idealisation step is informal, and “soundness” presupposes the very mental-state assumptions one cannot verify externally. The Spi Calculus (Abadi & Gordon 1997) is BAN’s process-calculus counterpoint — equivalence-based rather than belief-based, with the attacker built in as an arbitrary context. The Lowe attack on Needham-Schroeder, derivable from a careful BAN analysis but missed by the original 1978 informal argument, is the canonical worked example demonstrating why formal protocol verification matters and why even rigorous methods need more rigorous successors. BAN’s belief modalities also share semantic ground with Halpern & Moses 1990 — both apply epistemic logic to distributed/multi-agent systems, with BAN specialising to authentication and Halpern–Moses staying general.