A Formal Account of the Open Provenance Model