A flow-sensitive analysis of privacy properties

In this paper we consider service oriented architectures where many components interact with one another using a wireless network. We are interested in questions like: ldr Can I be sure that I do not get unsolicited information from some service? - unless I give my permission? ldr Can I be sure that information I send to some service never is leaked to another service? - unless I give my permission? We shall develop a static program analysis for the pi- calculus and show how it can be used to give privacy guarantees like the ones requested above. The analysis records the explicit information flow of the system and keeps track of, not only the potential configurations of the system, but also the order in which they may be encountered.