Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Backes, M., Hritcu, C., Maffei, M.: Type-checking zero-knowledge. In: Proceedings of CCS 2008, pp. 357–370 (2008)
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)
Braghin, C., Gorla, D., Sassone, V.: Role-based access control for a distributed calculus. Journal of Computer Security 14(2), 113–155 (2006)
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)
Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. Information and Computation 196(2), 127–155 (2005)
Compagnoni, A.B., Gunter, E.L., Bidinger, P.: Role-based access control for boxed ambients. Theoretical Computer Science 398(1-3), 203–216 (2008)
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)
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)
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)
Fournet, C., Gordon, A., Maffeis, S.: A type discipline for authorization in distributed systems. In: Proceedings of CSF 2007, pp. 31–48 (2007)
Hennessy, M., Rathke, J., Yoshida, N.: safedpi: A language for controlling mobile code. Acta Informatica 42(4-5), 227–290 (2005)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173(1), 82–120 (2002)
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)
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)
Liu, Y., Müller, S., Xu, K.: A static compliance-checking framework for business process models. IBM Systems Journal 46(2), 335–362 (2007)
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)
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)
Solove, D.J.: A Taxonomy of Privacy. University of Pennsylvania Law Review 154(3), 477–560 (2006)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kouzapas, D., Philippou, A. (2015). Type Checking Privacy Policies in the π-calculus. In: Graf, S., Viswanathan, M. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2015. Lecture Notes in Computer Science(), vol 9039. Springer, Cham. https://doi.org/10.1007/978-3-319-19195-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-19195-9_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19194-2
Online ISBN: 978-3-319-19195-9
eBook Packages: Computer ScienceComputer Science (R0)