BAN Logic

Origin. Michael Burrows, Martín Abadi, and Roger Needham, "A logic of authentication". The publication trail: DEC SRC Research Report 39 (February 1989, revised February 1990); Proceedings of the Royal Society of London A 426 (1989), 233–271; SOSP 1989, 1–13; ACM Transactions on Computer Systems 8(1) (1990), 18–36. Its analyses found weaknesses in published protocols, X.509 and the Andrew handshake among them.

Models. Belief, not truth, and authentication, not secrecy. A protocol is idealized into formulas; each principal's beliefs accumulate as messages arrive; the authentication goal is a belief about a key — A ∣≡ A ↔K B, B ∣≡ A ↔K B, and ideally each principal's belief that the other believes it. The annotation runs like a proof in Hoare Logic, the paper's own comparison, with initial assumptions in place of preconditions and final beliefs in place of postconditions. What the method surfaces is assumptions: a protocol flaw appears as a premise the derivation cannot do without and nothing in the protocol justifies.

Formalism.

Language: positive formulas only — no negation, no disjunction. P ∣≡ X: P believes X. P ◁ X: P sees X — a message containing X arrived, readable by P. P ∣∼ X: P once said X — at some time, past or present. P ⇒ X: P has jurisdiction over X — P is an authority on X. #(X): X is fresh — never sent in a message before the current run. P ↔K Q: K is a good key for P and Q — known only to P, Q, and principals they trust. ↦K P: K is P's public key; the matching secret key is K⁻¹. P ⇌Y Q: Y is a secret shared by P and Q, usable to prove identity. {X}K: X encrypted under K. ⟨X⟩Y: X uttered together with the secret Y.

Idealization: each concrete message becomes a formula stating what the message is meant to convey; cleartext parts are dropped, since they yield no beliefs. The idealized protocol is annotated with assertions, and the rules drive the derivation from initial assumptions to final beliefs.

Message meaning — from seeing to once-said:

P ∣≡ Q ↔K P P ◁ {X}K ───────────────────────── P ∣≡ Q ∣∼ X

Sound because {X}K carries its sender and a principal recognizes its own messages. Variants for public keys (from P ∣≡ ↦K Q and P ◁ {X}K⁻¹) and for shared secrets (from P ∣≡ Q ⇌Y P and P ◁ ⟨X⟩Y).

Nonce verification — from once-said to believes:

P ∣≡ #(X) P ∣≡ Q ∣∼ X ─────────────────────────── P ∣≡ Q ∣≡ X

The only rule that promotes ∣∼ to ∣≡; X must contain no encrypted part. The abstract form of challenge and response.

Jurisdiction — from another's belief to one's own:

P ∣≡ Q ⇒ X P ∣≡ Q ∣≡ X ──────────────────────────── P ∣≡ X

Freshness propagation:

P ∣≡ #(X) ─────────────── P ∣≡ #(X, Y)

What the analyses found (1989–90): Needham–Schroeder shared-key (1978): B reaches B ∣≡ A ↔Kab B only through the assumption B ∣≡ #(A ↔Kab B), which the paper calls dubious — nothing in the protocol gives B evidence the key is new. The premise is the replay weakness Denning and Sacco published in 1981, now explicit. Andrew Secure RPC handshake: nothing in the final message is fresh to A, so an intruder can replay an old, possibly compromised session key; the fix adds A's nonce to that message. CCITT X.509: two weaknesses, one found during idealization, one during derivation. Data signed after encryption gives no evidence the signer knows it — the fix is to sign before encrypting; and if the timestamp Ta goes unchecked, the nonce Nb fails to link the third message to the first, so an intruder can replay an old message of A's. Yahalom: the nonce Nb functions as a shared secret, which the protocol's designer had not noticed. Needham–Schroeder public-key: each principal must assume the certificate carrying the other's public key is fresh; timestamps resolve it.

Symbols.

