Authentication in Distributed Systems: Theory and Practice

Reference: Lampson, B., Abadi, M., Burrows, M., & Wobber, E. (1992). Authentication in Distributed Systems: Theory and Practice. ACM Transactions on Computer Systems (TOCS) 10(4): 265–310. November 1992. (DEC SRC Report 83, 1992.) URL (Microsoft Research) · DOI

Summary

The ABLP paper (named for Abadi–Burrows–Lampson–Plotkin’s later refinement, but originating here) introduces the speaks-for calculus: a clean formal vocabulary for distributed authentication, delegation, and who is entitled to assert what on whose behalf. The setting: a distributed system in which principals (users, processes, machines, services) send requests that must be authorised. The traditional access-control question — is this principal allowed to perform this action on this object? — presupposes a prior question the paper answers: who is the principal whose request this is? That prior question becomes hard once requests pass through delegation chains (a user logs in to a workstation, which authenticates to a file server, which calls a database service on the user’s behalf): authentication is no longer one-to-one between principal and request but a chain of compound principals.

The technical heart of the paper is the speaks-for relation A ⇒ B: principal A speaks for principal B means that any statement A makes can be treated as if B had made it. Speaks-for is reflexive, transitive, and closed under conjunction and group membership. From A ⇒ B and A says s, the system derives B says s. Compound principals are built from atomic ones via conjunction (A ∧ B says s requires both to assert s), quoting (A | B says s means A is making a statement on behalf of B, but A retains responsibility), roles (A as R is A acting in role R), and for-channel (A for K is A speaking over channel/key K). The calculus is implementable: speaks-for facts are encoded in signed certificates, the access-control matrix grants rights to principals at any level of compoundness, and authentication reduces to checking a chain of certificates.

For the agent communication and security agenda this vault tracks, the speaks-for calculus is the formal vocabulary for delegated commitments and signed credentials. When agent B accepts a commitment from a process speaking on A’s behalf, the question “did A really commit?” is answered by the speaks-for chain witnessed by the credential. The paper is the philosophical and engineering ancestor of SPKI/SDSI (Rivest–Lampson–Ellison’s capability-style PKI, which Lampson designed using the speaks-for vocabulary), DIDs and Verifiable Credentials, object-capability facets, and modern attribute-based authorisation. For CBCL, speaks-for is the natural answer to “who signed this commitment?” — the dialect contract specifies which principals may emit which verdicts under which delegation rules, and the speaks-for chain provides the proof.

Key Ideas

Principals are first-class: a principal is anything that can make a statement — users, processes, machines, services, public keys, roles, groups, conjunctions, quotations. The system reasons uniformly about all of them.
The says operator: A says s is the primitive — principal A has asserted statement s. Authentication delivers says judgements; authorisation uses them.
The speaks-for relation: A ⇒ B means everything A says, B says. Reflexive, transitive, closed under conjunction. The delegation primitive.
Compound principals: built by conjunction (A ∧ B), quoting (A | B — A speaking on behalf of B), roles (A as R), and for-channel (A for K). A workstation acting on behalf of a user over a particular key is a compound principal at the leaf of an authentication chain.
Certificates as speaks-for witnesses: a signed certificate stating K ⇒ A (this key speaks for that principal) is the wire-format proof of a speaks-for fact. Authentication is verifying a chain of such certificates.
Access control on compound principals: the access-control list grants rights to principals at any level — Alice as Admin, Workstation | Alice for K, Group(Engineers). The complex authorisation patterns of real systems become tractable.
Trusted Computing Base separation: each principal has its own TCB; speaks-for chains let one principal delegate trust to another without fully merging TCBs.
Implementable: the paper describes the Taos system (DEC SRC) implementing the calculus; the design influenced Windows NT’s authentication architecture.

Connections

Conceptual Contribution

Claim: Distributed authentication and delegation can be cleanly formalised by the speaks-for relation A ⇒ B over a rich algebra of principals (atomic, conjunction, quoting, role, for-channel) together with the says operator. Authorisation reduces to checking that the speaker’s principal-expression has been granted rights to perform the requested action.
Mechanism: Define principals as a recursive algebra (atomic, A ∧ B, A | B, A as R, A for K). Define A says s (primitive) and A ⇒ B (speaks-for, reflexive-transitive-conjunctive). Encode speaks-for facts as signed certificates; authentication chains certificates from a trusted root to the requesting principal. Access-control lists grant rights to any principal expression; the request is authorised iff the deduced speaker’s principal is on the ACL. Implement the calculus in the Taos distributed OS as a concrete proof of practicality.
Concepts introduced/used: Speaks-For Calculus, ABLP Logic, Says Operator, Compound Principal, Quoting Principal, Role Principal, Delegation, Access Control List, Trusted Computing Base.
Stance: foundational technical paper / industry-grade reference design.
Relates to: The formal vocabulary that makes SPKI/SDSI (Rivest–Lampson–Ellison) intelligible: SPKI is the speaks-for calculus packaged as a PKI. DIDs and VCs inherit the same algebraic structure. Object capabilities (Dennis–Van Horn / EROS / Miller) are a dual view of the same problem (rights attached to objects rather than chains of delegation); the Spritely / OCapN line composes both views. For agent communication, speaks-for is the natural vocabulary for delegated commitments: when an agent’s process commits on the agent’s behalf, the speaks-for chain witnesses authority. The pair with Singh 1999 is direct: commitments without authority chains are weak, and authority chains without commitments are unactionable. CBCL’s signed-verdict architecture is a speaks-for application: the dialect contract names which principals may emit which verdicts under which delegation rules. The cryptographic complement is BAN logic (1990) and Spi calculus (1997) — BAN reasons about protocol soundness, ABLP reasons about who.

Tags

#authentication #lampson #abadi #speaks-for #ablp #delegation #distributed-security #foundations #capability #pki #classical

Backlinks

Linked Pages

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

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.

Tags

#crypto-protocol-verification #ban-logic #belief-logic #burrows #abadi #needham #security #foundations

CBCL - Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication

Reference: O’Connor, H. (2026). LangSec Workshop, IEEE Security and Privacy Workshops (SPW 2026). arXiv:2604.14512v1 [cs.CR], 16 Apr 2026. Source file: oconnor-cbcl-langsec26.pdf. URL. Reference implementation: https://codeberg.org/anuna/cbcl-rs.

Summary

Building on McCarthy’s 1975/1982 Common Business Communication Language vision and the language-theoretic security programme of Sassaman, Patterson, Bratus and Locasto (Security Applications Of Formal Language Theory), this paper presents a contemporary CBCL: an agent communication language designed so that all messages — including runtime language extensions — remain within the deterministic context-free (DCFL) complexity class. The motivating diagnosis is that contemporary agent communication has slid up the Chomsky hierarchy without acknowledging the security cost: KQML and FIPA-ACL are CFL with informal extensibility, but MCP and LLM-based agent frameworks operate over inputs whose effective complexity is recursively-enumerable, where the validity of an arbitrary message is undecidable and “weird machines” (Exploit Programming - From Buffer Overflows To Weird Machines) become unavoidable. CBCL takes the opposite tack: minimal core (8 performatives — tell, ask, reply, hello, bye, ok, error, cancel) plus a homoiconic dialect mechanism that lets agents define, transmit, and adopt domain-specific vocabularies as first-class CBCL messages, with three machine-checked safety invariants — R1 (no recursion in dialect templates), R2 (declared resource bounds on depth, expansion size, verification time), R3 (core-vocabulary preservation) — that together guarantee DCFL preservation under arbitrary finite sequences of dialect installations.

The paper accompanies the design with a Lean 4 formalization (≈5,400 lines, 16 modules, 176 machine-checked theorems, zero sorry gaps, no custom axioms) covering parser correctness (soundness + completeness), R1–R3 verification, pipeline totality, and the central dcfl_preserved closure theorem; a verified parser binary cbcl-parse is extracted from the proofs. A separately-developed Rust reference implementation (cbcl-rs, ≈11,000 lines, no_std-compatible core) ships a hand-rolled O(n) parser, dialect verification engine, gossip-based dialect propagation (O(log n) convergence per Demers et al.), C FFI/WASM bindings, property-based and differential tests, and cargo-fuzz targets; differential tests cross-validate the Rust parser against the Lean-extracted binary, eliminating spec-implementation parser differentials. Five example dialects (precision agriculture, AI planning, cross-chain asset transfer, artifact management, email) are R1–R3-verified end-to-end. A draft IETF Internet-Draft specifying application/cbcl and a Nostr transport binding (cbcl-nostr) accompany the paper. The Discussion explicitly aligns the design with Singh’s social-agency programme: dialect installation is treated as a public commitment to the dialect’s declared semantics — semantic divergence becomes a breach of commitment, observable and accountable, rather than a hidden failure of shared mental state — sidestepping the unverifiable mentalistic semantics critique of Verifiable Semantics for ACLs.

Implementation status (post-paper, cbcl-rs). The reference implementation has shipped two further safety invariants the paper sketches as future work, plus a richer Lean formalisation: R4 (Integrity) — Ed25519-style signatures over canonical encodings via an algorithm-agnostic Signer trait, with three-valued install verdicts (Valid / Unsigned / Invalid) — and R5 (Contract Well-formedness) — optional (protocol …) and (shape …) clauses on a dialect, expressing causal Merkle DAG protocols and per-performative shape contracts; R5 enforces acyclicity, reachability from begin, performative definedness with ancestor closure for extends, step uniqueness, and depth-bound respect, all decidable in linear fuel at install time. The §VII-D structural-contracts vision is therefore live (SPEC-002, SPEC-003): verify_monotone, verify_all_is_meet, and verify_eventually_consistent are proved theorems showing causal-protocol verification is a lattice homomorphism that joins coordination-free under G-Set store merge — explicit CALM Theorem alignment. The Lean codebase has grown to 380+ declarations across 19 files (still zero sorry, only the standard axioms propext / Classical.choice / Quot.sound); the workspace ships 837 tests including 584 cbcl-core unit tests, 37 proptest cases, 21 differential integration tests against the Lean-extracted binary, libFuzzer harnesses, and cargo-mutants mutation testing at a 90% kill threshold. The crate layout has grown from the paper’s five to seven: the original cbcl-core / cbcl-parser / cbcl-cli / cbcl-wasm / cbcl-ffi plus cbcl-erl (Erlang/LFE binding, SPEC-009 — with SPEC-010 binding-conformance suite) and cbcl-arena (Agent Arena platform, SPEC-012 — composable referee on cbcl-lfe-router with capability-keyed message routing and signed receipt logs). A worked sealed-bid auction dialect (SPEC-004) demonstrates structural defence against false-claim manipulation — concrete evidence that the R5 contract layer is rich enough to encode mechanism-design integrity properties decidably. The earlier Scheme prototype (anuna-research/cbcl) is superseded; architecture decisions live as ADRs under .hence/ (purity boundary, parser library choice, error handling, WASM API surface, R4 adversarial review).

Key Ideas

DCFL as the Goldilocks complexity class: Regular is too weak for nested envelopes/dialects; general CFL admits ambiguous grammars and parser-differential attacks; context-sensitive is PSPACE-complete; Type-0 is undecidable. DCFL is the minimal class that supports nested structure with class-level unambiguity (parser equivalence under language evolution).
Homoiconic self-extension: Dialect definitions are themselves valid CBCL messages, parsed by the same recogniser used for ordinary communication — a single attack surface, no separate meta-language. Inspired by Racket’s #lang mechanism.
Three safety invariants R1–R3: declarative pattern-template substitution only (no recursion, no iteration, no reflection); declared resource bounds (depth ≤ 64, expansion ≤ 8192 chars, verification ≤ 1000 ms); the eight core performatives cannot be redefined.
DCFL preservation theorem: dialect invocations must appear inside a (lang name …) wrapper; the lang tag plus a unique dialect name forms a prefix-free partition that lets a deterministic pushdown automaton dispatch to the appropriate subgrammar without extra lookahead — circumventing the fact that DCFLs are not closed under union in general. Mechanised in Lean 4 as dcfl_preserved.
Lean 4 formalization with extraction: 176 theorems, 0 sorry gaps, no custom axioms; the verified parser binary cbcl-parse is extracted from the proofs and runs the same fuel-bounded recursive-descent parser as the model.
Rust reference implementation: cbcl-core (no_std, no unsafe), cbcl-parser, cbcl-cli, cbcl-ffi, cbcl-wasm. Differential tests against the Lean-extracted binary; cargo-fuzz over five entry points.
Eight core performatives (tell, ask, reply, hello, bye, ok, error, cancel) plus four message categories (simple, meta, lang-scoped, wrapped); keyword parameters in Common-Lisp style (:thread, :in-reply-to).
Single-pass template expansion: terminates in time linear in the template plus argument size; not Turing-complete; output is not fed back into the expander, ruling out unbounded re-expansion.
Epidemic dialect propagation: gossip-based with Demers et al.’s O(log n) convergence bound; agents independently verify R1–R3 and signatures before installing.
Canonical serialization per RFC 9804 for cryptographic operations — deterministic byte representation as a precondition for signature verification.
Dialect identity by content hash: name collisions resolved by canonical-form hash; downgrade attacks rejected at installation.
Self-expression vs self-adaptation (Zambonelli et al.): traditional ACLs support only parameter tuning within fixed structure; CBCL is a self-expressive protocol whose vocabulary structurally evolves under safety constraints.
Singh-aligned reading of dialect installation: a public commitment to declared semantics, with :examples clauses providing machine-checkable behavioural anchors — semantic divergence as observable breach rather than hidden mental-state mismatch.
Stated limitations: DCFL ceiling means no recursive transformations, no cross-field references (e.g. checksums over fields), no aggregation over variable-length collections, no context-sensitive validation. Standish-taxonomy paraphrastic only — no Orthophrase, no Metaphrase. Trust infrastructure (key distribution, revocation) and dialect-curation policy left to deployment.
Structural-contracts extension (sketched in §VII-D, shipped post-paper as R4 + R5): Ed25519-style dialect signatures plus protocol constraints as causal Merkle DAGs over performative-typed messages, with Visibly Pushdown Languages for shape constraints and coordination-free monotonic verification over an append-only store. Lean-mechanised lattice-homomorphism theorems (verify_monotone, verify_all_is_meet, verify_eventually_consistent) establish that replica verdicts join under G-Set merge.

