Cryptographic Wrapper

A thin layer that transparently encrypts, authenticates and integrity-protects messages passing between distributed language runtimes, preserving the source-level semantics of communication primitives while providing end-to-end security guarantees.

In this vault

Marshalling

The serialisation of in-memory language values into a form suitable for transmission or storage, together with the inverse unmarshalling at the receiver. Secure distributed languages wrap marshalling with authentication and confidentiality so that the abstract semantics of message passing is preserved.

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.

Cryptographic Wrapper

In this vault

Backlinks