Abstract
We introduce a Control Flow Analysis that statically approximates the dynamic behaviour of mobile processes, expressed in (a variant of) the π-calculus. Our analysis of a system is able to describe the essential behaviour of each sub-system, tracking where and between which sub-processes communications may occur. This means that we can safely approximate the behaviour of a system plugged in a larger and mainly unknown context, without explicitly analysing it. Several possible properties can be investigated using this approximation, among which some related to confidentiality and to access control policies.