Connections

Common Business Communication Language — McCarthy’s 1975/1982 origin; CBCL is the formally-verified realisation of that vision.
Security Applications Of Formal Language Theory — Sassaman et al.’s LangSec foundations.
Proof-Carrying Code - Necula — Necula 1997, the architectural ancestor of CBCL’s R4 split (host runs a small certified verifier; producer ships the proof).
Enforceable Security Policies - Schneider — Schneider 2000, the formal warrant for R5 monotone-verdict trace monitoring.
An Axiomatic Basis for Computer Programming - Hoare — Hoare 1969, root of the contract-based verification line CBCL inherits.
Authentication in Distributed Systems - Lampson Abadi Burrows Wobber — Lampson et al. 1992, the Speaks-For Calculus for delegated commitments.
Articulating Reasons - Brandom — Brandom 2000, the philosophical underwriting of Public Semantics (entry point).
Making It Explicit - Brandom — Brandom 1994, the full inferentialist treatise.
Empiricism and the Philosophy of Mind - Sellars — Sellars 1956, the Myth of the Given that makes Semantics-Without-Minds possible.
Philosophical Investigations - Wittgenstein — Wittgenstein 1953, Meaning As Use / language-games / rule-following.
Two Dogmas of Empiricism - Quine — Quine 1951, Semantic Holism.
Assertion - Stalnaker — Stalnaker 1978, Common Ground update semantics — operational analogue of CBCL’s verdict ledger.
Languages and Language - Lewis — Lewis 1975, Convention of Truthfulness picture of how an abstract language gets in force in a population.
Communicative Actions for Artificial Agents - Cohen Levesque — Cohen & Levesque 1995, the Mentalistic Semantics high-water mark CBCL deliberately is not.
FIPA-ACL Specifications — the engineering of FIPA-ACL (envelope, conversation-id, ontology slot) CBCL inherits; the semantics it replaces.
An Ontology for Commitments in Multiagent Systems - Singh — Singh 1999, the formal commitment ontology CBCL’s dialect contracts instantiate.
Jones-Sergot Normative Systems — Jones & Sergot 1993, the Counts-As Relation that gives wire events institutional meaning under a dialect contract.
Exploit Programming - From Buffer Overflows To Weird Machines — weird-machine analysis CBCL is designed to preclude at the parser layer.
PKI Layer Cake - Kaminsky Patterson Sassaman — concrete parser-differential attacks; CBCL’s class-level unambiguity rules these out at the grammar level.
The Halting Problems of Network Stack Insecurity
A Language-Based Approach To Prevent DDoS
LangSec
KQML as an Agent Communication Language
KQML - A Language And Protocol For Knowledge And Information Exchange
FIPA-ACL
ACL Rethinking Principles — Singh’s social-agency critique that CBCL’s “dialect installation as public commitment” inherits.
Agent Communication Languages - Rethinking the Principles
Verifiable Semantics for ACLs
A Common Ontology Of ACLs
Commitment-based Semantics
The State of the Art in Agent Communication Languages
Trends in Agent Communication Language
Toward Principles for the Design of Ontologies Used for Knowledge Sharing — Gruber’s ontological-commitment principle CBCL inherits.
Some Philosophical Problems from the Standpoint of Artificial Intelligence — McCarthy & Hayes’s representation/computation separation.
Elephant 2000 - A Programming Language Based on Speech Acts — McCarthy’s intra-program speech-act counterpart to CBCL’s inter-organisational vision.
Adjectival Modifiers
S-expression
Homoiconicity
Code as Data
Creating Languages in Racket — Flatt’s #lang mechanism that inspired CBCL’s homoiconic self-extension.
Extensibility in Programming Language Design - Standish
Language Extensibility Taxonomy
Paraphrase
Orthophrase
Metaphrase
Self-Expression
Self-Adaptation Self-Expression Self-Awareness ASCENS
Dialects and Idiolects
Keeping CALM - When Distributed Consistency is Easy — CALM theorem underwriting the forthcoming coordination-free contracts extension.
Visibly Pushdown Languages
MCP Landscape Security Threats And Future Research Directions
Survey Of AI Agent Protocols
Survey Of Agent Interoperability Protocols
ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems — concrete LLM-agent worm whose root-cause analysis CBCL’s lang-scoped provenance addresses.
Why AI Agents Communicate In Human Language
Why Do Multi-Agent LLM Systems Fail
Gossiping in Distributed Systems
Gossip-based Aggregation in Large Dynamic Networks

Conceptual Contribution

