• 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 polynomial-time adversaries can carry out on cryptographic protocols. We have defined a technique using first-order 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 g-leakage 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 geo-indistinguishability and developed a tool, called Location Guard, which can be used in order to obtain some location-based services without reveling the real location. Further plans to explore various topics: 1. Geo-indistinguishability, 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 so-called 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 input-output 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 programming-language-related 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