, , 2004.
, Enterprise Privacy Authorization Language (EPAL). IBM Research, 2003.
A-PPL: An Accountability Policy Language, Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance -9th International Workshop, DPM 2014, 7th International Workshop, SE-TOP 2014, and 3rd International Workshop, QASA 2014, Revised Selected Papers, vol.8872, pp.319-326, 2014. ,
Principles of Model Checking, 2008. ,
Satisfiability Modulo Theories, pp.305-343, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
Privacy and Contextual Integrity: Framework and Applications, Proceedings of the 27th IEEE Symposium on Security and Privacy, S&P'06, pp.184-198, 2006. ,
S4P: A Generic Language for Specifying Privacy Preferences and Policies, 2010. ,
A Generic Information and Consent Framework for the IoT, Inria, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01953052
Experiences in the Logical Specification of the HIPAA and GLBA Privacy Laws, Proceedings of the 2010 ACM Workshop on Privacy in the Electronic Society, WPES'10, pp.73-82, 2010. ,
Automatic License Plate Recognition (ALPR): A State-of-the-Art Review, IEEE Trans. Circuits Syst. Video Techn, vol.23, issue.2, pp.311-325, 2013. ,
Automated License Plate Readers (ALPR, 2017. ,
Privacy Expectations and Preferences in an IoT World, Proceedings of the 13th Symposium on Usable Privacy and Security, SOUPS'17, pp.399-412, 2017. ,
LPL, Towards a GDPR-Compliant Privacy Language: Formal Definition and Usage, Trans. Large-Scale Data-and Knowledge-Centered Systems, vol.37, pp.41-80, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01866050
A Policy Language for Distributed Usage Control, Proceedings of the 12th European Symposium On Research in Computer Security, ESORICS'07, vol.4734, pp.531-546, 2007. ,
The SPIN Model Checker -Primer and Reference Manual, 2004. ,
Privacy Risk Analysis, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01420968
Privacy Risk Analysis to Enable Informed Privacy Settings, 2018 IEEE European Symposium on Security and Privacy, Workshops, EuroS&P Workshops, pp.95-102, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01939845
A formal privacy management framework, Proceedings of the 5th International Workshop on Formal Aspects in Security and Trust, FAST'08, Revised Selected Papers, vol.5491, pp.162-176, 2008. ,
Geospatial Extensible Access Control Markup Language (GeoX-ACML), 2008. ,
Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies, Proceedings of the 19th IEEE Computer Security Foundations Workshop, CSFW'06, pp.85-97, 2006. ,
Formal Verification of Legal Privacy Requirements ,
, The UCON ABC Usage Control Model. ACM Trans. Inf. Syst. Secur, vol.7, issue.1, pp.128-174, 2004.
Distributed Usage Control, Commun. ACM, vol.49, issue.9, pp.39-44, 2006. ,
The Platform for Privacy Preferences, Commun. ACM, vol.42, issue.2, pp.48-55, 1999. ,
, Handbook of Automated Reasoning, vol.1, 2001.
Role-Based Access Control Models, IEEE Computer, vol.29, issue.2, pp.38-47, 1996. ,
, WP29: Guidelines on Consent under Regulation, 2016.
, WP29: Opinion 01/2017 on the Proposed Regulation for the ePrivacy Regulation, 2002.
,
P such that p ? P p ? . Assume p ? {p 1 ? dur 1 .P | ?p 2 ? dur 2 .P s.t. p 1 ? P p 2 } ,
, Given two data communication rules dcr 1 , dcr 2 ? DCR it holds that dcr 1 ? DUR dcr 2 DUR dcr 1 and dcr 1 ? DCR dcr 2 DCR dcr 2
We split the proof into the two conjuncts of Lemma 2. dcr 1 ? DUR dcr 2 DUR dcr 1 -We split the proof into the elements of data communication rules, i.e., conditions and entities and data usage rules ,
, ? dcr 1 .c ? dcr 2 .c ? dcr 1 .c
, ? dcr 1 .dur ? DUR dcr 2 .dur DCR dcr 1 .dur
, ? min
, TR ? tr 1 DCR tr 2 } · ?tr ? TR 1 s.t. tr ? DCR tr. Assume tr ? ? {tr 1 ? DCR tr 2 | tr 1 ? p 1 .TR ? tr 2 ? p 2 .TR ? tr 1 DCR tr 2 }. Then tr 1 ? p 1 .TR and tr ? DCR tr 1, ? ?tr ? ? {tr 1 ? DCR tr 2 | tr 1 ? p 1 .TR ? tr 2 ? p 2