Claim: Agent communication languages can be simultaneously expressive, runtime-extensible, and tractably verifiable iff every message — including those that extend the language — is constrained to the deterministic context-free language class; this constraint is compatible with first-class self-extension, can be machine-checked end-to-end, and converts the unverifiable-mental-state problem of mentalistic ACLs into a public-commitment problem at the protocol layer.
Mechanism: Eight-performative core grammar (LL(1), DCFL); homoiconic dialect mechanism — dialect definitions are valid CBCL messages with extend clauses describing pattern-template substitutions; three safety invariants R1–R3 enforced at installation (no recursion via DFS cycle detection, declared resource bounds, core-vocabulary preservation); (lang name …) wrapper providing prefix-free deterministic dispatch into per-dialect sub-grammars so the union remains DCFL. Lean 4 formalization (LeanCbcl, ~5,400 LoC, 176 theorems) covering parser soundness/completeness, R1–R3, pipeline totality, and dcfl_preserved; verified parser extracted to a runnable binary (cbcl-parse). Rust reference implementation (cbcl-rs, ~11,000 LoC) with a ResourceContext-tracked single-pass expander, gossip-based dialect propagation (O(log n) per Demers et al.), canonical RFC-9804 serialization for signing, algorithm-agnostic Signer trait, C FFI / WASM bindings, property-based + differential tests, fuzz targets. Draft IETF application/cbcl Internet-Draft and Nostr transport binding.
Concepts introduced/used: Deterministic Context-Free Language, LangSec, Homoiconicity, S-expression, Dialects and Idiolects, Performatives, Self-Expression, Paraphrase, Orthophrase, Metaphrase, Visibly Pushdown Languages, CALM Theorem, Commitment-based Semantics, Public Semantics, Verifiable Semantics, Adjectival Modifiers, Ontological Commitment, Lean 4, Property-Based Testing, Parser Differential Attack, Weird Machine, Gossip Protocols, Canonical Serialization, Nostr, hence
Stance: engineering / formal-methods, with explicit position-taking on the agent-communication design space
Relates to: Realises McCarthy’s Common Business Communication Language vision (1975/1982) by giving formal safety guarantees McCarthy could only gesture at. Sits squarely in the LangSec programme of Security Applications Of Formal Language Theory and Exploit Programming - From Buffer Overflows To Weird Machines, extending it from input-validation analysis to protocol design — claiming, plausibly, to be the first ACL designed from LangSec principles and the first to demonstrate that LangSec is compatible with runtime self-extension. Inherits the DCFL-vs-ambiguous-CFG argument from PKI Layer Cake - Kaminsky Patterson Sassaman and applies it at the message layer rather than the certificate layer. Builds explicitly on Singh’s social-agency critique (ACL Rethinking Principles) and Wooldridge’s verifiability programme (Verifiable Semantics for ACLs) by treating dialect installation as a public commitment whose semantics are anchored by the :examples clause — a machine-checkable analogue of the commitment-trace conformance that Flexible Protocol Specification and Execution (Yolum & Singh) and Commitment Machines - Yolum and Singh establish for protocol actions. Where Pact - A Choreographic Language for Agentic Ecosystems takes the individual-rationality fork to answer “why follow a protocol?”, CBCL takes the publicness/verifiability fork: the meaning of a message is fully determined by the formal grammar plus declared semantics, with no mental-state inference required. Inherits Gruber’s ontological-commitment architecture but replaces “out-of-band agreement” with in-protocol propose/query/teach. The extensibility design draws on Creating Languages in Racket (Flatt’s #lang) and respects the boundary set by Extensibility in Programming Language Design - Standish: paraphrastic only, deliberately excluding orthophrase/metaphrase to keep the attack surface bounded. The forthcoming structural-contracts extension uses Visibly Pushdown Languages for shape constraints and the CALM Theorem for coordination-free verification — a natural bridge to commitment-machine semantics. The LLM-agent threat-model framing (ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems, MCP Landscape Security Threats And Future Research Directions) positions CBCL as the structural alternative to MCP/JSON-RPC-with-natural-language: same extensibility, vastly tighter security envelope.

An Ontology for Commitments in Multiagent Systems - Singh

An Ontology for Commitments in Multiagent Systems: Toward a Unification of Normative Concepts

Reference: Singh, M. P. (1999). An Ontology for Commitments in Multiagent Systems: Toward a Unification of Normative Concepts. Artificial Intelligence and Law 7(1): 97–113. Kluwer. DOI · Author copy via Academia.edu · Singh publications (NCSU)

Summary

This paper is the formal core of Singh’s commitment-based programme — a piece that sits between the polemical <em>Rethinking the Principles</em> (1998) and the operationalised commitment machines line (Yolum & Singh 2002). Singh argues that the multiplicity of normative concepts used across MAS, deontic logic, and law — obligation, permission, prohibition, promise, contract, delegation, cancellation, release — can be unified by taking the social commitment as the basic ontological primitive and reconstructing the rest as patterns over commitments. A social commitment is a four-place relation: a debtor is committed to a creditor for the fulfilment of some condition in the context of a particular institution or social scope. Once these four roles are fixed, the standard normative operations — create, discharge, cancel, release, delegate, assign — become commitment-state transitions, and the deontic vocabulary becomes a derived layer over the commitment substrate.

The construction is deliberately public: commitments live in the social state, not in the heads of any agent. A commitment exists when a publicly observable act has created it (a promise speech act, a contract signing, an assertion under appropriate sincerity context); it persists until a publicly observable act has discharged or cancelled it. The truth-conditions for “agent A is committed” are externally checkable: they reference the social record, not A’s mental state. This is the exact alternative to the mentalistic semantics of FIPA / Cohen and Levesque 1995 that Rethinking the Principles called for. The paper also sets up the bridge to law: Singh notes the close fit with Jones and Sergot’s “count-as” relation, with deontic logic, and with the speaks-for tradition in distributed systems — establishing commitments as a unifying normative substrate across philosophy, law, MAS, and computer security.

For CBCL and the broader public-semantics line, this is the ontology document: it defines what “commitment” means precisely enough that protocol designers can map performatives onto commitment-state transitions and verifiers can monitor compliance from a transcript. The four-place structure (debtor, creditor, condition, context) maps almost directly onto the ledger-of-commitments architecture in Fornara & Colombetti 2004 and the dialect contracts in CBCL. The paper is also the place to cite when arguing that commitment-based ACL semantics is not merely a behavioural surrogate but a real normative theory with established connections to legal and deontic logic.

Key Ideas

Commitment as the primitive normative concept: a four-place relation C(debtor, creditor, condition, context) — agent x is committed to agent y for the fulfilment of condition q in the social context s. The four roles must always be specified; commitments without a creditor are degenerate.
Standard commitment operations: create (a new commitment comes into being via a public act), discharge (the condition is satisfied), cancel (the debtor unilaterally retracts, possibly incurring meta-commitment), release (the creditor waives), delegate (the debtor passes the obligation to a third party with creditor consent), assign (the creditor passes the entitlement).
Conditional commitments: CC(x, y, p ⊃ q, s) — x is committed to y to bring about q if p holds. The conditional structure handles contracts, contingent obligations, and protocol-state dependencies.
Discharge by satisfaction: a commitment is discharged when its condition is satisfied (in the relevant social interpretation); discharge is monotone — once discharged, the commitment is closed.
Deontic vocabulary as derived: obligation, permission, prohibition, right, and duty are reconstructable from commitment patterns plus the relevant institutional context.
Public, externally checkable semantics: commitments are facts about the social record, not about agent mental states. Verification is by inspection of the transcript and the institutional rules.
Bridges to legal informatics and deontic logic: the framework is explicitly compatible with Jones and Sergot’s count-as relation and with classical deontic-logic operators, positioning commitments as the unifier across philosophy, law, MAS, and distributed-security normative reasoning.

Connections

Conceptual Contribution

Claim: The proliferation of normative concepts across MAS, deontic logic, and law can be unified by taking the social commitment — a four-place relation C(debtor, creditor, condition, context) — as the basic primitive and reconstructing obligation, permission, prohibition, contract, and delegation as commitment patterns. Commitments are public: their existence is determined by observable acts and observable conditions, not by agent mental states.
Mechanism: Define commitments as four-place relations (debtor / creditor / condition / context) and conditional commitments analogously. Specify the operations create / discharge / cancel / release / delegate / assign as commitment-state transitions. Show how standard deontic-logic operators and standard legal concepts (promise, contract, breach, novation) reduce to patterns over these primitives. Sketch the bridge to Jones and Sergot’s count-as analysis of institutional facts.
Concepts introduced/used: Social Commitment, Conditional Commitment, Commitment Operations (create / discharge / cancel / release / delegate / assign), Debtor, Creditor, Condition, Context (Commitment), Deontic Reduction.
Stance: foundational technical paper / unifying ontology.
Relates to: The formal statement of the programme Singh 1998 argued for polemically; the bridge to the operational accounts in Yolum & Singh 2002, Yolum & Singh 2002b, and Fornara & Colombetti 2004. The philosophical complement is Brandom: Singh’s commitments are precisely the commitment leg of Brandom’s deontic scorekeeping triple. The legal complement is Jones & Sergot 1993 — count-as gives the institutional grounding for what makes a publicly observable act count as creating a commitment. The distributed-systems complement is the speaks-for tradition (Lampson et al. 1992) — credentials and delegated assertion authority are commitment patterns of the same family. CBCL’s dialect contracts and verdict ledger directly instantiate this ontology at wire-format granularity.

The Heart of Spritely - Distributed Objects and Capability Security

The Heart of Spritely: Distributed Objects and Capability Security

Reference: Christine Lemmer-Webber, Randy Farmer, Juliana Sims (2025). Spritely Institute whitepaper, May 21 2025. Source file: spritely-core.pdf. URL · Project

Summary

The second paper in Spritely’s three-part design series, this whitepaper lays out the technical core of Goblins — a distributed, transactional, object-programming environment built around object capability security (OCap). The thesis: secure peer-to-peer applications should feel like ordinary programming, not like a separate security discipline, and capability security makes that achievable. The operative slogan is “If you don’t have it, you can’t use it” — authority is conveyed only by holding a reference, never ambient.

The paper works through (1) capability security as ordinary reference-passing, motivated against Access Control Lists and the confused-deputy problem; (2) Goblins itself — a distributed object programming model with promise pipelining, vats as containers of synchronous turns, turns as cheap local transactions, and time-travel debugging; (3) OCapN — a new cross-implementation protocol for secure distributed object communication; (4) portable encrypted storage for capabilities; (5) library/application safety implications. Implementations exist for Guile and Racket Schemes, with a roadmap toward language-heterogeneous object invocation.

Goblins is the modern distillation of a three-decade lineage running through Mark Miller’s E language, the CapTP protocol, Jonathan Rees’s capability-kernel argument, and Carl Hewitt’s actor formalism. It reframes agent communication as object-reference passing over the network, offering an alternative substrate to the ACL/RPC-stack approach that dominates modern LLM-agent protocols.

Key Ideas

Principle of Least Authority (POLA): grant each piece of code only the authority it needs, no more
Object capability security: authority = unforgeable object reference. Lexical scoping + no ambient authority + no global mutable state
Confused-deputy problem: why ACLs fail when a privileged program is tricked into acting for an attacker
Vat: an isolated synchronous execution context; objects live inside vats; vats communicate asynchronously
Turn: an atomic event loop iteration inside a vat; turns are transactional — errors roll back the turn’s local state
Promise pipelining (from CapTP): chain calls on a reference before the prior call resolves, reducing round trips
Time-travel distributed debugging: replay turns deterministically across the network
OCapN (Object Capability Network): protocol for secure, cross-language distributed object invocation
Revocation and accountability as programmable patterns over references
“If you don’t have it, you can’t use it” — the design-level simplification capability security provides

Connections

Security Kernel Lambda Calculus — Rees’s lexical-scope-as-capability-kernel argument, directly cited
Capability Security
A Universal Modular Actor Formalism for Artificial Intelligence — vats descend from Hewitt actors
Actor Model
Programming Erlang Second Edition — sibling message-passing tradition
Communicating Sequential Processes — contrast in concurrency model
Agent Tcl Flexible Secure Mobile Agents — earlier capability-aware mobile agents
DAgents Security Book Chapter
Sandboxing
Distributed Security
LangSec
End-to-End Arguments in System Design — design-principle neighbour
Principled Design Of The Modern Web Architecture — architectural contrast (REST/ACL vs OCap)
Agent-to-Agent Protocol — OCapN is a capability-secure alternative
Model Context Protocol
Agent Network Protocol
Inter-Agent Trust Models - A Comparative Study — Constraint trust realised at the language level
Constraint Trust
MalTool Malicious Tool Attacks — OCap would structurally preclude many of these attacks
AI Agents Under Threat
ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems — the flat context trust model ClawWorm exploits is precisely what OCap eliminates
Flat Context Trust Model
Principle of Least Authority
Ambient Authority
Confused Deputy
Vat Model
Turn (Goblins)
Promise Pipelining
OCapN
CapTP
E Language
Time-Travel Debugging

Conceptual Contribution

Claim: Secure peer-to-peer applications become routine when authority is conveyed only by holding an unforgeable object reference — no ambient authority, no global mutable state, lexical scope as the capability kernel — and when the network distribution of such references is itself designed as an ordinary message-passing object system.
Mechanism: Goblins realises the E-language tradition in Scheme (Guile, Racket): objects live in vats; each vat runs atomic turns that serve as cheap local transactions; asynchronous inter-vat invocation uses promise pipelining to collapse round-trips; persistence, upgrade, and cross-language interop are handled by OCapN — a capability-preserving transport protocol. Time-travel debugging exploits the turn-level determinism.
Concepts introduced/used: Object Capability Security, Principle of Least Authority, Ambient Authority, Confused Deputy, Vat Model, Turn (Goblins), Promise Pipelining, OCapN, CapTP, E Language, Time-Travel Debugging, Capability Revocation
Stance: engineering / foundational design doc
Relates to: A modern engineering culmination of the capability-security thread rooted in Security Kernel Lambda Calculus (Rees 1995, explicitly cited) — lexical scope as a capability kernel, extended into a full distributed system. The vat model is a direct descendant of A Universal Modular Actor Formalism for Artificial Intelligence (Hewitt 1973) and sibling to Programming Erlang Second Edition but with security-by-reference as a first-class concern. Frames a structural alternative to the modern LLM-agent protocol stack: where Agent-to-Agent Protocol / Model Context Protocol / Agent Network Protocol layer trust on top of ACL/RPC primitives, OCapN encodes trust in the reference graph itself. The flat context trust model that ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems exploits and that MalTool Malicious Tool Attacks, AI Agents Under Threat catalogue is precisely the ambient-authority failure capability security is designed to prevent — making Goblins / OCapN a serious candidate substrate for Inter-Agent Trust Models - A Comparative Study’s Constraint trust dimension.

Capability Myths Demolished

Reference

Miller, Mark S.; Yee, Ka-Ping; Shapiro, Jonathan S. Capability Myths Demolished. Technical Report SRL-2003-02, Systems Research Laboratory, Johns Hopkins University, 2003. URL

Summary

This short, polemical technical report dismantles three widely repeated myths about capability-based security that had accreted in the literature over the preceding two decades and were being cited as reasons to avoid capability models or to pile extra access checks on top of them. The three myths are: (1) the Equivalence Myth - that ACL systems and capability systems are formally equivalent views of Lampson’s access matrix; (2) the Confinement Myth - that capability systems cannot enforce confinement; and (3) the Irrevocability Myth - that capability-based authority cannot be revoked.

The authors’ strategy is to disentangle three very different things all called “capability” in the literature: Model 2 (capabilities-as-rows of the access matrix), Model 3 (capabilities-as-keys / unforgeable bitstrings), and Model 4 (object-capabilities, where capabilities are object references in a memory-safe object language). They define seven security properties - including “no designation without authority,” dynamic subject creation, subject-aggregated authority management, and composable confinement - and show how the three models differ on each. Under this lens, the Equivalence Myth collapses: ACLs and object-capabilities have fundamentally different rules for how the access matrix is updated, even if both can be drawn as an access matrix at an instant.

The Confinement Myth is refuted by pointing to KeyKOS factories (Hardy 1988) and the EROS constructor, which demonstrably achieve confinement in object-capability systems. The Irrevocability Myth is refuted via the Redell forwarder/facet pattern (1974), elegantly explained with a simple diagram: Alice hands Bob a forwarder to Carol and keeps the revoker; dropping the revoker drops Bob’s access. The paper is the go-to reference whenever these myths resurface and is essential intellectual groundwork for the ocap tradition.

Key Ideas

Three distinct capability models: capabilities-as-rows, capabilities-as-keys, object-capabilities - not interchangeable.
The access-matrix snapshot lies: static snapshots ignore the update rules that actually distinguish ACL systems from capability systems.
No Designation Without Authority (Property A): in an ocap system, to name a resource is already to have authority to use it; ACL systems decouple designation from authority, which is the root of confused-deputy problems.
Subject-Aggregated Authority Management (Property C): in ocap, you edit your own C-list; in ACLs, changing one authority requires editing a resource’s ACL.
Confinement is achievable via factories / constructors; KeyKOS and EROS are existence proofs.
Revocation by forwarders (facets): give Bob not Carol but a forwarder F; keep R as revoker; R !stopForwarding revokes Bob cleanly.
Object capabilities subsume Lampson while avoiding the ambient-authority pitfalls that produce confused deputies.

Connections

The Heart of Spritely - Distributed Objects and Capability Security
Capability Security - this paper is the canonical clarification of what capability security actually claims.
Object Capability Security - Model 4 in this paper is the object-capability model.
E Language - examples and diagrams use E-flavoured ocap reasoning.
CapTP - distributed ocap relies on the same non-myths.
Ambient Authority - the Equivalence Myth’s error is essentially failing to see ambient authority in ACL systems.
Confused Deputy - the paper leans on Hardy’s example to justify Property A.
Principle of Least Authority - POLA is called out as a motivation for preferring ocap.
Distributed Security
Security Kernel Lambda Calculus
Capability Revocation - Redell forwarders / facets are explained here.
Capability Bounding

Conceptual Contribution

EROS - A Fast Capability System

EROS: A Fast Capability System

Reference

Shapiro, Jonathan S.; Smith, Jonathan M.; Farber, David J. “EROS: A Fast Capability System.” In Proceedings of the 17th ACM Symposium on Operating Systems Principles (SOSP ’99), Kiawah Island, SC, December 1999. Published as ACM SIGOPS Operating Systems Review 34(5):170-185. URL

Summary

EROS (Extremely Reliable Operating System) is the third-generation reimplementation of the GNOSIS/KeyKOS capability architecture - the lineage created by Norm Hardy et al. at Tymshare in 1982 - clean-roomed in C++ for x86 by Jonathan Shapiro, Jonathan Smith, and David Farber at Penn. The paper’s central claim, surprising to many at the time, is that a pure capability microkernel with transparent single-level store persistence can match or beat conventional Unix-kernel operation costs on commodity hardware. The authors show this through detailed microbenchmarks and careful architectural choices.

Architecturally, EROS is a microkernel. All resources - processes, address spaces, nodes (32-capability arrays), pages, entry capabilities, resume capabilities - are named and manipulated by unforgeable capabilities enforced by a tagged in-kernel data structure. A protection domain is defined by the set of capabilities held. The performance story rests on three pillars: (1) aggressive caching of abstract objects (processes, nodes, pages) in representations chosen for the underlying hardware; (2) unified design of IPC and capability invocation so that cross-domain calls are cheap; and (3) orthogonal persistence via periodic consistent snapshots with copy-on-write - meaning EROS has no file system in the traditional sense: the single-level store is the persistence mechanism, transparent to applications. A machine crash resumes where it left off, modulo the checkpoint interval.

The paper also addresses mandatory access control, the KeySAFE design (user-level reference monitors inserted between compartments for DAC/MAC composition), and the architectural features (nodes, entry capabilities, resume capabilities for one-shot continuations) that together let EROS support confinement and fine-grained POLA. EROS directly inspires seL4, CapROS, Coyotos, and is the principal existence proof cited whenever someone claims capability systems must be slow. It is a central reference in Miller’s Robust Composition thesis and in the Capability Myths Demolished paper’s defeat of the Confinement Myth.

Key Ideas

Single-level store: no file system; persistence is transparent, implemented by periodic consistent copy-on-write snapshots.
Capability is an unforgeable (object-id, rights) pair, kernel-enforced via tagged storage.
Nodes: 32-slot capability arrays, the building block for address spaces (tree of nodes) and process state.
Entry / resume capabilities: first-class continuation-like capabilities for efficient IPC and one-shot reply.
Fast IPC: EROS capability invocation matches L4-class IPC, demonstrated by microbenchmarks.
KeySAFE compartments: user-level reference monitors mediate flow between compartments for policy insertion.
Confinement via factories / constructors: inherited from KeyKOS, demonstrably solves the confinement problem.
Performance is not a capability-system inherent cost: with the right abstractions and caching, ocap kernels match conventional kernels.

Connections

The Heart of Spritely - Distributed Objects and Capability Security - EROS is in the direct intellectual lineage Spritely draws on.
Capability Security, Object Capability Security - EROS is the flagship existence proof for practical capability OSs.
E Language - Miller’s thesis advisor is Shapiro; EROS and E are sister projects in Johns Hopkins’ SRL.
CapTP
Ambient Authority - EROS has essentially none; every action requires an explicit capability invocation.
Confused Deputy - EROS’s design makes confused-deputy scenarios expressible-as-bugs only by explicit negligence.
Principle of Least Authority - fine-grained node capabilities enable POLA at page level.
Distributed Security
Security Kernel Lambda Calculus
Capability Bounding
Capability Revocation

Conceptual Contribution

Programming Semantics for Multiprogrammed Computations

Reference

Dennis, Jack B.; Van Horn, Earl C. “Programming Semantics for Multiprogrammed Computations.” Communications of the ACM, 9(3):143-155, March 1966. URL

Summary

The Dennis & Van Horn paper is the origin point of the capability concept in computer science. Written during the Project MAC era and responding to the needs of multiprogrammed, multi-user systems like MULTICS and the SABRE reservation system, it defines a set of meta-instructions that a supervisor provides to user programs to express the five core requirements of multiprogrammed computation: (1) parallel processing; (2) creating, suspending, and resuming computations; (3) protection of a computation from other computations; (4) debugging support; and (5) shared access to data and procedures.

The paper’s lasting contribution is the introduction of the capability (called a C-list entry) as the fundamental access-control primitive. A capability is an unforgeable pair of a unique-name (naming a segment or other object) and an access-indicator (X, R, RW, RWX) that determines what may be done with the object. A computation’s sphere of protection is defined precisely by its C-list. Crucially, a process cannot name a resource it has no capability for - designation and authority are unified. The paper introduces principals (the human or organisational accountability unit), processes as loci of execution, and the meta-instructions for fork/join, lock/unlock, I/O function invocation, and capability transfer.

This is the paper that every later capability system - Plessey 250, CAP, KeyKOS, EROS, seL4, E, Spritely - is ultimately paying tribute to. It is also striking how many apparently recent ideas (unforgeable references, segment-level fine-grained protection, per-process authority sets, mutually suspicious processes on one machine) are already present here in 1966.

Key Ideas

Capability as an unforgeable (unique-name, access-indicator) pair; the first definition in the literature.
C-list per process: the exhaustive list of a computation’s authorities.
Sphere of protection = closure of what a process can name and do via its C-list.
Principal vs process: accountability vs. execution.
Meta-instructions as the supervisor’s API for computations: fork, join, quit, lock, unlock, execute i/o function, create segment, enter block, etc.
Multiprogramming as access-control problem: protection, sharing, and scheduling are one design problem, not three.
Designation and authority unified: a name in a program is dereferenced through the C-list, so “unknown” resources are also “unreachable” - the ancestral seed of “no designation without authority.”
Mutually suspicious computations as a first-class goal.

Connections

The Heart of Spritely - Distributed Objects and Capability Security
Capability Security - this is the paper that invents the concept.
Object Capability Security - Miller-era ocap refines Dennis & Van Horn’s C-list into object references.
E Language - E’s reference-passing rules are a memory-safe OO realisation of Dennis-Van-Horn C-lists.
CapTP
Ambient Authority - designation-without-authority, which ambient-authority systems permit, is precisely what this paper eliminates by construction.
Confused Deputy - Hardy’s 1988 paper points back to Dennis & Van Horn as the road not taken.
Principle of Least Authority - C-lists make POLA expressible at segment granularity.
Distributed Security
Security Kernel Lambda Calculus
A Universal Modular Actor Formalism for Artificial Intelligence - Hewitt’s actors and Dennis-Van-Horn capabilities are parallel 1960s-70s answers to concurrent computation; Miller’s E later unifies them.
Actor Model
Vat Model

Conceptual Contribution

Verifiable Credential

A W3C-standardised signed assertion (JSON-LD or JWT) issued by one DID-identified party (the issuer) about another DID-identified party (the subject). Carries issuer, credentialSubject, dates, claims, and a cryptographic proof. Supports selective disclosure (BBS+ signatures), zero-knowledge predicates (zk-SNARK proofs over claims without revealing them), and revocation via status-list credentials. Presented to a verifier via a Verifiable Presentation.

In this vault

Decentralized Identifiers

W3C-standardised globally resolvable identifiers (DIDs) that are created, owned and controlled by their subject without a central registry. Each DID resolves to a DID Document containing public keys and service endpoints, supporting self-sovereign agent identity.

In this vault

SPKI-SDSI

SPKI / SDSI: A Simple Distributed Security Infrastructure with Linked Local Names

Reference: Rivest, R. L. & Lampson, B. (1996). SDSI — A Simple Distributed Security Infrastructure. (Working document, MIT.) Followed by: Ellison, C., Frantz, B., Lampson, B., Rivest, R., Thomas, B. & Ylonen, T. (1999). SPKI Certificate Theory. RFC 2693, IETF. (Also: Clarke, D. E., Elien, J.-E., Ellison, C., Fredette, M., Morcos, A. & Rivest, R. L. (2001). Certificate Chain Discovery in SPKI/SDSI. Journal of Computer Security 9(4).) Open access (RFC 2693) · SDSI 1.0 (Rivest-Lampson, MIT) · Chain discovery (Elien MIT MS thesis 1998)

Summary

Rivest, Lampson, Ellison and the SPKI working group develop SPKI/SDSI, a public-key infrastructure that takes a sharply different stance from the X.509 / hierarchical-CA tradition: instead of a global namespace of certified identities rooted in a chain of certificate authorities, SPKI/SDSI gives each principal its own local namespace and certificates that bind keys to authorisations rather than identities. SDSI’s central innovation is linked local names: K_alice's friends is a name in K_alice’s namespace; K_alice's friends's secretary is a chain of links — no global registry needed. Authority delegation is similarly local: a certificate K_a → K_b : auth issued by K_a grants authority auth to K_b, optionally with delegation rights. Authority is what matters, not who — a distinction Lampson summarised as “we’re moving from authentication to authorization.” The SPKI Certificate Theory (RFC 2693) formalises this: certificates are 5-tuples <Issuer, Subject, Delegation, Authority, Validity>; chain discovery (Clarke et al. 2001) gives a sound and complete algorithm for deriving “does this principal have this authority?” from a collection of certificates. The design directly anticipates modern decentralised identity / object-capability composition: SPKI/SDSI is the conceptual bridge between the object-capability tradition (E, Spritely) and the cryptographic-identity tradition (X.509, PGP). DIDs and Verifiable Credentials inherit substantial conceptual machinery from SPKI/SDSI; Macaroons (Birgisson et al. 2014) are SPKI-style attenuable capability tokens for HTTP APIs.

Key Ideas

Authorization, not authentication: certificates bind keys to authorities — what the principal is permitted to do — rather than to identities. The question “who is this key?” is replaced by “what is this key allowed to do?”
Local namespaces (SDSI): each principal has its own namespace; names are local identifiers like K_alice's bob, with no global resolution. Linked local names chain across namespaces: K_alice's bob's friends resolves through K_alice’s and then K_bob’s namespaces.
Delegation as a first-class certificate field: a certificate may grant authority with or without the right to re-delegate; chains of delegated certificates are the principal authority-derivation mechanism.
5-tuple certificates: <Issuer, Subject, Delegation-flag, Authorization-S-expression, Validity> (RFC 2693 §2.4 calls the field “Authorization”, not “Authority”); the Authorization is an S-expression in a structured language (action, object, qualifier) that supports rich access-control specifications.
Chain discovery (Clarke et al. 2001): given a goal K_principal has authority A, the chain-discovery algorithm searches the certificate collection for a derivation; sound and complete; polynomial in the size of the certificate collection for many practical fragments.
No mandatory identity binding: certificates may bind keys to local names (SDSI-style) or directly to authorisations (SPKI-style) — identity is just one kind of authority. The system can be used without ever assigning a global “real name” to a key.
Capability composition: SPKI authorities compose under intersection and chain; the resulting authority is the most-restrictive intersection along the chain. This is exactly the capability-security composition rule lifted to a certificate-based distributed setting.

Connections

Conceptual Contribution

Claim: A distributed security infrastructure should bind cryptographic keys to authorisations (what they may do) rather than to identities (who they “really” are); each principal should have its own local namespace; authority delegation should be first-class with an explicit chain-discovery algorithm. The X.509 hierarchical-CA model is the wrong fit for most distributed-system access-control needs.
Mechanism: 5-tuple certificate format (issuer / subject / delegation / authority / validity); local namespaces with linked-local-names resolution; sound and complete chain-discovery algorithm; authority composition under intersection.
Concepts introduced/used: SPKI, SDSI, Linked Local Names, Capability Certificate, Authority-not-Identity, Chain Discovery.
Stance: foundational systems-design paper / IETF specification.
Relates to: Direct conceptual bridge between the object-capability tradition (Dennis & Van Horn 1966, EROS, the E-language line in Miller 2006) and the cryptographic-identity tradition (X.509, PGP). SPKI/SDSI explicitly takes the capability stance — unforgeable name = capability — and lifts it into a distributed cryptographic setting where the unforgeability comes from the public-key cryptography rather than from memory protection. The Macaroons paper (Birgisson, Politz, Erlingsson, Taly, Vrable & Lentczner 2014) is SPKI/SDSI’s most-deployed modern descendant: HMAC-chained authority tokens with attenuation, used in production at Google and elsewhere. Modern decentralised-identity standards — W3C DIDs, Verifiable Credentials, the Authorization Capabilities (zCaps) work — inherit substantial conceptual machinery from SPKI/SDSI even when they do not cite it directly. Within this vault, SPKI/SDSI is the missing distributed-cryptographic counterpart of the in-process capability work in Capability Myths Demolished and Robust Composition - Towards a Unified Approach to Access Control and Concurrency Control — it is what those frameworks become when keys cross machine boundaries. The Lowe/PKI Layer Cake - Kaminsky Patterson Sassaman-style critiques of X.509 PKI are simultaneously arguments for SPKI-style local-name systems: parser differentials and the trust-collapse-by-CA-misissuance problem largely vanish when certificates bind authority rather than identity.

Tags

#capability-security #spki #sdsi #pki #distributed-security #authorisation #foundations

Trusted Computing Base

(page does not exist)

Access Control List

(page does not exist)

Delegation

Authorisation pattern: principal A grants B the right to act on A’s behalf, subject to restrictions. Formalised in ABLP Logic via compound principals; recurring concern in capability systems and in agent infrastructure.

In this vault

Authentication in Distributed Systems - Lampson Abadi Burrows Wobber

Role Principal

(page does not exist)

Quoting Principal

(page does not exist)

Compound Principal

In ABLP Logic and related authentication frameworks: a principal built from simpler ones by operators like as, for, and quoting, modelling Delegation and role-assumption.

In this vault

Authentication in Distributed Systems - Lampson Abadi Burrows Wobber

Says Operator

Modal operator in ABLP Logic and SDSI/SPKI: A says φ means principal A has uttered or supports proposition φ. Distinct from A believing φ; tracks attribution rather than truth.

In this vault

Authentication in Distributed Systems - Lampson Abadi Burrows Wobber

ABLP Logic

Abadi–Burrows–Lampson–Plotkin (1993) modal logic of authentication: introduces the <em>says</em> operator and a notion of compound principals for Delegation. Underlying logic of distributed authorisation systems.

In this vault

Authentication in Distributed Systems - Lampson Abadi Burrows Wobber

Speaks-For Calculus

Lampson–Abadi–Burrows–Wobber’s (1992) formalism for distributed authentication, delegation, and who is entitled to assert what on whose behalf. The primitives are says (principal A asserts statement s, written A says s) and speaks-for (A ⇒ B — anything A says, B says). The principal algebra is rich: atomic principals (users, processes, keys), conjunction A ∧ B, quoting A | B (A speaking on behalf of B), roles A as R, and for-channel A for K. Speaks-for facts are witnessed by signed certificates; authentication is checking chains of certificates from a trusted root. Access control then grants rights to principals at any level of compoundness. The calculus is the formal vocabulary underlying SPKI/SDSI, DIDs and Verifiable Credentials, modern attribute-based authorisation, and any system that needs to reason about delegated commitment.

In this vault

Authentication in Distributed Systems - Lampson Abadi Burrows Wobber — the founding paper
A Logic of Authentication — BAN Logic (1990) for protocol-level reasoning
Spi Calculus — pi-calculus with cryptography
SPKI-SDSI — capability-style PKI built on speaks-for
Decentralized Identifiers
Capability Myths Demolished
Programming Semantics for Multiprogrammed Computations — the Object Capability dual view
The Heart of Spritely - Distributed Objects and Capability Security
An Ontology for Commitments in Multiagent Systems - Singh — delegated commitments
Distributed Security
Agent Infrastructure
CBCL - Safe Self-Extending Agent Communication — signed-verdict architecture

Multi-Agent Security

The discipline of securing networks of interacting AI agents against threats that emerge from interaction — secret collusion, swarm attacks, network-effect contagion, dispersion-based stealth. Named as a distinct field by Schroeder de Witt et al. 2025.

In this vault

Agent Security

Security concerns specific to LLM-agent systems: tool attacks, prompt injection, memory poisoning, inter-agent trust failures.

In this vault

Distributed Security

Security of distributed/agent systems: mobile code, secure messaging, language-based defences.

Trusted Machine Learning Models Unlock Private Inference

Trusted Machine Learning Models Unlock Private Inference for Problems Currently Infeasible with Cryptography

Reference: Shumailov, Ramage, Meiklejohn, Kairouz, Hartmann, Balle & Bagdasarian (2025). Trusted Machine Learning Models Unlock Private Inference for Problems Currently Infeasible with Cryptography. arXiv:2501.08970 (Google Research). URL.

Summary

The paper proposes Trusted Capable Model Environments (TCMEs) — a new design point in the privacy-preserving-computation landscape, sitting between classical trusted execution environments and cryptographic protocols such as multi-party computation (MPC), homomorphic encryption, and zero-knowledge proofs. The motivating observation: capable modern ML models can plausibly play the role of the trusted third party in many private-inference scenarios that classical cryptography handles only at toy scale or not at all.

A TCME is defined by three constraints under which a capable model operates: (i) explicit input/output constraints scoping what the model is permitted to receive and emit; (ii) explicit information-flow control binding outputs to authorised data-flow channels; (iii) explicit statelessness — the model cannot retain or leak inputs across sessions. Under these constraints, even an inscrutable LLM can serve as a credible “trusted intermediary”: it computes a function of two parties’ data and reveals only the agreed output.

The authors argue TCMEs unlock private inference for problems where MPC is infeasible because the function is too rich, the inputs too large, or the spec too implicit (natural-language matching, fuzzy de-duplication, semantic agreement-checking). They walk through use cases — private record matching, contract negotiation, secret-keeping triage — and show that even classical cryptographic problems (private set intersection, secure multi-party comparison) admit TCME implementations that scale further than current MPC. The paper closes with the limitations: trust in TCMEs reduces to trust in the model+hardware+policy stack; statelessness must be engineered, not assumed.

Key Ideas

TCME definition: a capable ML model + explicit I/O constraints + explicit information-flow control + explicit statelessness.
Trusted-third-party substitution: the model fills the role MPC traditionally requires a non-colluding cryptographic protocol to enact.
Coverage envelope: TCMEs handle privacy problems too rich or too implicit for current MPC (semantic matching, fuzzy agreements, natural-language contracts).
Bridge to cryptography: even classical PSI/comparison protocols can be implemented as TCMEs — sometimes more efficiently.
Statelessness is engineered: memory leaks, side channels, and re-training contamination are the real attack surface, not the model logic.
Trust composition: TCME trust assumption = trust(model) ∧ trust(hardware) ∧ trust(policy enforcement).
Use cases sketched: private record matching, negotiation, triage, search over private corpora, semantic compliance checks.

Connections

Conceptual Contribution

Claim: Capable ML models, operated under explicit information-flow and statelessness constraints, can act as trusted third parties for private-inference problems that classical cryptography cannot scale to. This expands the realm of feasible privacy-preserving computation beyond MPC’s current envelope.
Mechanism: Define Trusted Capable Model Environments (TCMEs): model + explicit I/O constraints + explicit IFC + explicit statelessness. Demonstrate via use cases that TCMEs solve both novel privacy problems (semantic matching) and re-instantiate classical ones (PSI) at scales MPC cannot reach.
Concepts introduced/used: Trusted Capable Model Environment, Trusted Third Party, Information Flow Control, Private Inference, Statelessness (Privacy), Multi-Party Computation
Stance: position / architectural proposal
Relates to: Direct companion to NDAI Agreements — both treat TEE+AI or model+constraints as a substrate for previously infeasible commitment / privacy primitives. Provides the technical substrate that Privacy Reasoning in Ambiguous Contexts reasons about behaviourally and that Infrastructure for AI Agents would expose as governance infrastructure. Complementary to Defeating Prompt Injections by Design’s CaMeL: both treat the agent as a constrained reasoner whose outputs are gated by information-flow policy.

NDAI Agreements

Reference: Stephenson, Miller, Sun, Annem & Parikh (2025). NDAI Agreements. arXiv:2502.07924 (UIUC; Cornell Tech; et al.). URL.

Summary

The “NDAI agreement” — non-disclosure AI agreement — is a mechanism in which a TEE combined with an AI agent jointly stands in for a trusted human intermediary, resolving the classical disclosure–appropriation paradox of information markets first identified by Arrow (1962) and Nelson (1959). An inventor cannot reveal an idea to a potential investor without risking misappropriation; without revealing it, no efficient bargain can be struck. The result is well-known: under-disclosure, under-investment, under-licensing.

Stephenson et al. show formally — via a buyer/seller bargaining game — that delegating the disclosure-and-payment decision to a tamper-proof program running inside a TEE eliminates the hold-up problem, achieving full disclosure and an efficient ex post transfer. When the invention’s value exceeds the value a TEE can fully secure (e.g. because some leakage is unavoidable), partial disclosure still strictly improves welfare over the no-disclosure equilibrium. They then model agent error — payments or disclosures going wrong — and prove that simple safeguards (budget caps, acceptance thresholds) preserve most of the efficiency gains.

The substantive economic claim is that TEE + AI behave as an “ironclad NDA”: a credible commitment device for the disclosure problem that was previously unattainable with paper contracts (because expropriation is unverifiable) or with cryptography alone (because invention value is unbounded and the seller’s information is a complex unstructured artefact). The result links the Mechanism Design / Hold-Up Problem tradition to AI-agent infrastructure, and gives a sharp theoretical case for the economic value of trusted model environments and confidential-compute hardware as agent-economy substrates.

Key Ideas

Formalises the Arrow–Nelson information paradox / hold-up problem in a bargaining model between seller (inventor) and buyer (investor).
TEEs + AI agents delegate disclosure and payment to tamper-proof programs that neither party can subvert; this implements an ex-ante commitment device unavailable under classical contracts.
Full-disclosure efficient equilibrium under the NDAI when the invention’s value lies within what the TEE can secure.
Partial disclosure dominates no-disclosure even when full security is impossible: high-value inventions still get partially revealed in welfare-improving ways.
Models agent imperfection: errors in payment or disclosure can occur; budget caps and acceptance thresholds bound the damage and preserve most welfare.
Frames TEEs+AI as an “ironclad NDA”: a cryptographically/hardware-enforced commitment that traditional NDAs cannot match.
Policy implications for R&D Commercialisation, Technology Transfer, and inter-firm collaboration; bridges economic theory to confidential-compute hardware.

Connections

Conceptual Contribution

Claim: A trusted execution environment hosting an AI agent can serve as a credible commitment device that solves the classical Arrow–Nelson disclosure problem of information markets — achieving full disclosure and efficient transfer where paper NDAs and pure cryptography both fail.
Mechanism: A bargaining model in which TEEs+AI mediate the disclosure-and-payment decision; closed-form characterisation of equilibria for full and partial disclosure; sensitivity analysis to agent error with policy-instrument bounds (budget caps, acceptance thresholds).
Concepts introduced/used: NDAI Agreement, Trusted Execution Environment, Hold-Up Problem, Arrow Information Paradox, Mechanism Design, Commitment Device, Disclosure Game
Stance: formal economic theory with technical implications
Relates to: Companion to Trusted Machine Learning Models Unlock Private Inference — both argue that capability + trusted execution can replace previously infeasible cryptographic primitives. The economic counterpart to the engineering catalogue in Infrastructure for AI Agents; a building block for the markets imagined in Virtual Agent Economies and the information-asymmetry resolution explored in Language Models Can Reduce Asymmetry in Information Markets. Sits in the lineage of Vickrey / mechanism-design tradition.

Infrastructure for AI Agents

Reference: Chan, Wei, Huang, Rajkumar, Perrier, Lazar, Hadfield & Anderljung (2025). Infrastructure for AI Agents. TMLR (accepted). arXiv:2501.10114 (Centre for the Governance of AI; Oxford; ANU; Toronto). URL.

Summary

The paper proposes the concept of agent infrastructure: the technical systems and shared protocols, external to any individual agent, that mediate how agents interact with each other, with humans, and with institutions. The argument is by analogy to the Internet: a network of capable agents requires its own equivalent of TLS, DNS, X.509, BGP, and HTTP — because most safety properties of multi-agent ecosystems cannot be obtained by behavioural training of any individual model.

Chan et al. identify three functions agent infrastructure should serve. (1) Attribution — binding actions, properties, and credentials to specific agents and to the humans or institutions accountable for them, via agent IDs, attestations, and audit logs. (2) Interaction shaping — efficient inter-agent communication protocols, agreement formation, mechanism design for resource allocation, and reputation systems. (3) Detection and remediation — monitoring for harmful behaviour and providing mechanisms to roll back, contain, or compensate for damage.

For each function the paper sketches research directions, candidate adoption paths, relationships to existing internet infrastructure, and open problems. The framing is deliberately governance-first: infrastructure exists not to make agents more capable but to keep their externalities tractable as deployment scales. The paper is now the standard citation for the agent-governance / agent-infrastructure thread underlying Model Context Protocol, Agent-to-Agent Protocol, Agent Network Protocol, and emerging “agent passport” / verifiable-credential proposals.

Key Ideas

Agent infrastructure as governance layer: external technical systems mediating agent interactions — distinct from training-time alignment.
Three functions: attribution; interaction shaping; detection & remediation. Each maps to concrete research directions.
Attribution: agent IDs, verifiable credentials, attestations, audit logs, principal-binding (which human/org owns this agent).
Interaction shaping: inter-agent communication protocols; standardised agreement primitives; mechanism design; reputation.
Detection & remediation: anomaly detection on agent traffic; rollback mechanisms; insurance / compensation rails; “kill switch” governance.
Analogy to Internet protocols (HTTPS, DNS, BGP, X.509): infrastructure adoption is path-dependent, requires standardisation bodies, and trades expressivity for safety properties.
Open questions: who issues credentials, how privacy interacts with attribution, how to bootstrap adoption, what is enforceable cross-jurisdiction.

Connections

Conceptual Contribution

Claim: Many of the safety, accountability, and interoperability properties society will need from AI agents are not properties of any individual model — they live in the infrastructure between agents. Just as the Internet’s safety depends on TLS / DNS / BGP rather than on any single application, agent ecosystems will depend on agent-level analogues: attribution, interaction shaping, and detection-and-remediation infrastructure.
Mechanism: A three-function taxonomy (attribution / interaction-shaping / detection-and-remediation) with a catalogue of candidate primitives — agent IDs, verifiable credentials, inter-agent protocols, certification regimes, reputation systems, rollback mechanisms — plus analysis of adoption pathways relative to existing internet infrastructure.
Concepts introduced/used: Agent Infrastructure, Agent ID, Verifiable Agent Credentials, Inter-Agent Protocols, Action Attribution, Agent Reputation, Agent Rollback, AI Governance
Stance: governance / position paper / research-agenda
Relates to: Provides the governance scaffolding within which Open Challenges in Multi-Agent Security threats must be addressed; the institutional counterpart to Virtual Agent Economies’s economic framing; concrete protocols proposed include Model Context Protocol, Agent-to-Agent Protocol, Agent Network Protocol — surveyed alongside in Survey Of AI Agent Protocols and Survey Of Agent Interoperability Protocols. The attribution leg connects to NDAI Agreements (TEEs as a particular attribution / commitment substrate) and Trusted Machine Learning Models Unlock Private Inference (capable models as a trust substrate).

A Commitment-Based Approach to Agent Communication

Reference: Fornara, N. & Colombetti, M. (2004). Applied Artificial Intelligence 18(9–10): 853–867. DOI: 10.1080/08839510490509054. The journal article is paywalled; the open-access AAMAS-02 conference precursor — Operational Specification of a Commitment-Based Agent Communication Language (pp. 535–542) — captures the same model and is the locally archived source. Source file: fornara-colombetti-aamas02.pdf. URL

Summary

Fornara and Colombetti develop an object-oriented operational semantics for an Agent Communication Language grounded entirely in social commitments, intended for open environments populated by self-interested, heterogeneous agents who cannot be assumed to share an honest mental architecture. A Commitment is an abstract data type with fields Identifier, Debtor, Creditor, State ∈ {empty, cancelled, precommitment, conditional, active, fulfilled, violated}, Content (a temporal proposition), Condition (another temporal proposition), and Time-out. Its evolution is given by an explicit finite-state machine driven by two kinds of transitions: agent-invoked methods (mc, mp, ap, cc, cp, rp) and event-driven update rules triggered when the truth value of the content or condition resolves.

The authors’ key innovation over the Yolum-Singh treatment is the precommitment state, which models the social situation a directive speech act creates: the speaker cannot directly commit the hearer, so a request instantiates a precommitment whose debtor is the hearer; the hearer either accepts it (turning it into an active or conditional commitment), rejects it, fulfills it implicitly by performing the action, or lets the time-out elapse. This machinery yields uniform commitment-based definitions for Searle’s main illocutionary categories — assertives (inform, informIf, informRef), commissives (promise, conditionalPromise), and directives (request, conditionalRequest, accept, reject, yes/noQuestion, whQuestion) — and lets a propose act be defined compositionally as a conditional request conjoined with a conditional promise. A worked auction-style proposal protocol is given as an interaction diagram whose state contents are computed from the speech-act definitions, and whose soundness is checked by requiring that all final-state commitments be empty, fulfilled, or violated.

Key Ideas

Commitment-as-object: a commitment is an abstract data type with a state in {e, c, p, cc, a, f, v} whose dynamics are described by an explicit FSM.
Temporal proposition class: the content/condition of a commitment is a sentence + time interval + ∀/∃ mode + state, resolved by a domain “notifier” — separating what is committed from when and how its truth is observed.
Precommitment models directive speech acts: a request creates C(p, hearer, speaker, P|Q) that the hearer can accept (ap), reject (rp), implicitly fulfil (update rule 5), or let time out.
Conditional commitment with a temporal condition becomes active when the condition is satisfied and is automatically cancelled if the condition fails.
Five update rules link the truth-state of content and condition propositions to commitment-state transitions (active→fulfilled/violated, conditional→active/cancelled, precommitment→fulfilled).
Searle’s taxonomy of illocutionary acts is recovered by composition: inform, promise, request, accept/reject, yes/noQuestion, whQuestion, propose.
Soundness of an interaction protocol is checked by an interaction diagram in which every final state’s commitments are empty, fulfilled, or violated — a structural correctness criterion for negotiation protocols.
The notion of a conversational commitment (a meta-commitment to react to interlocutor speech acts) is sketched as the principled justification for the time-out field.

Connections

Conceptual Contribution

Claim: Speech-act semantics for an ACL should be specified operationally — as state-machine transitions over a public commitment data type — so that meaning is independent of any agent’s internal mental architecture, observable to third parties, and compositional across the speech-act taxonomy; in particular, the directive family requires a dedicated precommitment state because no agent can unilaterally commit another.
Mechanism: Define an abstract Commitment class with seven explicit states and a transition FSM driven by methods (mc/mp/ap/cc/cp/rp) plus five event-driven update rules that read truth-states of Temporal Proposition objects; define each Searle category by a single-line operation on commitment objects (inform := mc(a,b,P,T), request := mp(a,b,P,T), propose := conditionalRequest ∧ conditionalPromise, etc.); validate interaction protocols structurally via a state-content interaction diagram in which final-state commitments must all be empty/fulfilled/violated.
Concepts introduced/used: Commitment, Social Commitment, Precommitment, Conditional Commitment, Temporal Proposition, Commitment-Based Protocol, Commitment-based Semantics, Public Semantics, Verifiable Semantics, Speech Act Theory, Directives, Conversation Protocols, Interaction Protocols, Open Multi-Agent Systems, Conversational Commitment
Stance: formal-semantic / engineering
Relates to: Closest neighbour is Flexible Protocol Specification and Execution (Yolum & Singh, AAMAS-02) — the authors explicitly compare the two approaches: where Yolum-Singh use the Event Calculus and an abductive planner over create/discharge/cancel/release/assign/delegate, Fornara-Colombetti use an OO/FSM data type and add the precommitment apparatus to cover directives. Both belong to the social-semantics programme catalysed by ACL Rethinking Principles and formalised verifiability-style by Verifiable Semantics for ACLs; both are subsumed under the role-based unification of A Common Ontology Of ACLs. Repudiates the mentalistic line of FIPA-ACL / Intention Is Choice with Commitment for interoperable ACL semantics while keeping speech-act theory (Speech Acts - An Essay in the Philosophy of Language, A Taxonomy of Illocutionary Acts) as the organising taxonomy. The 2004 Applied AI version this entry primarily cites elaborates the AAMAS-02 model with extended treatment of negotiation protocols and the soundness-via-conversational-commitment programme that the authors’ later artificial-institutions work develops.

Tags

Proof-Carrying Code - Necula

Proof-Carrying Code

Reference: Necula, G. C. (1997). Proof-Carrying Code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97), Paris, January 1997, pp. 106–119. ACM. URL (author’s Berkeley page, original PostScript) · URL (Illinois course PDF mirror) · DOI (ACM)

