Ambient calculus-based modal logics for mobile ambients are disclosed. Formal analysis mechanisms or frameworks with which mobile ambients can be described, and within which policies such as security policies can be tested against those ambients, are disclosed. In one embodiment, a computer-implemented method receives at least one container, where each container has at least one process. The method applies the containers, including their processes, against a predetermined modal logic. The modal logic is based on ambient calculus, and provides for spatial relationships among the processes of the containers. The containers and their processes are output, as applied against the logic.