Refinement checking for privacy policies. (English) Zbl 1243.68041

Summary: This paper presents a framework for analysis and comparison of privacy policies expressed in P3P (platform for privacy preferences). In contrast to existing approaches to policy analysis, which focus on demonstrations of equality or equivalence of policies, our approach makes it possible to check for refinement between policies. We automatically generate a CSP model from a P3P policy, which represents the policy’s intended semantics; using the FDR model checker, we then perform various tests (using process refinement) to determine (a) whether a policy is internally consistent, and (b) whether a given policy refines another by permitting similar data collection, processing and sharing practices. Our approach allows for the detection of subtle differences between practices prescribed by different privacy policies, the comparison of relative levels of privacy offered by different policies, and captures the semantics of policies intended in the original P3P standard. The systematic translation of policies to CSP provides a formal means of reasoning about websites’ privacy policies, and therefore the practices of various enterprises with regards to personal data.


68M11 Internet topics
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)


Full Text: DOI


[1] The PRIME project. URL: https://www.prime-project.eu/.
[2] The PrimeLife project. URL: http://www.primelife.eu.
[3] The EnCoRe project. URL: http://www.encore-project.info.
[4] L. Cranor, B. Dobbs, S. Egelman, G. Hogben, J. Humphrey, M. Langheinrich, M. Marchiori, M. Presler-Marshall, J.M. Reagle, M. Schunter, D.A. Stampley, R. Wenning, The Platform for Privacy Preferences 1.1 (P3P1.1) specification, World Wide Web Consortium, Note NOTE-P3P11-20061113 (November 2006).
[5] G. Hogben, A technical analysis of problems with P3P v1.0 and possible solutions, in: Proceedings of W3C Workshop on the Future of P3P, 2002. URL: http://www.w3.org/2002/p3p-ws/pp/jrc.html.
[6] T. Moses, eXtensible Access Control Markup Language TC v2.0 (XACML) (February 2005). URL: http://docs.oasis-open.org/xacml/2.0/access_control-xacml-2.0-core-spec-os.pdf.
[7] T. Moses, Privacy policy profile of XACML (16 September 2004). URL: http://docs.oasis-open.org/xacml/access_control-xacml-2_0-privacy_profile-spec-cd-01.pdf.
[8] Moffett, J. D.; Sloman, M. S.: Policy hierarchies for distributed systems management, IEEE J. Sel. areas commun. 11, 1404-1414 (1993)
[9] Roscoe, A. W.: Understanding concurrent systems, (2010) · Zbl 1211.68205
[10] Formal Systems (Europe) Ltd., FDR2 User’s Manual version 2.82 (June 2005). URL: http://www.fsel.com/documentation/fdr2/fdr2manual.pdf.
[11] IBM P3P Policy Editor. URL: http://www.alphaworks.ibm.com/tech/p3peditor.
[12] Privacy Finder. URL: http://www.privacyfinder.org/.
[13] M.J. May, C.A. Gunter, I. Lee, Strong and weak policy relations, in: Proceedings of IEEE International Symposium on Policies for Distributed Systems and Networks, POLICY’09, London, UK, 2009.
[14] T. Yu, N. Li, A.I. Antón, A formal semantics for P3P, in: Proceedings of ACM Workshop on Secure Web Services, Fairfax VA, USA, 2004.
[15] Stamey, J. W.; Rossi, R. A.: Automatically identifying relations in privacy policies, , 233-238 (2009)
[16] Bryans, J.: Reasoning about XACML policies using CSP, , 28-35 (2005)
[17] Ryan, P.; Arnesen, R. R.: A process–algebraic approach to security policies, Dbsec: IFIP conference Proceedings, vol. 256 256, 301-312 (2002) · Zbl 1090.68522
[18] Fisler, K.; Krishnamurthi, S.; Meyerovich, L. A.; Tschantz, M. C.: Verification and change-impact analysis of access-control policies, , 196-205 (2005)
[19] Zhang, N.; Ryan, M.; Guelev, D. P.: Synthesising verified access control systems in xacml, , 56-65 (2004)
[20] Gunter, C. A.; May, M. J.; Stubblebine, S. G.: A formal privacy system and its application to location based services, Lecture notes in computer science 3424 (2005)
[21] M.J. May, C.A. Gunter, I. Lee, Privacy APIs: Access control techniques to analyze and verify legal privacy policies, in: Computer Security Foundations Workshop, CSFW, July 2006, Venice, Italy, 2006.
[22] Fournet, C.; Gordon, A. D.; Maffeis, S.: A type discipline for authorization policies, ACM transactions on programming languages and systems 29, No. 5, 25 (2007) · Zbl 1108.68456
[23] D. Walker, A type system for expressive security policies, Tech. rep., Ithaca, NY, USA, 1999. · Zbl 1323.68233
[24] M.Y. Becker, A. Malkis, L. Bussard, S4P: A generic language for specifying privacy preferences and policies, Technical Report MSR-TR-2010-32, Microsoft Research, April 2010.
[25] Ouaknine, J.; Schneider, S.: Timed CSP: A retrospective, Entcs 162 (2006)
[26] I. Agrafiotis, S. Creese, M. Goldsmith, N. Papanikolaou, The logic of consent and revocation (2010) (submitted for publication).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.