Summary

Proof-Carrying Code (PCC) is the architectural ancestor of every “ship a proof with the artefact, verify the proof rather than re-deriving safety from scratch” pattern in the modern security stack — including CBCL’s R4 split (host runs a small certified verifier on each dialect contract proof), CIVeX certificates (causal-identifiability artefacts shipped from prover to host), BAN-style protocol soundness certificates, and TEE attestations. The premise is direct: untrusted code arrives at a host that must run it under a safety policy (no out-of-bounds memory access, no division by zero, no privilege escalation, only sanctioned syscalls). Re-deriving safety on every load is expensive (general program analysis is undecidable, conservative approximations reject too much real code) and shifts trust onto the host’s analyser. PCC inverts the burden: the code producer generates a machine-checkable proof that the code respects the policy, and the code consumer checks the proof. Proof checking is mechanical, syntactic, decidable, and cheap; proof finding (the work that produced the proof) is hard and lives on the producer’s side.

The technical content of the paper is the framework that makes this practical. Necula defines a safety policy as a set of rules in a first-order theory over machine states; programs come accompanied by a safety predicate whose proof in this theory entails the policy. Proofs are encoded in a logical framework (LF / Edinburgh Logical Framework), so the proof-checker is a single, small, generic LF type-checker independent of the safety policy. Necula demonstrates the architecture on a packet-filter benchmark: a Berkeley Packet Filter untrusted assembler program is verified to terminate, stay in bounds, and call no syscalls — by checking ~5 KB of LF proof against the BPF policy, in milliseconds. The signal is that the verifier is tiny and policy-parameterised; safety becomes a function of proof checkability rather than of expensive whole-program analysis.

