 Members
 Japanese Side:
 French Side:

Short description of scientific topics
 Computationally Sound Cryptographic Protocol Verification
 This research direction aims at obtaining complexity theoretic security guarantees of cryptographic protocols by using
symbolic verification techniques, suitable for automation. We want to automatically find all possible attacks probabilistic polynomialtime adversaries
can carry out on cryptographic protocols. We have defined a technique using firstorder logic, called “computationally complete symbolic attacker”: It
contains a simple set of FOL core axioms, and an additional set of axioms expressing standard cryptographic hardness and security assumptions (DDH assumption,
CPA, security etc) is continuously expanded. The technique is suitable for both indistinguishability and trace properties. If the assumptions are not
sufficient for the verification of a given protocol, attacks are delivered in a systematic manner, and new properties can be included to avoid the attacks.
Once the verification finishes, it delivers a set of properties, which, if satisfied by an implementation, ensures the security of the protocol. A number
of simple protocols have been analyzed by hand, targeting anonymity, secrecy, agreement, authentication etc., for any number of sessions. Main directions
of development: 1. Create a library of axioms for further standard cryptographic assumptions. 2. Apply the technique to important practical protocols such
as those used in passports or electronic voting. 3. Create efficient decision procedures. 4. Create an automated tool. 5. Test the tool on further
protocols.
 Quantitative Information Flow, Differential Privacy
 Quantitative Information Flow is a formal measure of the leakage of private information via the correlation
with public information.
 Differential Privacy  Catuscia Palamidesi's team
We have been contributing to the development of a framework called gleakage capturing a large class of adversaries. We are exploring connections
with game theory. Differential privacy is a framework for privacy that was originally designed for applications to statistical databases. We have
proposed an extended version that is suitable for any metric domain, and we have explored some applications. In particular, in the context of location
privacy, we have proposed the notion of geoindistinguishability and developed a tool, called Location Guard, which can be used in order to obtain
some locationbased services without reveling the real location. Further plans to explore various topics: 1. Geoindistinguishability, by considering
the case of traces. 2. The “higher order” case in which the information to be concealed is a distribution rather than a particular value. 3. The
relation with machine learning in the context of geolocation. 4. We have also proposed a variant of the socalled Kantorovich metric (generally accepted
as the most suitable bisimulation metric for trace based properties), suitable for proving differential privacy. We intend to explore efficient ways
to compute the metric, and develop a modal logic to reason about the metric.
 Side Channel Attack Resilience  Tachio Terauchi's team
In previous work, we have investigated algorithms and complexities of checking and inferring quantitative information flow, i.e., information flow analysis.
While information flow analysis traditionally concerns the regular inputoutput channel of a program, we have recently began to investigate an application
of the analysis to program's side channels. In this work, we intend to leverage our expertise on information flow analysis and other
programminglanguagerelated techniques to formally analyze how resilient a given program is to a side channel attack, or to compile a program into a form
that is resilient to such an attack.
 Security Protocol Verification Techniques for the Coq Proof Assistant