Mobile Ambients -Annex-

We develop some theory of the ambient calculus, based on a labeled transition system, strong bisimilarity and contextual equivalence. The goal of this Annex to the main paper is to recast notions of observational equivalence from the ß-calculus in the setting of the ambient calculus, so as to reason about mobile computation. In Section 1 we review the technical definitions of the ambient calculus from the main part of the paper. In Section 2 we define the commitment relation, a labeled transition system for the calculus, and strong bisimilarity. In Section 3 we define contextual equivalence and prove an instance, the Perfect Firewall Equation. Section 4 concludes. 1 Review of the Ambient Calculus In this section we review the syntax of the ambient calculus, and the structural congruence and reduction relations. 1.1 Capabilities and Processes We assume an infinite set of names. We let m and n range over names. Moreover, we assume there is an infinite collections of variables ranged o..