For the security agenda this vault tracks, PCC is foundational in three respects. First, it generalises capability-secure thinking (Dennis & Van Horn 1966, Shapiro et al.) from access control to behavioural conformance: the proof is a behavioural capability the producer holds, the verifier is the gatekeeper. Second, it operationalises Rice’s theorem in a constructive direction — Rice says semantic properties of arbitrary programs are undecidable, but PCC shows that with a proof in hand, checking that the proof establishes the semantic property is trivial. Third, it is the architectural pattern that CBCL’s R4 split inherits literally: a CBCL dialect contract is the code, a Lean 4 proof that the contract is well-formed and policy-respecting is the certificate, and the host’s small Lean kernel check is the PCC verifier. The discussion section of any CBCL/CIVeX paper should cite PCC explicitly.

Key Ideas

Ship the proof with the artefact: the code producer (who knows why the code is safe) generates a proof; the code consumer checks the proof. Proof-checking is cheap, mechanical, syntactic, and decidable; the finding of proofs is hard and lives on the producer’s side.
Safety policy = first-order theory: a safety policy is a set of inference rules in a first-order theory over machine states and operations. Programs come with a safety predicate; a proof of the predicate in the theory entails the policy.
Logical Framework as the proof carrier: proofs are LF terms (Edinburgh Logical Framework). The verifier is an off-the-shelf LF type-checker — small, generic, policy-parameterised. Trusted code base: the LF type-checker plus the policy rules.
Asymmetry of effort: producer effort scales with program complexity; consumer effort scales with proof size, which is bounded by program size in practice but does not depend on the difficulty of the underlying analysis.
Decoupling of policy from verifier: changing the safety policy means changing the inference-rule set; the LF checker is reused unchanged. New policies can be deployed without re-validating the verifier.
No trust in the producer: a malicious producer can submit malicious code, but cannot generate a verifiable proof for it (under soundness of the policy). The producer is untrusted; the verifier is the trust anchor.
Packet-filter benchmark: BPF programs, originally trusted via interpretation in a kernel sandbox, are PCC-verified to be safe to run as native code. Verification cost drops from microseconds-per-packet (interpreter) to a one-time millisecond proof check at load time.
Generalises to many policies: type safety, memory safety, resource bounds, information-flow control, even fine-grained behavioural contracts — all expressible as PCC safety policies.

