Security Types for Mobile Safe Ambients

The {\em Ambient Calculus} and the {\em Safe Ambient Calculus} have been recently successfully proposed as models for the Web. They are based on the notions of ambient {\em movement} and ambient {\em opening}. Different type disciplines have been devised for them in order to avoid unwanted behaviours of processes. In the present paper we propose a type discipline for safe mobile ambients which is essentially motivated by ensuring {\em security} properties. We associate security levels to ambients and we require that an ambient at security level $s$ can only be traversed or opened by ambients at security level at least $s$. Since the movement and opening right can be unrelated, we consider two partial orders between security levels. We give some examples of use of our type discipline. A first protocol models a mailserver with different mailboxes and users: each user is allowed to enter only his own mailbox. A second example show that we can encode a security policy for reading and writing recently proposed for the $\pi$-calculus. Lastly we present the renaming, firewall and channel protocols which are already typed in other type disciplines for comparisons and for showing how some behavioural conditions can be expressed in our system as type constraints.