Tags:Maude, Privacy, Privacy policies, Type systems and π-calculus
Abstract:
Philippou and Kouzapas have proposed a privacy-related framework, consisting of (i) a variant of the π-calculus, called Privacy Calculus, that describes the interactions of processes, (ii) a privacy policy language, (iii) a type system that serves to check whether Privacy Calculus processes respect privacy policies. We present an executable implementation of (a version of) it in the programming/specification language Maude: we give an overview of the framework, outline the key aspects of its implementation, and offer a simple example of how the implementation can be used.
Implementation of Privacy Calculus and Its Type Checking in Maude