Connections

Conceptual Contribution

Claim: Safe execution of untrusted code under a stated safety policy can be achieved by having the code producer ship a machine-checkable proof of policy compliance with the code, and having the code consumer check the proof rather than re-derive safety. This inverts the standard burden: hard-to-derive properties become trivial-to-check given the right artefact.
Mechanism: Express the safety policy as a first-order theory over machine states; require submissions to include a proof of the program’s safety predicate; encode proofs in a Logical Framework (LF) so the consumer-side checker is a generic LF type-checker independent of the policy. The trusted code base is the LF checker plus the policy rules; the producer is untrusted. Demonstrated on the Berkeley Packet Filter, where PCC verification runs in milliseconds at load and replaces interpreter-based sandboxing.
Concepts introduced/used: Proof-Carrying Code, Safety Policy, Safety Predicate, Logical Framework (LF), Producer-Consumer Asymmetry, Verifier, Trusted Code Base, Behavioural Capability.
Stance: foundational technical paper / architectural pattern.
Relates to: The architectural ancestor of CBCL’s R4 split — dialect contracts are shipped with Lean 4 proofs of well-formedness and policy compliance; the host’s small Lean kernel check is the PCC verifier. PCC is the citation for “ship the proof, check the proof.” Operationalises Rice’s theorem in a constructive direction: undecidable in general, decidable with the producer’s proof in hand. The natural pair is Schneider 2000 — Schneider characterises which policies are enforceable by trace monitoring; PCC characterises how a code consumer can verify static policies without re-deriving them. The verification heritage runs through Hoare 1969 / Floyd (axiomatic semantics and inductive assertions) to PCC’s LF-encoded proofs. The LangSec tradition (Sassaman et al.) is the dual move: restrict the input language so safety becomes decidable without a producer-side proof. CBCL combines both: a DCFL surface (LangSec) with proof-carrying dialect contracts (PCC).

Enforceable Security Policies - Schneider

Enforceable Security Policies

Reference: Schneider, F. B. (2000). Enforceable Security Policies. ACM Transactions on Information and System Security (TISSEC) 3(1): 30–50. February 2000. URL (Schneider’s Cornell page) · DOI

Summary

Schneider’s paper is the theoretical backdrop for trace-monitor enforcement — the move that takes a stated security policy and asks, formally, can this policy be enforced by a mechanism that observes program execution one step at a time and halts execution if a violation is about to occur? The answer is only if the policy is a safety property: precisely, the policies enforceable by an execution monitor (EM) are exactly those whose violations are finite-prefix detectable. Liveness properties — “good thing eventually happens” — cannot be enforced by monitoring, because no finite prefix witnesses violation. Schneider formalises EM enforcement as a class of security automata — automata that read the program’s execution one event at a time, transitioning over states that encode the policy’s history, and halting the program upon entering a no-good state.

The result has three teeth. First, it gives a precise, decidable characterisation of the enforceable policies: EM-enforceable iff specifiable as a safety property over execution traces. Second, it cleanly separates the policy (the security automaton) from the mechanism (the EM machinery that interposes between the program and its environment), so the same EM machinery can enforce many policies by swapping the automaton. Third, it lays the groundwork for inlined reference monitors and security-typed languages (Schneider’s later work with Erlingsson on SASI, Ligatti–Bauer–Walker on edit automata that generalise EM with transformation in addition to halting).

For the architecture this vault tracks, Schneider is the formal warrant for CBCL’s R5 monotone-verdict trace monitor and for session-type monitorability in general. CBCL’s invariant — only emit monotone verdicts — is the safety-property restriction: a CBCL verdict is a finite-prefix witness, the verdict ledger is the security automaton’s state, and the host’s enforcement is precisely an EM in Schneider’s sense. The paper also bounds what CBCL cannot do: liveness properties (every commitment is eventually discharged) are not EM-enforceable, only EM-monitorable for violation of safety lower bounds (e.g. a deadline expires → record commitment broken). The CBCL discussion section should cite Schneider for the formal precision and Ligatti–Bauer–Walker for the edit-automaton generalisation if transformations are wanted.

