Data provenance is the history of derivation of a data ar- tifact from its original sources. As the real-life provenance records can likely cover thousands of data items and derivation steps, one of the pressing challenges becomes development of formal frameworks for their automated verification. In this paper, we consider data expressed in standard Semantic Web on- tology languages, such as OWL, and define a novel verification formalism called provenance specification logic, building on dynamic logic. We val- idate our proposal by modeling the test queries presented in The First Provenance Challenge, and conclude that the logic core of such queries can be successfully captured in our formalism.