Massimo Merro
 

We study a variant of Levi and Sangiorgi's Safe Ambients (SA) enriched
with passwords (SAP). In SAP by managing passwords, for example
generating new ones and distributing them selectively, an ambient may
now program who may migrate into its computation space, and when.
Moreover in SAP an ambient may provide different services depending on
the passwords exhibited by its incoming clients.

We give an lts based operational semantics for SAP and a labelled
bisimulation based equivalence which is proved to coincide with barbed
congruence.

We use our notion of bisimulation to prove a set of algebraic laws
which are subsequently exploited to prove more significant examples.