Formalization of Differential Privacy in Isabelle/HOL
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909362591629312 |
|---|---|
| author | Sato, Tetsuya Minamide, Yasuhiko |
| author_facet | Sato, Tetsuya Minamide, Yasuhiko |
| contents | Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade.
In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_15386 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formalization of Differential Privacy in Isabelle/HOL Sato, Tetsuya Minamide, Yasuhiko Logic in Computer Science Cryptography and Security Programming Languages Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism. |
| title | Formalization of Differential Privacy in Isabelle/HOL |
| topic | Logic in Computer Science Cryptography and Security Programming Languages |
| url | https://arxiv.org/abs/2410.15386 |