We describe a modal logic for the ambient calculus, whose main novelty is the introduction of spatial connectives (in addition to standard and temporal connectives). Our logic can be used for specifying mobility protocols, for expressing mobility policies, and as a playground for model checking of mobile computation, with potential applications to bytecode verification of mobile code.
In our latest development, we have extended our logic to describe systems with hidden/secret locations. To this end, we combine a Gabbay-Pitts fresh-name quantifier with a novel "revelation" operator that can talk about restricted names. The talk will focus on these recent topics.