A Data Sharing Agreement (DSA) is an agreement among contracting parties regulating how they share data. DSA are usually sub- ject to a lifecycle consisting (at least) of the following phases: de?nition, enforcement, and disposal. In particular, during the de?nition phase, the parties negotiate the respective authorizations on data covered by the agreement. This phase may be iterative: authoring of the DSA is fol- lowed by analysis of its content in order to identify possible con icts or incompatibilities among authorizations clauses, before enforce them. In this paper, we concentrate on DSA formal veri?cation by proposing a for- mal framework for the automated analysis of DSA. The proposed mech- anism is built on a process algebra formalism dealing with contextual data, encoded into the executable speci?cation language Maude, based on Rewriting Logic.

Maurizio Colombo

Fabio Martinelli

Ilaria Matteucci

Marinella Petrocchi