Formal Policy-based Provenance Audit


Formal Policy-based Provenance Audit


Denis Butin, Denise Demirel, and Johannes Buchmann (TU Darmstadt)


Data processing within large organisations is often complex, impeding both the traceability of data and the compliance of processing with usage policies. The chronology of the ownership, custody, or location of data — its provenance — provides the necessary information to restore traceability. However, to be of practical use, provenance records should include sufficient expressiveness by design with a posteriori analysis in mind, e.g. the verification of their compliance with usage policies. Additionally, they ought to be combined with systematic reasoning about their correctness. In this paper, we introduce a formal framework for policy-based provenance audit. We show how it can be used to demonstrate correctness, consistency, and compliance of provenance records with machine-readable usage policies. We also analyse the suitability of our framework for the special case of privacy protection. A formalised perspective on provenance is also useful in this area, but it must be integrated into a larger accountability process involving data protection authorities to be effective. The practical applicability of our approach is demonstrated using a provenance record involving medical data and corresponding privacy policies with personal data protection as a goal.


11th International Workshop on Security, IWSEC 2016, (

Place and Date

Tokyo, Japan, September 12-14, 2016

Publication Reference

Denis Butin, Denise Demirel, and Johannes Buchmann (TU Darmstadt). Formal Policy-based Provenance Audit. 11th International Workshop on Security, IWSEC 2016, Tokyo, Japan, September 12-14, 2016, Proceedings.


@inproceedings{	TUD-CS-2016430,
	author = {Denis Butin and Denise Demirel and Johannes Buchmann},
	title = {Formal Policy-based Provenance Audit},
	month = sep,
	year = {2016},
	booktitle = {The 11th International Workshop on Security - IWSEC 2016},
	location = {sola city Conference Center, Akihabara-Ochanomizu District, Tokyo, Japan},
	pubkey = {TUD-CS-2016-1430},
	research_area = {CROSSING, Theoretische Informatik - Kryptographie und Computeralgebra},
	research_sub_area = {PRISMACLOUD, Solutions, S6},
	Website = { (Link:\"\" )},