During the first year of the project, we made advances in several directions of our research program.
Gergei Bana and Mitsuhiro Okada re-considered the classical first-order semantics developed in [Bana-Comon POST'12] for symbolic verification of reachability properties, in the "provable security" framework of computer security, as a special case of Fitting's embedding of classical logic in S4. They showed how it can be generalized to treat situations in which satisfaction is allowed to fail on sets that are considered insignificant. The results of this work were published at CSL'16, and a journal version is under preparation.
Hubert Comon and Adrien Koutsos applied the previously developed technique for indistinguishability properties to verify computational unlinkability in case of RFID protocols. The results of this work are under preparation for publication.
Yusuke Kawamoto developed a hybrid statistical method that combines precise and statistical analyses for estimating mutual information in probabilistic systems. This method is useful for quantitative information flow analysis on large systems. The results of this work were published at FM 2016.
Yusuke Kawamoto, Konstantinos Chatzikokolakis and Catuscia Palamidessi extended their previous work on the compositional analysis of large systems in the Quantitative Information Flow model. The results of this work were submited for publication to the LMCS journal.
Konstantinos Chatzikokolakis and Catuscia Palamidessi developed an axiomatic study of leakage for Quantitative Information Flow, showing important dependencies among different axioms and establishng a completeness result about the g-leakage family. The results of this work were published in CSF’16.
Yusuke Kawamoto, Konstantinos Chatzikokolakis and Catuscia Palamidessi have been working on modelling the information leakage under adaptive/probabilistic attackers. This work is under development.
During the second year of the project, we made further progress in our research program.
Gergei Bana and Mitsuhiro Okada continued developing the formal methods for cryptographic protocol verification called Computationally Complete Symbolic Attacker. They revised the work published last year in CSL 2016, the "provable security" semantics for reachability properties, as a special case of Fitting's embedding of classical logic in S4, where the computational model was treated in the possible world semantics and Fitting’s embedding guaranteed computational soundness of first-order logical-formal methods of protocol verification. They also hinted applications of this semantics in other fields of computer science such as conditional logic and default reasoning. This work is ready for submission to a journal.
Furthermore, Bana and Okada continued developing the Bana-Comon’s technique for indistinguishability to enrich the library of axioms with axiomatizing the DDH assumption, various security levels of encryptions such as CPA, CCA security, unforgeability of signatures, verified various versions of Diffie-Hellman key exchange, some in a mechanized manner with the Coq proof assistant. This is a collaborative work with researchers of the University of Missouri and is undersubmission to a journal. The above work includes initial work on partial completeness of axiomatization, which will be one of the next year’s targets.
In order to understand some foundational issue of formal methods and formal-rule based proof methods, Okada gave a review and reconsideration of formal logical proofs. [Proc. “Beyond Logic”, May 2017, Centre culturel international de Cerisy-la-Salle (CCIC)].
Hubert Comon and Adrien Koutsos studied proofs of RFID protocols in the computational model, relying on the computationally complete symbolic attacker: design of axioms for hash functions, formalization of computational unlikability, applications to case studies. This work was published in IEEE CSF 2017).
In an ongoing work, Comon and Koutsos design an algorithm that decides if a set of cryptographic games/game transformations allows to prove the security of a given protocol. In other words, they aim at deriving a decision result for the Bana-Comon logic (CCS 2014).
Yusuke Kawamoto (together with Fabrizio Biondi, Axel Legay, and Louis-Marie Traonouez at Inria Rennes) developed and released the analysis tool HyLeak for estimating mutual information in probabilistic systems by combining precise program analysis and statistical analysis for source codes. As far as we know this is the first freely available tool using the hybrid method for quantifying information leakage. The tool paper was published at ATVA 2017 conference. The tool is available at https://project.inria.fr/hyleak/.
Yusuke Kawamoto, Konstantinos Chatzikokolakis and Catuscia Palamidessi extended their previous work on the compositional analysis of large systems in the quantitative information flow model. The results of this work were published in the journal Logical Methods in Computer Science.
Chatzikokolakis, Kawamoto, and Palamidessi (together with Mário S. Alvim) have proposed the notion of information leakage game, a game-theoretic model for information leakage under adaptive / probabilistic attackers. More specifically, they employ game theory to study information leakage in interactive scenarios, in which both an adversary and a defender can behave adaptively. The results of this work were published at GameSec 2017 conference.
Chatzikokolakis, Kawamoto, and Palamidessi also studied the two operators (visible and invisible choice) that arise from the probabilistic composition of protocols, and their algebraic properties. Continuing the previous work of formalizing the interplay between defender and adversary in a game-theoretic framework, they established a hierarchy of these games, and provided methods for finding the optimal strategies (at the points of equilibrium) in the various cases. This work was submitted for publication. Moreover, in an ongoing work, Chatzikokolakis, Kawamoto, and Palamidessi have been working on extending the information leakage game framework to various settings.
Tachio Terauchi investigated methods for synthesizing leakage resilient circuits, under the n-threshold probing model of leakage resilience which is a formal notion of side channel attack resilience related to probabilistic non-interference. The work proves a new compositionality property of the leakage resilience model, and utilizes it to develop a method that can efficiently synthesize compact circuits with a high degree of resilience. The result of the work is published in POST 2017, and was nominated for the best paper award.
Tachio Terauchi investigated methods for detecting and proving the absence of timing channel attacks. The work proposes an idea called phi-quotient partitioning whereby the given program's traces are decomposed in such a way that proving the timing channel security of the decomposed components imply the security of the whole. The method is shown to be effective for detecting and proving the absence of timing channel attacks in real-world systems, and also is generalized to be applicable to arbitrary k-safety hyperproperties. The result of the work is published in PLDI 2017.
During the final year of the project, we made further progress in our research program.
Chatzikokolakis, Kawamoto, and Palamidessi (together with Mario S. Alvim) studied the two operators (visible and hidden choice) that arise from the probabilistic composition of protocols, and their algebraic properties. Continuing the previous work of formalizing the interplay between defender and adversary in a game-theoretic framework, they established a hierarchy of these games, and provided methods for finding the optimal strategies (at the points of equilibrium) in the various cases. This work was published at POST 2018 and an extended version at the journal Entropy.
Moreover, Chatzikokolakis, Kawamoto, and Palamidessi have been investigating a variant of leakage games to differential privacy. They are also working on extending the information leakage game framework to various settings.
Gergei Bana and Mitsuhiro Okada continued developing the formal methods for cryptographic protocol verification called Computationally Complete Symbolic Attacker (CCSA). They revised the work published in CSL’16, the "provable security" semantics for reachability properties, as a special case of Fitting's embedding of classical logic in S4, where the computational model was treated in the possible world semantics and Fitting’s embedding guaranteed computational soundness of first-order logical-formal methods of protocol verification. They also hinted applications of this semantics in other fields of computer science such as conditional logic and default reasoning. This work is ready for submission to a journal.
Furthermore, Bana and Okada continued developing the Bana-Comon’s technique for indistinguishability to enrich the library of axioms with axiomatizing the DDH assumption, various security levels of encryptions such as CPA, CCA security, unforgeability of signatures, verified various versions of Diffie-Hellman key exchange, some in a mechanized manner with the Coq proof assistant. This is a collaborative work with researchers of the University of Missouri and is undersubmission to a journal. The above work includes initial work on partial completeness of axiomatization, which will be one of the next year’s targets. This work has been submitted to Transactions on Computational Logic.
Gergei Bana has also worked with researchers at the University of Missouri to apply the CCSA technique to electronic voting. They have published their results on the FOO voting protocol at Esorics'18.
Adrien Koutsos, Hubert Comon's student has obtained decidability results for the indistinguishability version of the CCSA. His paper, "Deciding Indistinguishability" is in the process of publication.
Tachio Terauchi made contributions on general techniques for temporal property verification of higher-order programs, resulting in publications at POPL 2018, LICS 2018.