Key Ideas

Execution Monitor (EM) enforcement: a mechanism that observes program execution one event at a time and halts execution if continuing would violate the policy. Standard examples: reference monitors, system-call interposition, security wrappers.
Safety-property characterisation: EM-enforceable policies are exactly the safety properties — properties whose violations are detectable on a finite prefix of execution. Liveness properties cannot be EM-enforced.
Security automata: a formal model for EM enforcement. A security automaton is a (possibly infinite-state) automaton that reads execution events, maintains policy-relevant history, and transitions to a “no-good” state on violation; the EM halts the program at that point.
Policy / mechanism separation: the security automaton specifies what is enforced; the EM machinery enforces how. Swapping automata changes the policy without changing the enforcement infrastructure.
Liveness is out of scope: properties like “every request is eventually served” cannot be EM-enforced because no finite prefix witnesses violation. They can be monitored for violation of finite-bounded safety approximations (e.g. timeout-deadline as a safety surrogate).
Anti-Rice (constructively): Rice tells us most semantic properties of programs are undecidable, but EM enforcement sidesteps Rice by limiting attention to properties expressible as runtime-checkable trace predicates rather than as program properties.
Genealogical successors: Ligatti–Bauer–Walker edit automata generalise EM by allowing the monitor to transform events (insert, suppress, replace), enlarging the enforceable class beyond pure safety to certain renewal properties; inlined reference monitors (Erlingsson–Schneider SASI) move the EM machinery into the program text itself.

Connections

Conceptual Contribution

Claim: A security policy can be enforced by an execution monitor (a mechanism that observes one event at a time and halts on impending violation) iff it is a safety property — i.e., its violations are detectable on a finite prefix of execution. Liveness properties cannot be EM-enforced.
Mechanism: Define EM enforcement formally: a (possibly infinite-state) security automaton reads execution events, maintains policy-relevant history, transitions on each event, and signals “no-good” on violation; the EM halts the program at the signalling step. Show that the class of policies so enforceable is exactly the safety properties (in the Alpern–Schneider sense). Separate the automaton (policy) from the EM machinery (mechanism), enabling policy-parametric enforcement.
Concepts introduced/used: Execution Monitor (EM), Security Automaton, Safety Property, Liveness Property, Trace Property, Inlined Reference Monitor, Edit Automaton (Ligatti–Bauer–Walker generalisation).
Stance: foundational technical paper.
Relates to: The formal warrant for CBCL’s R5 monotone-verdict trace monitor — CBCL verdicts are finite-prefix witnesses, the verdict ledger is the security automaton’s state, and host-side enforcement is exactly an EM. The paper also bounds what trace-monitor enforcement can do: liveness properties (every commitment eventually discharged) are not enforceable, only approximable via timeout-deadline safety surrogates. Pairs naturally with Necula’s PCC (static proof-bearing artefacts) — Schneider tells you which dynamic properties are runtime-monitorable, PCC tells you which static properties can be discharged at load time by a proof-checker. The genealogical successors are inlined reference monitors (Erlingsson–Schneider), edit automata (Ligatti–Bauer–Walker), and the entire runtime-verification literature. The LangSec pair is conceptually adjacent: LangSec restricts the input language so safety is decidable at parse time; Schneider’s EM restricts the enforced policy class so safety is decidable at runtime. monitorability of session types is the direct session-type analogue. The deeper conceptual map: Schneider is to runtime enforcement what Hoare is to static specification and PCC is to load-time proof-checking.

The Protection of Information in Computer Systems

Reference: Jerome H. Saltzer, Michael D. Schroeder (1975). Proceedings of the IEEE, 63(9):1278-1308. Source file: saltzer-schroeder-1975.pdf. URL

Summary

The foundational tutorial on information protection in computer systems, concentrating on the architectural structures (hardware and software) necessary to support protection. Organised as three sections: (I) basic principles, functions and elementary protection/authentication mechanisms; (II) descriptor-based protection architectures and the relation between capability systems and access-control-list systems; (III) state of the art and research projects.

The paper is most remembered for its eight design principles (economy of mechanism, fail-safe defaults, complete mediation, open design, separation of privilege, least privilege, least common mechanism, psychological acceptability). It gives precise definitions for principal, capability (“an unforgeable ticket”), access control list, domain, protected subsystem, confinement, and distinguishes discretionary from nondiscretionary controls. Saltzer and Schroeder frame the tension between capability-oriented (ticket-oriented) and list-oriented systems that still shapes modern access control.

Key Ideas

Three categories of violation: unauthorized information release, unauthorized modification, unauthorized denial of use
Eight design principles for protection mechanisms (least privilege, fail-safe defaults, complete mediation, etc.)
Functional taxonomy: unprotected / all-or-nothing / controlled sharing / user-programmed sharing
Capability (“ticket-oriented”) vs. access-control-list (“list-oriented”) as dual descriptor structures
Protected subsystems as encapsulated domains with controlled entry points
Authentication vs. authorization distinction; the notion of principal as the unit of accountability
Confinement problem: preventing a borrowed program from leaking the data it accesses

Connections

Conceptual Contribution

Claim: Protection is not a bag of techniques but an architectural discipline; a small set of design principles (especially least privilege, fail-safe defaults, complete mediation, economy of mechanism) together with the capability/ACL descriptor abstraction is sufficient to organise the design space of secure systems.
Mechanism: Descriptor-based protection: every access to a protected object passes through a descriptor (capability or ACL entry) managed by a reference monitor. Protected subsystems encapsulate data with domain-specific procedures callable only at designated entry points. Principals are authenticated once; authorization is then mediated per access.
Concepts introduced/used: Principle of Least Authority (least privilege), Capability Security, Object Capability Security, Ambient Authority (as an antipattern), Confused Deputy (implicit in the delegation discussion), access control list, protected subsystem, confinement, complete mediation, fail-safe defaults, separation of privilege, economy of mechanism, psychological acceptability.
Stance: engineering / systems — normative architectural guidance grounded in Multics experience.
Relates to: Provides the vocabulary used by Object Capability Security and Capability Security work (Dennis & Van Horn, Hydra, KeyKOS, EROS, Capsicum). Its least-privilege principle underlies Principle of Least Authority, and its critique of pervasive authority is the ancestor of Ambient Authority and Confused Deputy analyses. The architectural posture prefigures End-to-End Arguments in System Design (Saltzer again) and is philosophically aligned with LangSec’s call for narrow, verifiable interfaces. Fundamental to Distributed Security.

Tags

Distributed Electronic Rights in JavaScript

Reference

Miller, Mark S.; Van Cutsem, Tom; Tulloh, Bill. “Distributed Electronic Rights in JavaScript.” In Programming Languages and Systems - 22nd European Symposium on Programming (ESOP 2013). LNCS 7792, pp. 1-20, Springer, 2013. URL

Summary

This ESOP 2013 paper reports on the effort to turn JavaScript into the ubiquitous distributed object-capability fabric for smart contracts and erights (electronic rights). JavaScript already has ubiquity, a memory-safe object model, and first-class functions with lexical closure; what it lacks, the authors argue, is the three missing ingredients for robustly composing mutually suspicious code across machines: a secure subset, a promise-based distributed object model, and persistent resilience. These are provided respectively by SES (Secure EcmaScript, an ocap subset of ES5), the Q promise library (distributed-JS with eventual-send !), and NodeKen (distributed orthogonal persistence on Node.js, built atop the Ken system). Together they form Dr. SES - Distributed Resilient Secure EcmaScript.

The paper walks through the whole stack. SES freezes primordials, whitelists globals, and makes def(obj) produce defensively consistent tamper-proof records. confine(src, endowments) safely evaluates untrusted JS with a supplied endowments record, giving first-class mobile-code capability security. The Q library adds ! (eventual-send) so that p!getX() sends a message to whatever p will designate when resolved - this is promise pipelining, generalised to remote and failed promises. NodeKen provides “every message ever sent will be delivered in order exactly once,” allowing programmers to ignore partition and crash.

The demonstration is a 42-line escrow exchange contract: two mutually suspicious parties wish to swap goods/money via an untrusted escrow agent, and the Dr. SES code expresses the contract clearly and executes safely across distributed JS event loops. This paper is the crucial bridge between Miller’s E tradition and the modern web - its ideas flow directly into the TC39 proxies proposal, ECMAScript frozen realms, hardened-JS / LavaMoat, Agoric’s Zoe, and the MetaMask / secure-ECMAScript supply-chain work.

Key Ideas

Dr. SES = SES + Q + NodeKen: secure ocap JS + distributed promises + orthogonal persistence.
SES: ocap subset of ES5 - frozen primordials, whitelisted globals, powerless-by-default imports, def() for defensive consistency, confine() for safe mobile code.
Eventual-send !: target!method(args) is a non-blocking message-send returning a promise; distribution-transparent.
Promise pipelining as the basic async composition: chained .then on a remote promise reduces round-trips.
Defensively consistent objects: maintain invariants despite malicious clients.
WeakMap for rights amplification: identity-keyed tables let a facet holder recover the full object.
Escrow exchange in 42 lines: demonstrates that non-trivial smart contracts become pedagogically small under the right fabric.
NodeKen / Ken: survives crashes and partitions by orthogonal checkpointing, so distributed programmers can reason as if messages were reliable.

Connections

The Heart of Spritely - Distributed Objects and Capability Security - Spritely’s ocapN and Goblins are the Guile-side reincarnation of Dr. SES principles.
E Language - Dr. SES is E’s design translated into JavaScript.
CapTP - Q’s eventual-send over the wire is a CapTP-spirit protocol.
Capability Security, Object Capability Security
Ambient Authority - SES’s frozen-globals / powerless-imports directly attacks ambient authority in JS.
Confused Deputy - confine() with explicit endowments is an anti-confused-deputy idiom.
Principle of Least Authority - endowments are POLA made concrete.
Distributed Security
Security Kernel Lambda Calculus
A Universal Modular Actor Formalism for Artificial Intelligence
Actor Model
Vat Model - each JS event loop is a vat.
Promise Pipelining - Q is the mass-market pipelining library.

Conceptual Contribution

Robust Composition - Towards a Unified Approach to Access Control and Concurrency Control

Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control

Reference

Miller, Mark Samuel. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD Dissertation, Johns Hopkins University, May 2006. Advisor: Jonathan S. Shapiro. Readers: Scott Smith, Yair Amir. URL

Summary

Mark Miller’s dissertation is the foundational synthesis of the object-capability tradition. It argues that the act of composing separately written programs so that they cooperate rather than destructively interfere is the fundamental problem that has limited the scale and functionality of software systems. The thesis proposes a unified framework that binds together access control and concurrency control as two faces of the same compositional discipline: each message send is at once an authority-propagation event and a concurrency-interleaving event, and both must be disciplined together if we are to compose code written by mutually suspicious authors on mutually suspicious machines.

Miller extends decades of object-oriented progress from its comfortable setting (sequential, single-machine, benign components) to the hostile general case: concurrent, distributed, and potentially malicious components. The vehicles for this are the E programming language - a distributed, persistent, object-capability language built around vats, near/far references, eventual-send, promise pipelining, and CapTP - and CapDesk, a virus-safe desktop built in E. Together E and CapDesk form working embodiments of the thesis: authority is only granted by reference-passing along the message graph, and concurrency hazards (deadlock, non-determinism, plan interference) are tamed by the communicating-event-loop / vat model rather than by shared-memory locks.

The dissertation pulls together and formalises the lineage from Dennis & Van Horn, Hardy’s confused deputy, KeyKOS/EROS, Actor-model eventual send, and the SPKI/Granovetter diagram tradition, and it is by far the most-cited reference for object-capability security. Its substantive chapters cover attenuating authority, distributed concurrency control, promise pipelining, the “excess authority as gateway to abuse” argument, and the POLA design discipline.

Key Ideas

Unification of access and concurrency control: both are consequences of disciplining what one object can do to another across a message send.
Object-capability model: authority == what references you hold; “only connectivity begets connectivity.”
Vats and communicating event loops: each vat is a single-threaded turn-taking event loop; cross-vat calls are eventual sends returning promises.
Promise pipelining: chained messages to not-yet-resolved promises reduce round-trips and compose naturally as plans.
CapTP: the cryptographic capability transport protocol that preserves object-capability semantics across mutually-suspicious machines.
Defensive consistency: an object defends its own invariants against arbitrary clients.
POLA as design discipline: hand out only the authority actually needed for each delegation.
CapDesk: demonstrates that a virus-safe desktop is achievable by threading object-capabilities through the UI/shell layer (powerboxes, caplets).

Connections

