Commit 51b2a8ea authored by gartur's avatar gartur
Browse files

1.0.1

parent 7183f5fa
......@@ -4,6 +4,10 @@
"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": {
"gdpr": {
"formula": "src/gdpr.mfotl",
"signature": "src/sig.sig"
},
"info_on_consent": {
"formula": "src/info_on_consent.mfotl",
"signature": "src/sig.sig"
......
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
LET lawful_processing(data,dataid,dsid) = f"lawful_processing.mfotl"s"sig.sig" IN
LET consent(data,dataid,dsid) = f"lawful_processing.mfotl"s"sig.sig" IN
LET info_on_consent(data,dataid,dsid) = f"info_on_consent.mfotl"s"sig.sig" IN
LET right_to_access(dsid) = f"right_to_access.mfotl"s"sig.sig" IN
LET right_to_erasure(data,dataid,dsid,procid) = f"right_to_erasure.mfotl"s"sig.sig" IN
LET right_to_restriction_of_processing(data,dataid,dsid) = f"right_to_restriction_of_processing.mfotl"s"sig.sig" IN
LET right_to_object(data,dataid,dsid) = f"right_to_object.mfotl"s"sig.sig" 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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment