Advertisement

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)

Abstract

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.

Keywords

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

References

  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).  https://doi.org/10.1145/1063979.1063998
  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).  https://doi.org/10.1007/s00778-006-0023-0CrossRefGoogle Scholar
  3. 3.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. Inf. Comput. 196(2), 127–155 (2005).  https://doi.org/10.1016/j.ic.2004.08.003MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Clavel, M., et al.: Maude Manual (Version 2.7). Technical report, SRI International Computer Science Laboratory (2015). http://maude.cs.uiuc.edu/maude2-manual
  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). https://www.springer.com/la/book/9783540719403
  6. 6.
    Jakšić, S., Pantović, J., Ghilezan, S.: Linked data privacy. Math. Struct. Comput. Sci. 27(1), 33–53 (2017).  https://doi.org/10.1017/S096012951500002XMathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-33612-1_8CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-19195-9_12CrossRefGoogle Scholar
  9. 9.
    Kouzapas, D., Philippou, A.: Privacy by typing in the \(\pi \)-calculus. Logical Methods Comput. Sci. 13(4) (2017).  https://doi.org/10.23638/LMCS-13(4:27)2017
  10. 10.
    Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7), 721–781 (2012).  https://doi.org/10.1016/j.jlap.2012.06.003MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1145/1805974.1805980CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-74835-9_6CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-10431-7_30CrossRefGoogle 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).  https://doi.org/10.1016/B978-044482830-9/50026-6CrossRefGoogle Scholar
  15. 15.
    Pitsiladis, G.V.: Type checking conditional purpose-based privacy policies in the \(\pi \)-calculus. Limassol, Cyprus (2016). http://users.ntua.gr/gpitsiladis/files/documents/2016-11-fmpriv-conditions.pdf
  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). http://dspace.lib.ntua.gr/handle/123456789/44439
  17. 17.
    Solove, D.J.: A Taxonomy of Privacy. SSRN Scholarly Paper ID 667622, Social Science Research Network, Rochester, NY, February 2005. https://papers.ssrn.com/abstract=667622
  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).  https://doi.org/10.1016/S1571-0661(05)80125-2MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1016/S1571-0661(05)82539-3CrossRefGoogle 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