Applying Formal Methods to Describe Privacy Control Requirements in a Real Scenario: Emerging Ambiguities and Proposed Solutions

by Ioannis Agrafiotis, Sadie Creese, Michael Goldsmith, Nick Papanikolaou
Abstract:
In this paper, we demonstrate how formal methods can be used to unambiguously express privacy requirements. We focus on requirements for consent and revocation controls in a real world case study that has emerged within the EnCoRe project. We analyse the ambiguities and issues that arise when requirements expressed in natural language are transformed into a formal notation, and propose solutions to address these issues. These ambiguities were brought to our attention only through the use of a formal notation, which we have designed specifically for this purpose.
Reference:
Applying Formal Methods to Describe Privacy Control Requirements in a Real Scenario: Emerging Ambiguities and Proposed Solutions (Ioannis Agrafiotis, Sadie Creese, Michael Goldsmith, Nick Papanikolaou), In Proceedings of PrimeLife/IFIP Summer School 2010: Privacy and Identity Management for Life, Helsingborg, Sweden, 2010.
Bibtex Entry:
@INPROCEEDINGS{Agrafiotis2010,
  author = {Ioannis Agrafiotis and Sadie Creese and Michael Goldsmith and Nick
	Papanikolaou},
  title = {Applying Formal Methods to Describe Privacy Control Requirements
	in a Real Scenario: Emerging Ambiguities and Proposed Solutions},
  booktitle = {Proceedings of PrimeLife/IFIP Summer School 2010: Privacy and Identity
	Management for Life, Helsingborg, Sweden},
  year = {2010},
  month = aug,
  __markedentry = {[Nick]},
  abstract = {In this paper, we demonstrate how formal methods can be used to unambiguously
	express privacy requirements. We focus on requirements for consent
	and revocation controls in a real world case study that has emerged
	within the EnCoRe project. We analyse the ambiguities and issues
	that arise when requirements expressed in natural language are transformed
	into a formal notation, and propose solutions to address these issues.
	These ambiguities were brought to our attention only through the
	use of a formal notation, which we have designed specifically for
	this purpose.},
  owner = {nikos},
  timestamp = {2011.10.30},
  url = {../files/PrimeLife-Jo.pdf}
}