Implementation of Privacy Calculus and Its Type Checking in Maude

  • Georgios V. PitsiladisEmail author
  • Petros Stefaneas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


Philippou and Kouzapas have proposed a privacy-related framework, consisting of (i) a variant of the \(\pi \)-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.


Maude Privacy Privacy policies \(\pi \)-calculus Type systems 


  1. 1.
    Byun, J.W., Bertino, E., Li, N.: Purpose based access control of complex data for privacy protection. In: Proceedings of the Tenth ACM Symposium on Access Control Models and Technologies, SACMAT 2005, pp. 102–110. ACM, New York (2005).
  2. 2.
    Byun, J.W., Li, N.: Purpose based access control for privacy protection in relational database systems. VLDB J. 17(4), 603–619 (2008). Scholar
  3. 3.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. Inf. Comput. 196(2), 127–155 (2005). Scholar
  4. 4.
    Clavel, M., et al.: Maude Manual (Version 2.7). Technical report, SRI International Computer Science Laboratory (2015).
  5. 5.
    Clavel, M., et al.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. Programming and Software Engineering. Springer, Heidelberg (2007).
  6. 6.
    Jakšić, S., Pantović, J., Ghilezan, S.: Linked data privacy. Math. Struct. Comput. Sci. 27(1), 33–53 (2017). Scholar
  7. 7.
    Kokkinofta, E., Philippou, A.: Type checking purpose-based privacy policies in the \(\pi \)-Calculus. In: Hildebrandt, T., Ravara, A., van der Werf, J.M., Weidlich, M. (eds.) WS-FM 2014-2015. LNCS, vol. 9421, pp. 122–142. Springer, Cham (2016). Scholar
  8. 8.
    Kouzapas, D., Philippou, A.: Type checking privacy policies in the \(\pi \)-calculus. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 181–195. Springer, Cham (2015). Scholar
  9. 9.
    Kouzapas, D., Philippou, A.: Privacy by typing in the \(\pi \)-calculus. Logical Methods Comput. Sci. 13(4) (2017).
  10. 10.
    Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7), 721–781 (2012). Scholar
  11. 11.
    Ni, Q., et al.: Privacy-aware Role-based access control. ACM Trans. Inf. Syst. Secur. 13(3), 24:1–24:31 (2010). Scholar
  12. 12.
    Ni, Q., Lin, D., Bertino, E., Lobo, J.: Conditional privacy-aware role based access control. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 72–89. Springer, Heidelberg (2007). Scholar
  13. 13.
    Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 378–392. Springer, Cham (2014). Scholar
  14. 14.
    Parrow, J.: An introduction to the \(\pi \)-calculus. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 479–543. Elsevier Science, Amsterdam (2001). Scholar
  15. 15.
    Pitsiladis, G.V.: Type checking conditional purpose-based privacy policies in the \(\pi \)-calculus. Limassol, Cyprus (2016).
  16. 16.
    Pitsiladis, G.V.: Type Checking Privacy Policies in the \(\pi \)-calculus and its Executable Implementation in Maude (in Greek). Diploma thesis, National Technical University of Athens, Greece (2016).
  17. 17.
    Solove, D.J.: A Taxonomy of Privacy. SSRN Scholarly Paper ID 667622, Social Science Research Network, Rochester, NY, February 2005.
  18. 18.
    Stehr, M.O.: CINNI - A generic calculus of explicit substitutions and its application to \(\lambda \)- \(\varsigma \)- and \(\pi \)-calculi. Electron. Notes Theor. Comput. Sci. 36, 70–92 (2000). Scholar
  19. 19.
    Thati, P., Sen, K., Martí-Oliet, N.: An executable specification of asynchronous \(\pi \)-calculus semantics and may testing in Maude 2.0. Electron. Notes Theor. Comput. Sci. 71, 261–281 (2004). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.National and Kapodistrian University of AthensIlissiaGreece
  2. 2.National Technical University of AthensZografouGreece

Personalised recommendations