The Heart of Spritely - Distributed Objects and Capability Security - Spritely is the direct modern successor carrying Miller’s E design forward into Goblins/Guile.
E Language - E is the concrete language Miller designs and evaluates here.
CapTP - Miller’s distributed capability transport, specified in detail.
Capability Security and Object Capability Security - this thesis is the canonical statement of the ocap model.
Ambient Authority - Miller’s thesis is the source of the modern critique of ambient authority.
Confused Deputy - Miller reframes Hardy’s confused-deputy problem as a composition failure.
Principle of Least Authority - POLA is given its definitive formulation here.
Distributed Security - the thesis generalises ocap security to distributed settings.
Security Kernel Lambda Calculus - close kin in the formal-ocap tradition.
A Universal Modular Actor Formalism for Artificial Intelligence - the Actor model is one of E’s direct intellectual ancestors.
Actor Model - vats and eventual sends are the ocap-refined descendants of Hewitt’s actors.
Vat Model - the vat abstraction is introduced and justified here.
Promise Pipelining - Miller gives the definitive account of pipelining in this thesis.

Conceptual Contribution

The Confused Deputy - Hardy

The Confused Deputy (or why capabilities might have been invented)

Reference

Hardy, Norm. “The Confused Deputy (or why capabilities might have been invented).” ACM SIGOPS Operating Systems Review, 22(4):36-38, October 1988. URL

Summary

Norm Hardy’s three-page note is the single most quoted security story in the capability tradition. It is a “nearly true” anecdote from roughly 1974 at Tymshare. A FORTRAN compiler, stored in directory SYSX, writes statistics to (SYSX)STAT and is therefore granted home files license - the ambient authority to write any file in SYSX. Users invoke the compiler as RUN (SYSX)FORT and may supply the name of a file in their own directory for optional debugging output. One day, a user passes (SYSX)BILL - the system billing file - as the output filename. The compiler, running with its SYSX authority, dutifully opens (SYSX)BILL for write and clobbers it. The billing data is lost.

Hardy walks through the standard reactions (blame the compiler, add a check for sensitive filenames, recategorise files, enumerate forbidden names) and shows that each misses the point. The compiler has been delegated authority it did not ask for and cannot distinguish: it cannot tell whether a request to write (SYSX)BILL comes from its own invariant need to write STAT (authority inherent to the compiler) or from the invoker’s request channel (authority inherent to the invoker). The compiler is acting as deputy for two different principals - itself and its invoker - with two different authorities, but the operating system gives it only one aggregated authority set with no way to trace which request justified which use.

The capability fix, Hardy explains, is to pass each authority as a capability at the point of need rather than to aggregate them ambiently on the compiler process. The invoker passes a capability to the output file; the compiler holds a separate capability to the statistics file; no ASCII pathname walk ever happens against an ambient authority. The Tymshare/KeyKOS team built KeyKOS on precisely this discipline. Hardy’s essay is the canonical demonstration of why ACL-plus-pathname operating systems have a structural bug (the confused deputy) that capability operating systems avoid by construction.

Key Ideas

Confused deputy: an authorised program manipulated by a less-authorised invoker into wielding its own greater authority on the invoker’s behalf.
Ambient authority is the underlying cause: the compiler’s SYSX home-files-license is in effect whenever the compiler runs, independent of which request is in flight.
Two principals, one process: the compiler serves its own goals and the invoker’s, with distinct authorities that the OS conflates.
Designation vs. authority: a filename in ACL systems is a pure designator; authority comes from who-is-running. In capability systems the capability is the designator-with-authority - no conflation possible.
Capabilities as the fix: present-tense authority via capability arguments eliminates the confusion.
KeyKOS is offered as the system built on precisely this discipline, with factories defeating Trojan horses and confined subsystems.

Connections

The Heart of Spritely - Distributed Objects and Capability Security
Confused Deputy - this note is Hardy’s original paper; Confused Deputy is the concept page.
Capability Security - Hardy’s “why capabilities might have been invented” is the operational motivation of the whole tradition.
Object Capability Security - object-capabilities inherit the fix directly.
E Language - E’s reference-passing discipline is an anti-confused-deputy design.
CapTP
Ambient Authority - Hardy is the source of the critique; ambient authority IS the bug.
Principle of Least Authority - the confused deputy appears when a process has more authority than the request demands.
Distributed Security
Security Kernel Lambda Calculus
Capability Bounding

Conceptual Contribution

Capability-based Financial Instruments

Reference

Miller, Mark S.; Morningstar, Chip; Frantz, Bill. “Capability-based Financial Instruments.” In Proceedings of the 4th International Conference on Financial Cryptography (FC 2000), Anguilla, BWI, February 20-24, 2000. LNCS 1962, pp. 349-378, Springer, 2001. URL

Summary

Also called the “Ode” paper (after its original filename ode.pdf), this paper bridges three previously disjoint communities: object-oriented programming, capability-based secure operating systems, and financial cryptography. The authors argue that each community has been strong where the others were weak - objects give composition and abstraction, capability OSs give mutually-protected shared platforms for untrusted code, and financial cryptography gives mutually-suspicious multiparty protocols - and that a unified abstraction, the Granovetter diagram, captures the core of all three.

The Granovetter diagram (named after sociologist Mark Granovetter’s work on how social topology evolves by introduction) shows three objects - Alice, Bob, Carol - where Alice holds references to both Bob and Carol and sends Bob a foo message containing her reference to Carol, thereby introducing Bob to Carol. This single operator is at once an object message send, a capability-security introduction (only connectivity begets connectivity), a cryptographic capability-transport step, an SPKI certificate-style authorisation delegation, a multi-player game-theoretic move, and the basic step for transferring a financial bearer right.

The paper presents the E programming language, its cryptographic transport protocol Pluribus (the predecessor of CapTP), and a worked example: a covered call option implemented in ~20 lines of E as a smart contract between five mutually-suspicious parties, implemented automatically as a cryptographic protocol. This is arguably the first paper to describe smart contracts in recognisably modern form, and it predates the blockchain era entirely. It is foundational for Agoric and for all later Miller work on eights/erights.

Key Ideas

Granovetter operator: the unit of object-capability computation - Alice holds refs to Bob and Carol; Alice sends Carol-ref to Bob; Bob now has Carol.
Only connectivity begets connectivity: authority can change only by this three-party introduction step.
Six perspectives on the Granovetter operator: object computation, capability security, cryptographic protocol, public-key infrastructure, multi-player game rule, financial bearer instrument.
Smart contracts as object code: a covered-call option is just an object with references to the underlying asset, the strike-price payment, and its counterparties.
Rights = sendable messages: a right is exercised by sending a message to an object that embodies it; secure transfer of a right = secure transfer of a reference.
Pluribus: E’s cryptographic capability transport, turning local object semantics into distributed multiparty protocols.
Bearer instruments classified along axes: exclusive/non-exclusive, fungible/specific, exercisable, assayable.

Connections

The Heart of Spritely - Distributed Objects and Capability Security - Spritely’s goblin/ocapN inherits the same Granovetter-diagram semantics.
E Language - this paper is the first major presentation of E to the financial-crypto world.
CapTP - Pluribus here is the direct predecessor of CapTP.
Capability Security and Object Capability Security
Ambient Authority - this paper is emphatic that ambient-authority systems cannot express financial rights safely.
Confused Deputy
Principle of Least Authority
Distributed Security
Security Kernel Lambda Calculus
A Universal Modular Actor Formalism for Artificial Intelligence
Actor Model
Vat Model
Promise Pipelining

Conceptual Contribution

Using Encryption for Authentication

Using Encryption for Authentication in Large Networks of Computers

Reference: Needham, R. M. & Schroeder, M. D. (1978). Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12), pp. 993–999. (With critical follow-up: Lowe, G. (1995). An Attack on the Needham–Schroeder Public-Key Authentication Protocol. Information Processing Letters 56(3), pp. 131–133, and Lowe (1996) Breaking and Fixing the Needham–Schroeder Public-Key Protocol Using FDR, TACAS ’96.) ACM DOI · Open access PDF (UT Austin) · Lowe attack (1995) DOI

Summary

Needham and Schroeder describe two foundational authentication protocols for large untrusted networks: a symmetric-key protocol relying on a trusted authentication server (which became the basis of Kerberos), and a public-key protocol that establishes mutual authentication and a shared session-secret between two principals using only public-key encryption. The symmetric protocol uses nonces to prevent replay and a server S that knows long-term keys for every principal; messages 1–3 obtain a fresh session key K_AB from S, message 4 challenges B with a nonce, message 5 returns the nonce decremented as proof of session-key possession. The public-key protocol is shorter — three messages exchanging two nonces under the partners’ public keys, with mutual authentication established by demonstrating the ability to decrypt and return the partner’s nonce. The paper became a touchstone of the cryptographic-protocol literature, both for what it got right (the use of nonces, the trusted-third-party authentication server, the layered structure of session establishment) and — famously — for what it got wrong. In 1995 Gavin Lowe found that the public-key protocol is vulnerable to a man-in-the-middle attack: a dishonest principal I can interpose himself between A and B, convincing B that A initiated a session with him when in fact A initiated a session with I. The flaw is invisible in the original informal argument; Lowe found it by formal model-checking with FDR, and the fix (include B’s identity in the second message) is a one-line change. The Needham-Schroeder–Lowe story became the canonical case-study for why formal protocol verification matters: a protocol that “looked correct” for 17 years and was widely cited contained a fundamental flaw that was systematically discovered the moment a formal tool was applied.

Key Ideas

Trusted authentication server (Kerberos lineage): in the symmetric-key protocol, an online server S shares a long-term key with every principal and brokers session-key establishment between any pair. This pattern became the architectural foundation of Kerberos and (with adjustments) of every realistic enterprise SSO system.
Nonces for freshness: each principal includes a nonce in their request so that replay of an old session-key message can be detected. The use of nonces is correct; their interpretation in BAN-style analysis is more subtle than the original informal argument suggested.
Public-key symmetric-style authentication: the public-key protocol shows authentication can be done without an online server given only certificates of long-term public keys — three messages, two nonces, mutual authentication.
The Lowe attack: in the original public-key protocol, message 2 from B to A returns {N_A, N_B}_pubA (A’s nonce together with B’s nonce, encrypted with A’s public key). If A is talking to a dishonest I, then I can re-encrypt and forward to B, who responds to I thinking he is responding to A — and I can pose as A to B for the duration of the session. The attack is a strict man-in-the-middle: A and B reach inconsistent beliefs about who they are talking to.
The Lowe fix: include B’s identity in message 2 — {N_A, N_B, B}_pubA — so that A can verify the message was intended for him from B specifically and the substitution attack is detected.
Methodological lesson: informal correctness arguments — even by careful authors over careful protocols — are unreliable for cryptographic protocols. Formal verification (BAN Logic, Spi Calculus, ProVerif, FDR) is necessary, not optional.

Connections

Conceptual Contribution

Claim: Cryptographic authentication in large networks can be built from a small set of primitives — long-term keys, nonces for freshness, a trusted third party (or public-key infrastructure) — combined into protocols of three to five messages. (And the now-canonical second claim, supplied by Lowe 1995/1996: even careful informal arguments for such protocols cannot be trusted; formal verification is required.)
Mechanism: Two protocol designs — symmetric-key with online server, public-key with PKI — using nonces for freshness and explicit role identifiers. Lowe’s contribution: model-checking the public-key protocol with FDR, finding the man-in-the-middle attack, and supplying the one-message fix.
Concepts introduced/used: Needham-Schroeder Protocol, Nonce, Replay Attack, Trusted Third Party, Public-Key Authentication, Lowe Attack, Man-in-the-Middle Attack.
Stance: foundational protocol design + canonical worked example for protocol verification.
Relates to: Direct ancestor of Kerberos and of every enterprise authentication-and-key-distribution system. Provides the worked example that motivates BAN Logic (Burrows, Abadi & Needham 1990 — Needham himself); the original protocol’s analysis under BAN already revealed weaknesses missed in the 1978 informal argument. Lowe’s 1995/96 attack and FDR analysis launched the formal-methods-for-protocols programme that produced the Spi Calculus (Abadi & Gordon 1997) and the symbolic provers ProVerif / Tamarin. The Lowe attack is structurally a parser-differential attack at the protocol level — A and B parse the protocol-state differently, with I exploiting the difference — directly analogous to the PKI Layer Cake - Kaminsky Patterson Sassaman attack on certificate parsing in PKIs. Within the agent-communication literature, NS is the canonical example proving that informal speech-act-based protocol correctness arguments — including most ACL conformance arguments — are insufficient: a KQML or FIPA-ACL interaction protocol with the same structural flaw would have the same vulnerability, and ACL conformance methodologies need the same kind of formal underpinning.

Tags

#crypto-protocols #authentication #needham #schroeder #lowe #replay-attack #security #foundations

Authentication Protocol

A cryptographic protocol whose goal is to allow one principal to verify the identity of another (and typically to establish a shared session key for subsequent secure communication). Canonical examples: Needham-Schroeder Protocol (1978), Kerberos (1980s), TLS handshake, Signal X3DH/PQXDH, FIDO2/WebAuthn. Verification is the subject of BAN Logic, the Spi Calculus, and modern symbolic provers (ProVerif, Tamarin) under the Dolev-Yao threat model.