Behavioral theory for mobile ambients

We study a behavioral theory of Mobile Ambients, a process calculus for modelling mobile agents in wide-area networks, focussing on reduction barbed congruence. Our contribution is threefold. (1) We prove a context lemma which shows that only parallel and nesting contexts need be examined to recover this congruence. (2) We characterize this congruence using a labeled bisimilarity: this requires novel techniques to deal with asynchronous movements of agents and with the invisibility of migrations of secret locations. (3) 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.