Affiliations: [a] Dipartimento di Informatica, Università di Pisa, Via F. Buonarroti 2, I-56127 Pisa, Italy. E-mail: [email protected], [email protected] | [b] Dipartimento di Informatica e Telecomunicazioni, Università di Trento, Via Sommarive, 1438050 Povo (TN), Italy. E-mail: [email protected]
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.
Keywords: Control Flow Analysis, security, access control policies, enhanced semantics
