Secure Communications Processing for Distributed Languages
Reference: Abadi, Fournet, Gonthier (1999). Compaq SRC / Microsoft Research / INRIA technical paper. Source file: Secure_communications_processing_for_dis.pdf. URL
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.
Connections
Conceptual Contribution
Tags