Results


2020

Kawamoto, Palamidessi, and Chatzikokolakis, together with M.S. Alvim, have continued to study the interplay between defender and adversary in a game-theoretic framework. Building on their works published in POST 2018 and Entropy 2018,  where they studied the algebraic properties of the operators of visible and hidden choice that arise from the probabilistic composition of protocols, and established a hierarchy of these games, they have investigated the information leakage in interactive scenarios, in which both the adversary and the defender can behave adaptively, and methods for finding the optimal strategies at the points of equilibrium in the various cases. The results have been reported in a paper submitted to a journal.

Fernandes, Kawamoto and Murakami have proposed a mechanism providing extended DP with a wide range of metrics. The mechanism is based on locality sensitive hashing (LSH) and randomized response, and can be applied to a wide variety of metrics including the angular distance (or cosine) metric, Jaccard metric, Earth Mover’s metric, and 𝑙𝑝 metric. Moreover, the mechanism works well for personal data in a high-dimensional space. The authors have analyzed the privacy properties of the mechanism, introducing new versions of concentrated and probabilistic extended DP to explain the guarantees provided. Finally, the authors have applied the mechanism to friend matching based on highdimensional personal data with an angular distance metric in the local model. This is particularly interesting because existing local DP mechanisms, such as RAPPOR, do not work in this application. The authors have also shown through experiments that the proposed mechanism makes possible friend matching with rigorous privacy guarantees and high utility. The results have been reported in a paper submitted to a conference.

We also have proposed an epistemic approach to formalizing statistical properties of machine learning. Specifically, we have introduced a formal model for supervised learning based on a Kripke model where each possible world corresponds to a possible dataset and modal operators are interpreted as transformation and testing on datasets. Then we have formalized various notions of the classification performance, robustness, and fairness of statistical classifiers by using an extension of statistical epistemic logic (StatEL). In this formalization, we have shown relationships among properties of classifiers, and relevance between classification performance and robustness. As far as we know, this is the first work that uses epistemic models and logical formulas to express statistical properties of machine learning, and would be a starting point to develop theories of formal specification of machine learning.

2019

Kawamoto, Palamidessi, Fernandez and Romanelli have investigated a method to estimate privacy measures under the black-box assumption using machine learning. Black-box means that we don't know how the system is constructed, or that anyway it is too complicated to compute the degree of privacy via analytical methods. We only assume that it is possible to interact with the system and that thus we can input data (representing sensitive information) and observe the reaction of the system. Then, we can produce a collection of examples (data point, observable) on which we can compute the leakage of information. Related research involves the measurement of the information leakage via machine learning in a black-box scenario, on which Palamidessi and Chatzikokolakis, together with G. Cherubin, have published a paper in IEEE Security & Privacy 2019 and developed the tool F-BLEAU. Kawamoto has worked on this topic with Tom Chothia producintg several publications and the tool leakiEst. 

Bana and Okada, together with R.Chadha and A. K. Eeralla, continued developing the Bana-Comon’s technique for indistinguishability. They enriched the library of axioms with the Decisional Diffie-Hellman (DDH) assumption. Then, they analyzed the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. They provided computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol for multiple sessions, without any restrictions on the computational implementation other than the DDH assumption. They also showed authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, they axiomatized IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. They formalized the axiomatic system in an interactive theorem prover, Coq, and machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol. The work has appeared in the Transactions on Computational Logic, Volume 21 Issue 1, 2019.