A. Anderson, A. Nadalin, M. Mcintosh, M. Kudo, and S. Proctor, , 2004.

P. Ashley, S. Hada, G. Karjoth, C. Powers, and M. Schunter, Enterprise Privacy Authorization Language (EPAL). IBM Research, 2003.

M. Azraoui, K. Elkhiyaoui, M. Önen, K. Bernsmed, A. S. De-oliveira et al., 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.

C. Baier and J. Katoen, Principles of Model Checking, 2008.

C. Barrett and C. Tinelli, Satisfiability Modulo Theories, pp.305-343, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01095009

A. Barth, A. Datta, J. C. Mitchell, and H. Nissenbaum, Privacy and Contextual Integrity: Framework and Applications, Proceedings of the 27th IEEE Symposium on Security and Privacy, S&P'06, pp.184-198, 2006.

M. Becker, A. Malkis, and L. Bussard, S4P: A Generic Language for Specifying Privacy Preferences and Policies, 2010.

M. Cunche, D. Le-métayer, and V. Morel, A Generic Information and Consent Framework for the IoT, Inria, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01953052

H. Deyoung, D. Garg, L. Jia, D. K. Kaynar, and A. Datta, 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.

S. Du, M. Ibrahim, M. S. Shehata, and W. M. Badawy, 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.

. Electronic-fountrier-foundatino, Automated License Plate Readers (ALPR, 2017.

P. Emami-naeini, S. Bhagavatula, H. Habib, M. Degeling, L. Bauer et al., Privacy Expectations and Preferences in an IoT World, Proceedings of the 13th Symposium on Usable Privacy and Security, SOUPS'17, pp.399-412, 2017.

A. Gerl, N. Bennani, H. Kosch, and L. Brunie, 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

M. Hilty, A. Pretschner, D. A. Basin, C. Schaefer, and T. Walter, 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.

G. J. Holzmann, The SPIN Model Checker -Primer and Reference Manual, 2004.

J. De, S. Le-métayer, and D. , Privacy Risk Analysis, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01420968

J. De, S. Le-métayer, and D. , 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

L. Métayer and D. , 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.

A. Matheus and J. Herrmann, Geospatial Extensible Access Control Markup Language (GeoX-ACML), 2008.

M. J. May, C. A. Gunter, and I. Lee, 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.

R. Pardo and D. Le-métayer, Formal Verification of Legal Privacy Requirements

J. Park and R. S. Sandhu, The UCON ABC Usage Control Model. ACM Trans. Inf. Syst. Secur, vol.7, issue.1, pp.128-174, 2004.

A. Pretschner, M. Hilty, and D. A. Basin, Distributed Usage Control, Commun. ACM, vol.49, issue.9, pp.39-44, 2006.

J. Reagle and L. F. Cranor, The Platform for Privacy Preferences, Commun. ACM, vol.42, issue.2, pp.48-55, 1999.

A. J. Robinson and A. Voronkov, Handbook of Automated Reasoning, vol.1, 2001.

R. S. Sandhu, E. J. Coyne, H. L. Feinstein, and C. E. Youman, 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.

. Inria,

. }-·-?p-?-?-dur-2, 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

. Proof, 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