In this paper we propose a formal framework for studying privacy. Our framework is based on the π-calculus with groups accompanied by a type system for capturing privacy requirements relating to information collection, information processing and information dissemination. The framework incorporates a privacy policy language. We show that a system respects a privacy policy if the typing of the system is compatible with the policy. We illustrate our methodology via analysis of privacy-aware schemes proposed for electronic traffic pricing.


Access Control Privacy Policy Smart Card Policy Language Private Data 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Backes, M., Hritcu, C., Maffei, M.: Type-checking zero-knowledge. In: Proceedings of CCS 2008, pp. 357–370 (2008)Google Scholar
  2. 2.
    Barth, A., Datta, A., Mitchell, J.C., Nissenbaum, H.: Privacy and contextual integrity: Framework and applications. In: Proceedings of S&P 2006, pp. 184–198 (2006)Google Scholar
  3. 3.
    Braghin, C., Gorla, D., Sassone, V.: Role-based access control for a distributed calculus. Journal of Computer Security 14(2), 113–155 (2006)Google Scholar
  4. 4.
    Bugliesi, M., Colazzo, D., Crafa, S., Macedonio, D.: A type system for discretionary access control. Mathematical Structures in Computer Science 19(4), 839–875 (2009)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. Information and Computation 196(2), 127–155 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Compagnoni, A.B., Gunter, E.L., Bidinger, P.: Role-based access control for boxed ambients. Theoretical Computer Science 398(1-3), 203–216 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Datta, A., Blocki, J., Christin, N., DeYoung, H., Garg, D., Jia, L., Kaynar, D., Sinha, A.: Understanding and protecting privacy: Formal semantics and principled audit mechanisms. In: Jajodia, S., Mazumdar, C. (eds.) ICISS 2011. LNCS, vol. 7093, pp. 1–27. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  8. 8.
    de Jonge, W., Jacobs, B.: Privacy-friendly electronic traffic pricing via commits. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 143–161. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Dezani-Ciancaglini, M., Ghilezan, S., Jakšić, S., Pantović, J.: Types for role-based access control of dynamic web data. In: Mariño, J. (ed.) WFLP 2010. LNCS, vol. 6559, pp. 1–29. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  10. 10.
    Fournet, C., Gordon, A., Maffeis, S.: A type discipline for authorization in distributed systems. In: Proceedings of CSF 2007, pp. 31–48 (2007)Google Scholar
  11. 11.
    Hennessy, M., Rathke, J., Yoshida, N.: safedpi: A language for controlling mobile code. Acta Informatica 42(4-5), 227–290 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173(1), 82–120 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Koleini, M., Ritter, E., Ryan, M.: Model checking agent knowledge in dynamic access control policies. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 448–462. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Kouzapas, D., Philippou, A.: A typing system for privacy. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 56–68. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  15. 15.
    Liu, Y., Müller, S., Xu, K.: A static compliance-checking framework for business process models. IBM Systems Journal 46(2), 335–362 (2007)CrossRefGoogle Scholar
  16. 16.
    May, M.J., Gunter, C.A., Lee, I.: Privacy APIs: Access control techniques to analyze and verify legal privacy policies. In: Proceedings of CSFW 2006, pp. 85–97 (2006)Google Scholar
  17. 17.
    Ni, Q., Bertino, E., Lobo, J., Brodie, C., Karat, C., Karat, J., Trombetta, A.: Privacy-aware role-based access control. ACM Trans. on Information and System Security 13(3) (2010)Google Scholar
  18. 18.
    Solove, D.J.: A Taxonomy of Privacy. University of Pennsylvania Law Review 154(3), 477–560 (2006)CrossRefGoogle Scholar
  19. 19.
    Tschantz, M.C., Wing, J.M.: Formal methods for privacy. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 1–15. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  • Dimitrios Kouzapas
    • 1
    • 2
  • Anna Philippou
    • 3
  1. 1.Department of ComputingImperial College LondonLondonUK
  2. 2.Department of Computing ScienceUniversity of GlasgowGlasgowUK
  3. 3.Department of Computer ScienceUniversity of CyprusNicosiaCyprus

Personalised recommendations