1.0.0

manifest.json

+{
+  "name": "monpoly-gdpr",
+  "author": "gartur",
+  "repository": "git@gitlab.ethz.ch:gartur/monpoly-gdpr.git",
+  "description": "formulas to monitor GDPR\nThis packet implements formulas to monitor GDPR\nbased on the paper Monitoring the GDPR\n",
+  "entities": {
+    "info_on_consent": {
+      "formula": "src/info_on_consent.mfotl",
+      "signature": "src/sig.sig"
+    },
+    "lawful_processing": {
+      "formula": "src/lawful_processing.mfotl",
+      "signature": "src/sig.sig"
+    },
+    "consent": {
+      "formula": "src/consent.mfotl",
+      "signature": "src/sig.sig"
+    },
+    "right_to_erasure": {
+      "formula": "src/right_to_erasure.mfotl",
+      "signature": "src/sig.sig"
+    },
+    "right_to_restriction_of_processing": {
+      "formula": "src/right_to_restriction_of_processing.mfotl",
+      "signature": "src/sig.sig"
+    },
+    "right_to_object": {
+      "formula": "src/right_to_object.mfotl",
+      "signature": "src/sig.sig"
+    }
+  },
+  "dependencies": {}
+}
\ No newline at end of file

src/consent.mfotl

+LET consent(data,dataid,dsid) = use(data,dataid,dsid) AND (NOT ONCE legal_grounds(dsid,data)) AND (NOT((NOT ds_revoke(dsid,data)) SINCE ds_consent(dsid,data))) IN
+consent(data,dataid,dsid)
\ No newline at end of file

src/gdpr.mfotl

+LET lawful_processing(data,dataid,dsid) = use(data,dataid,dsid) AND (NOT ONCE(ds_consent(dsid,data) OR legal_grounds(dsid,data))) IN
+LET consent(data,dataid,dsid) = use(data,dataid,dsid) AND (NOT ONCE legal_grounds(dsid,data)) AND (NOT((NOT ds_revoke(dsid,data)) SINCE ds_consent(dsid,data))) IN
+LET info_on_consent(data,dataid,dsid) = collect(data,dataid,dsid) AND (NOT NEXT(inform(dsid) OR (ONCE inform(dsid)))) IN
+LET right_to_access(dsid) = ds_access_request(dsid) AND (NOT EVENTUALLY[0,30d] grant_access(dsid)) IN
+LET right_to_erasure_1(data,dataid,dsid) = ds_deletion_request(data,dataid,dsid) AND (NOT EVENTUALLY[0,30d] delete(data,dataid,dsid)) IN
+LET right_to_erasure_2(data,dataid,dsid) = use(data,dataid,dsid) AND (ONCE delete(data,dataid,dsid)) IN
+LET right_to_erasure_3(data,dataid,dsid,procid) = ds_deletion_request (data, dataid, dsid) AND ONCE share_with( procid , dataid) AND NOT EVENTUALLY[0,30d] notify_proc(procid , dataid) IN
+LET right_to_restriction_of_processing(data,dataid,dsid) = use(data, dataid, dsid) AND (NOT ds_repeal(data, dataid, dsid) SINCE ds_restrict (data, dataid, dsid)) IN
+LET right_to_object(data,dataid,dsid) = use(data,dataid,dsid) AND (NOT ((NOT ds_object(dsid,data)) SINCE legal_grounds(dsid,data))) IN
+lawful_processing(data,dataid,dsid) OR
+consent(data,dataid,dsid) OR
+info_on_consent(data,dataid,dsid) OR
+right_to_access(dsid) OR
+right_to_erasure_1(data,dataid,dsid) OR
+right_to_erasure_2(data,dataid,dsid) OR
+right_to_restriction_of_processing(data,dataid,dsid) OR
+right_to_object(data,dataid,dsid)
\ No newline at end of file

src/info_on_consent.mfotl

+LET info_on_consent(data,dataid,dsid) = collect(data,dataid,dsid) AND (NOT NEXT(inform(dsid) OR (ONCE inform(dsid)))) IN
+info_on_consent(data,dataid,dsid) 
\ No newline at end of file

src/lawful_processing.mfotl

+LET lawful_processing(data,dataid,dsid) = use(data,dataid,dsid) AND (NOT ONCE(ds_consent(dsid,data) OR legal_grounds(dsid,data))) IN
+lawful_processing(data,dataid,dsid)
\ No newline at end of file

src/right_to_access.mfotl

+LET right_to_access(dsid) = ds_access_request(dsid) AND (NOT EVENTUALLY[0,30d] grant_access(dsid)) IN
+right_to_access(dsid)
\ No newline at end of file

src/right_to_erasure.mfotl

+LET right_to_erasure_1(data,dataid,dsid) = ds_deletion_request(data,dataid,dsid) AND (NOT EVENTUALLY[0,30d] delete(data,dataid,dsid)) IN
+LET right_to_erasure_2(data,dataid,dsid) = use(data,dataid,dsid) AND (ONCE delete(data,dataid,dsid)) IN
+LET right_to_erasure_3(data,dataid,dsid,procid) = ds_deletion_request (data, dataid, dsid) AND ONCE share_with( procid , dataid) AND NOT EVENTUALLY[0,30d] notify_proc(procid , dataid) IN
+right_to_erasure_3(data,dataid,dsid,procid)

src/right_to_object.mfotl

+LET right_to_object(data,dataid,dsid) = use(data,dataid,dsid) AND (NOT ((NOT ds_object(dsid,data)) SINCE legal_grounds(dsid,data))) IN
+right_to_object(data,dataid,dsid)
\ No newline at end of file

src/right_to_restriction_of_processing.mfotl

+LET right_to_restriction_of_processing(data,dataid,dsid) = use(data, dataid, dsid) AND (NOT ds_repeal(data, dataid, dsid) SINCE ds_restrict (data, dataid, dsid)) IN
+right_to_restriction_of_processing(data,dataid,dsid)
\ No newline at end of file

src/sig.sig

+ds_deletion_request(data:string, dataid:string, dsid:string)
+ds_access_request(dsid:string)
+ds_consent(dsid:string, data:string)
+ds_restrict(data:string, dataid:string, dsid:string)
+ds_repeal(data:string, dataid:string, dsid:string)
+ds_object(dsid:string, data:string)
+legal_grounds(dsid:string, data:string)
+ds_revoke(dsid:string, data:string)
+delete(data:string, dataid:string, dsid:string)
+grant_access(dsid:string)
+share_with(processorid:string, dataid:string)
+inform(dsid:string)
+notify_proc(processorid:string, dataid:string)
+use(data:string, dataid:string, dsid:string)
+collect(data:string, dataid:string, dsid:string)
\ No newline at end of file