Sjoin Calculus

A secure variant of the join calculus in which channel names are cryptographic keys and message reception requires possession of the matching key. It gives a process-calculus foundation for end-to-end-protected distributed programming.

In this vault

Summary

Abadi, Fournet, and Gonthier formalize communications processing — the marshaling, unmarshaling, and cryptographic operations that wrap distributed language primitives like RPC and RMI — within a process calculus. They study how local communication semantics (single machine or protected network) can be extended transparently to hostile distributed networks through a generic cryptographic “wrapper” that operates like a firewall with an encrypting tunnel.

The technical core uses the join-calculus and its cryptographic extension, the sjoin-calculus, to translate high-level join-calculus processes into protected low-level sjoin-calculus processes that exchange encrypted messages. They prove a full-abstraction theorem showing the wrapping preserves observational equivalence — attackers on the public network cannot distinguish wrapped processes that behave the same locally.

Key Ideas

Join-calculus as basis for concurrent/distributed language semantics.

Sjoin-calculus adds symmetric encryption primitives.

Wrapper as filter/firewall doing marshaling + encryption uniformly.

Full-abstraction theorem: wrapping preserves equivalences.

Security reasoned compositionally across distribution boundaries.

Conceptual Contribution

Claim: The communications-processing layer of a distributed language (marshalling + crypto) can be compiled automatically from a local-semantics specification in such a way that distribution becomes observationally transparent even under an active network attacker.

Mechanism: Abadi, Fournet and Gonthier use the join-calculus for local semantics and the sjoin-calculus (join + symmetric crypto primitives) for the low-level network, defining a wrapper translation that implements channel communication via encrypted tunnels gated by a firewall-like filter. A full-abstraction theorem proves that two source programs are observationally equivalent iff their wrapped versions are, so security reasoning composes with functional reasoning.

Concepts introduced/used: Join Calculus, Sjoin Calculus, Full Abstraction, Communications Processing, Cryptographic Wrapper, Observational Equivalence, Marshalling

Stance: formal-semantic

Relates to: Provides the calculus-level counterpart to language-engineering security efforts like The Halting Problems of Network Stack Insecurity and A Language-Based Approach To Prevent DDoS; its transparent-distribution agenda links to the actor-style transparency claims of Programming Erlang Second Edition and the SOL/SINS encrypted inter-agent channels in Architectural Patterns for Dependable Software Systems - SOL.

Sjoin Calculus

In this vault

Backlinks