Refinement Checking for Privacy Policies

by Nikolaos Papanikolaou, Sadie Creese, Michael Goldsmith
Abstract:
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.
Reference:
Refinement Checking for Privacy Policies (Nikolaos Papanikolaou, Sadie Creese, Michael Goldsmith), In Science of Computer Programming, volume 77, 2012.
Bibtex Entry:
@ARTICLE{Papanikolaou2010c,
  author = {Nikolaos Papanikolaou and Sadie Creese and Michael Goldsmith},
  title = {Refinement Checking for Privacy Policies},
  journal = {Science of Computer Programming},
  year = {2012},
  volume = {77},
  pages = {1198},
  number = {10, 11},
  month = {September},
  abstract = {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.},
  doi = {10.1016/j.scico.2011.07.009},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {../files/polrefc.pdf}
}