Specifying Secure Mobile Applications

Abstract. Ambient calculi are a promising formalism for specifying mo-bile computation, which benefit from a range of analysis techniques. How-ever, Ambient calculi have been designed mostly as minimal models for mobility, rather than as specification languages for mobile applications. This paper describes a variant of Ambients, the Channel Ambient calcu-lus, which is designed to be at a level of abstraction suitable for specifying secure mobile applications on distributed TCP/IP networks. A graphical representation for the calculus is also presented, allowing specifications to be written in either textual or graphical format, together with a number of mechanisms that can be used to enhance the security of mobile appli-cations. The calculus has the advantage that it can be directly mapped to program code, which is executed by a runtime system based on a provably correct abstract machine.