Metatheory. The report closes with a semantics of its own, but the one with standing is Martín Abadi and Mark Tuttle, "A semantics for a logic of authentication" (PODC 1991, 201–216): a possible-worlds model over protocol runs in which belief is resource-bounded, defeasible knowledge, with a reformulated rule set sound for it. Their reconstruction located two soft points. The good-key definition demands secrecy, yet the soundness of message meaning needs only that P and Q alone encrypt with K — who else discovers K is irrelevant to the rule; and the promotion of saying to believing relies on an implicit honesty assumption — principals believe what they say — which Abadi and Tuttle argue is not well defined, and which their reformulation removes. Gong, Needham, and Yahalom, "Reasoning about belief in cryptographic protocols" (IEEE Symposium on Security and Privacy 1990, 234–248), extended the logic in the same direction; Abadi and Tuttle record it as the more complicated sibling of their own reformulation. Dan Nessett, "A critique of the Burrows, Abadi and Needham logic" (Operating Systems Review 24(2), 1990, 35–38), gave the two-message protocol A → B: {Na, Kab}Ka⁻¹, B → A: {Nb}Kab, in which A publishes the session key by signing it, and derived all the usual BAN goals for it; the rejoinder (same issue, 39–40) answers that the premise A ∣≡ A ↔Kab B is inconsistent with the paper's stated scope, and that no logic protects against false premises. Both are right, and that is the finding: the verdicts are sound relative to premises the logic cannot audit. There is no computational soundness — encryption is a symbolic constructor, and the reconciliation of the symbolic and computational views began with Abadi and Rogaway, "Reconciling two views of cryptography (the computational soundness of formal encryption)" (Journal of Cryptology 15, 2002, 103–127), for the symbolic model the field had meanwhile adopted: Dolev and Yao's ("On the security of public key protocols", IEEE Transactions on Information Theory 29, 1983, 198–208), an active intruder who reads, blocks, and composes every message. On that model the field moved to process calculi: the spi calculus of Abadi and Gordon ("A calculus for cryptographic protocols: The spi calculus", CCS 1997, 36–47; Information and Computation 148, 1999, 1–70) extends the Pi Calculus with cryptographic primitives, represents protocols as processes, and states security properties as process equivalences.

Applies to. Authentication protocol analysis — Needham–Schroeder, Kerberos, Otway–Rees, Yahalom, Andrew RPC, X.509, as in the original paper. The successor belief logics, GNY among them. Teaching protocol failure. The predecessor of the symbolic methods — Dolev–Yao model checking and the spi calculus (Pi Calculus) — and, for knowledge-based alternatives, Epistemic Logic and Epistemic Temporal Logic.

Limitations. The verdict is relative to the idealization, and idealization has no rules: the step from concrete messages to formulas is where the analyst's judgment enters, and one of the X.509 weaknesses was found during that step rather than by the calculus. Secrecy is outside the scope by the paper's own statement — no attempt to detect weaknesses of encryption schemes or unauthorized release of secrets — and Nessett's counterexample exercises exactly this: a protocol that publishes its session key still supports a derivation of every BAN goal, since the logic addresses who has a key and never who must not have it. There is no intruder in the model: the paper declines to treat authentication of untrustworthy principals, and the man-in-the-middle attack Gavin Lowe found on the Needham–Schroeder public-key protocol ("An attack on the Needham-Schroeder public-key authentication protocol", Information Processing Letters 56, 1995, 131–133) lives precisely in the active-intruder model the logic excludes — the BAN analysis of that protocol ends in the intended beliefs. The language has no negation, so nothing can be disbelieved and no statement made that a principal fails to know something; beliefs only accumulate, within a single run. And the belief operator answers to no independent standard: the original paper's semantics is, by Abadi and Tuttle's assessment, hard to relate to standard models of computation and belief, and their soundness theorem covers their reformulation, not the original rules.

© 2026 Lingenic LLC