Burrows–Abadi–Needham Logic¶
A formal authentication-belief calculus derives what protocol principals may believe from idealized messages, explicit trust and freshness premises, and named inference postulates.
Core Idea¶
Burrows–Abadi–Needham (BAN) logic is a formal way to reason about what participants in an authentication protocol may believe. It gives names to statements such as “A believes X,” “B once said X,” and “X is fresh,” then applies stated inference rules to idealized messages and explicit assumptions about keys and trusted authorities. A claimed belief follows only when its proof uses the declared rules and premises.[^ref-b7cbdbc06b3a]
The logic itself is a fixed set of symbols and rules. Applying it to a real message exchange requires an analyst to translate messages into those symbols and justify the starting beliefs. A valid proof is conditional on that translation and those assumptions; it is not by itself a proof that an implementation is secure.[^ref-b7cbdbc06b3a]
Scope of Application¶
Use BAN logic to examine whether an authentication or key-establishment protocol gives its participants grounds for intended beliefs about one another and about a session key. State the protocol version, who sends and receives each message, what each party can read, the idealized messages, trusted keys and authorities, freshness evidence, and the goal to be proved. Changing any of those inputs can change the conclusion.[^ref-b7cbdbc06b3a]
The original authors apply it to Kerberos, which uses a server and timestamps, and to an early Andrew Secure RPC handshake, which uses nonces. The analysis concerns those represented versions and assumptions, not every later deployment of either protocol.[^ref-b7cbdbc06b3a]
Clarity¶
Keep “said” and “believes” separate. “B said X” allows that B uttered X in a past run. A freshness premise plus the nonce-verification rule may support the stronger claim that B currently believes X. A jurisdiction premise is needed before A can adopt B's belief as its own. A proof must show each step and satisfy each rule's conditions.[^ref-b7cbdbc06b3a]
The translation step matters just as much. An encrypted packet does not literally say in ordinary language that a key is good. The analyst must explain why the fields a recipient can read and authenticate warrant that idealized assertion. Otherwise the formal proof may be valid for a stronger message than the actual protocol sent.[^ref-b7cbdbc06b3a]
Manages Complexity¶
The calculus turns a message exchange into a limited set of belief formulas and proof steps. That makes it easier to see which key assumption, freshness premise, authority claim, or inference rule supports a goal. In the early Andrew analysis, a desired belief cannot be derived because the final new-key message lacks freshness evidence that A can use.[^ref-b7cbdbc06b3a]
This simplification leaves out implementation errors, cryptosystem weaknesses, secret disclosure, and the full space of adversarial executions. Those are outside the original paper's stated focus and need other evidence.[^ref-b7cbdbc06b3a]
Abstract Reasoning¶
Begin with a precise goal, such as A believing that B currently believes a new session key is good. List the idealized messages and independent initial beliefs. Follow the message-meaning, freshness, and jurisdiction rules with their conditions, recording where a past utterance becomes a current belief. If the goal cannot be reached, identify the missing premise or message evidence instead of treating the goal as an axiom.[^ref-b7cbdbc06b3a]
A successful derivation shows what follows inside the model. A failed derivation can signal a useful defect or missing assumption, but it does not automatically prove an attack in every implementation. The early Andrew case includes the authors' separate replay account; that account should travel with its protocol version and assumptions.[^ref-b7cbdbc06b3a]
Knowledge Transfer¶
The same four roles appear in unlike cases: belief language, idealized messages, initial key/freshness/authority premises, and inference rules. Kerberos uses a trusted server and clocks to support scoped session-key beliefs. The early Andrew exchange lacks a needed freshness link for its final key message and suggests a nonce repair. The rules remain BAN rules in both analyses; the messages and premises differ.[^ref-b7cbdbc06b3a]
BAN is a domain-specific instance of the live Formal System Prime: its symbols and explicit postulates form a rule-governed calculus. Its key, message and freshness meanings come from authentication protocols. The shared pattern does not make BAN a general theory of every formal system.
Example¶
Kerberos: In the authors' server-mediated example, A and B receive material concerning a session key from server S. The language expresses each participant's beliefs; idealization represents tickets and replies as assertions; premises include trust in S and fresh timestamps; rules derive scoped key beliefs. The result depends on synchronized clocks. The optional fourth message supports a participation belief that the three-message version does not establish in the same way.[^ref-b7cbdbc06b3a]
Early Andrew Secure RPC: A and B already share a key and exchange nonces before B sends a new key. The language states A's desired belief about B and that key; idealization translates four messages; premises include the old key and generated nonces; rules stop short of the desired current belief because A has no freshness evidence for the last message. The authors give a replay account and propose including A's nonce in the repair.[^ref-b7cbdbc06b3a]
Relationships to Other Abstractions¶
Current abstraction Burrows–Abadi–Needham Logic Domain-specific
Parents (1) — more general patterns this builds on
-
Burrows–Abadi–Needham Logic is a kind of Formal System Prime
BAN logic specializes a rule-governed symbolic derivation system to authentication beliefs.
Hierarchy paths (2) — routes to 2 parentless roots
- Burrows–Abadi–Needham Logic → Formal System → Formalization → Representation → Abstraction
- Burrows–Abadi–Needham Logic → Formal System → Formalization → Transformation → Function (Mapping)
Neighborhood in Abstraction Space¶
Burrows–Abadi–Needham Logic sits in a sparse region of the domain-specific corpus (89th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Interpersonal Communication & Pragmatics (12 abstractions)
Nearest neighbors
- Induction of regular languages — 0.80
- Default logic — 0.80
- Radical probabilism — 0.80
- Esthesic and poietic — 0.80
- Semantic holism — 0.79
Computed from structural-signature embeddings · 2026-10-08
Not to Be Confused With¶
The protocol is the exchange under analysis; BAN is the calculus applied to its idealized messages. A freshness claim is an assumption to justify, not a fact created by writing it as a premise. A formally derived belief is conditional on the model and does not establish packet-level security or cryptographic secrecy. A past “said” statement is weaker than a current “believes” statement until the appropriate rules and conditions bridge them.[^ref-b7cbdbc06b3a]
References¶
[^ref-b7cbdbc06b3a]: Michael Burrows, Martin Abadi, and Roger Needham, “A Logic of Authentication,” ACM Transactions on Computer Systems 8, no. 1 (February 1990): 18–36, §§1–5.1 (method, Kerberos and Andrew Secure RPC analyses). https://web.stanford.edu/class/cs259/WWW04/papers/ban1990.pdf