Towards a Calculus of Secure Mobile Computations

The SEAL calculus is a calculus of mobile computations designed for programming secure distributed applications over large scale open networks. The calculus is a distributed variant of the π-calculus that incorporates agent mobility as well as strong protection mechanisms. Linear, revocable, capabilities control access to resources and ensure that agents may only use resources that have been allocated to them. Capabilities are also used to protect agents from the hosts on which they execute. The syntax and semantics of the SEAL calculus are presented and its expressive power is demonstrated with an example secure mobile