25/01/2001: Ivano Salvo (Univ. de Turin)
Security Types for Safe Mobile Ambients.

Résumé
The _Ambient Calculus_ and the _Safe Ambient Calculus_ have been recently successfully proposed as models for the Web. They are based on the notions of ambient _movement_ and ambient _opening_. Different type disciplines have been devised for them in order to avoid unwanted behaviours of processes.
In this talk we describe a type discipline for safe mobile ambients which is essentially motivated by ensuring _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 shows 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.