Ambient Calculus

Origin. Cardelli and Gordon (1998). Mobile computation in hierarchical spaces. Ambients as boundaries. Movement primitives. Foundation for mobile security.

Models. Ambients contain processes and sub-ambients. Movement: in, out, open. Hierarchy changes dynamically. Capability-based.

Formalism.

Syntax: P ::= 0 | P | Q | !P | (νn)P | n[P] | M.P

Ambient: n[P]: ambient named n containing P. Boundary with interior.

Capabilities: in n: enter ambient n. out n: exit ambient n. open n: dissolve n's boundary.

Capability prefix: M.P: perform M then continue as P. M ::= in n | out n | open n

Movement (in): n[in m.P | Q] | m[R] → m[n[P | Q] | R] n enters m.

Movement (out): m[n[out m.P | Q] | R] → n[P | Q] | m[R] n exits m.

Opening: open n.P | n[Q] → P | Q Dissolve boundary.

Structural congruence: P | 0 ≡ P n[(νm)P] ≡ (νm)n[P] (if m ≠ n) Standard rules.

Types: Ambient types: restrict capabilities. Immobile, locked ambients. Security properties.

Symbols.

Symbol	Unicode	Name	Meaning
n[P]	—	Ambient	Named boundary
in n	—	Enter	Move into n
out n	—	Exit	Move out of n
open n	—	Open	Dissolve n

Metatheory. Type systems for security. Decidability results. Encoding π-calculus. Behavioral equivalences.

Applies to. Mobile code security. Firewalls. Administrative domains. Distributed systems. Web services.

Limitations. Complex semantics. Security proofs hard. Limited implementations. Theoretical focus.