We study a behavioural theory of Cardelli and Gordon's Mobile Ambients, a process calculus for modelling mobile agents in wide-area networks, focussing on reduction barbed congruence. Our contribution is threefold. We prove a context lemma that shows that only parallel and nesting contexts need be examined to recover this congruence. We characterise this congruence using a labelled bisimilarity: this requires novel techniques to deal with asynchronous movements of agents and with the invisibility of migrations of secret locations. We develop refined proof methods involving up-to proof techniques, which allow us to verify a set of algebraic laws and the correctness of more complex examples.
