We study the behavioural theory of Cardelli and Gordon's Mobile Ambients. We give an lts based operational semantics and a labelled bisimulation based equivalence that coincides with reduction barbed congruence. We also provide two up-to proof techniques that we use to prove a set of algebraic laws, including the perfect firewall equation.

This is joint work with Massimo Merro.