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