Banana is a tool for the analysis of information leakage in mobile agent specifications. The language considered is Mobile Ambient
calculus, initially proposed by Cardelli and Gordon with the main purpose of explicitly modeling mobility [5]. Sites and agents (i.e., processes) are modeled as nested boxes (i.e., ambients), provided with capabilities for entering,
exiting and dissolving other boxes. This specification language provides a very simple framework to reason about information
flow and security when mobility is an issue [1].
Partially supported by MIUR Project “Modelli formali per la sicurezza”, the EU Contract IST-2001-32617 “Models and Types for
Security in Mobile Distributed Systems”, and project “Matematica per le scienze e la tecnologia”, Universitá di Trieste.