Publications

  • G. Bana, M. Okada. Semantics for “Enough-Certainty" and Fitting’s Embedding of Classical Logic in S4 Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), to appear, 2016.
  • Yusuke Kawamoto, Fabrizio Biondi and Axel Legay. Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow. Proc. of 21st International Symposium on Formal Methods (FM 2016), LNCS 9995, pp.1-20, November 2016.
  • M. Alvim, K. Chatzikokolakis, A. McIver, C. Morgan, C. Palamidessi and G. Smith. Axioms for Information Leakage. Proc. of CSF '16, IEEE Computer Society Press, pp. 77-92, 2016.
  • Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Temporal Verification of Higher-Order Functional Programs. Proc. of POPL 2016, ACM SIGPLAN Notices 51 (1), pp. 57-68, ACM, 2016.
  • Yusuke Kawamoto. Verification of Cryptosystems - from Introduction to Computer-Aided Security Proofs Computer Software. Vol.33 No.3, October 2016. (Invited, tutorial paper in Japanese)
  • Yusuke Kawamoto. Quantification of information leakage by statistical method combined with program analysis. Second Joint Workshop between France and Japan on Cybersecurity, September 2016.
  • Tachio Terauchi. On Predicate Refinement Heuristics in Program Verification with CEGAR. 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016), Eindhoven, Netherlands, 2016. (Invited talk)
  • Okada. What is logic. Cerisy Meeting “What is logic?” (invited paper) International Cultural Centre of Cerisy, May 2017.
  • Hubert Comon, Adrien Koutsos. Formal Computational Unlinkability Proofs of RFID Protocols. 30th IEEE Computer Security Foundations Symposium (CSF 2017), pp.100-114, 2017.
  • Mário S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, Catuscia Palamidessi. Information Leakage Games. 8th International Conference on Decision and Game Theory for Security (GameSec 2017), LNCS 10575, pp.437-457, October 2017.
  • Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, and Louis-Marie Traonouez. HyLeak: Hybrid Analysis Tool for Information Leakage. 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), LNCS 10482, pp.156-163, October 2017.
  • Yusuke Kawamoto, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. On the Compositionality of Quantitative Information Flow. Logical Methods in Computer Science, Vol.13, No.3:11, pp.1-31, August 2017.
  • Yusuke Kawamoto. Models and Mechanisms for Quantitative Privacy. JSIAM 2017 Annual Meeting. Invited talk at Formal Approach to Information Security Activity Group, September 2017. (In Japanese).
  • HyLeak (Hybrid analysis tool for information leakage). Software, April 2017. Available at https://project.inria.fr/hyleak
  • Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels. 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), ACM SIGPLAN Notices 52 (6), pp.362-375. ACM, June, 2017.
  • Arthur Blot, Masaki Yamamoto, and Tachio Terauchi. Compositional Synthesis of Leakage Resilient Programs. 6th International Conference on Principles of Security and Trust (POST 2017), LNCS 10204, pp.277-297, Springer, April, 2017.
  • Gergei Bana, Rohit Chadha, and Ajay Kumar Eeralla. Formal Analysis of Vote Privacy Using Computationally Complete Symbolic Attacker. ESORICS (2), 2018: 350-372
  • Mitsuhiro Okada and Yuta Takahashi. On quasi-ordinal diagram systems. Proceedings of TERMGRAPH 2018 (10th International Workshop on Computing with Terms and Graphs), Oxford, UK, July 2018, 12 pages.
  • Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, and Louis-Marie Traonouez. Hybrid Statistical Estimation of Mutual Information and its Application to Information Flow. Formal Aspects of Computing, 2018, To appear.
  • Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi. A Game-Theoretic Approach to Information-Flow Control via Protocol Composition. Entropy, 20(5:382), pp.1-43, May 2018.
  • Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto, and Catuscia Palamidessi. Leakage and Protocol Composition in a Game-Theoretic Perspective. In Proc. of the 7th International Conference on Principles of Security and Trust (POST 2018), Lecture Notes in Computer Science, Vol. 10804, pp. 134-159, April 2018.
  • Y. Nanjo, H. Unno, E. Koskinen, and T. Terauchi. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In Proc. of LICS'18, pp. 759-768, ACM, 2018.
  • H. Unno, Y. Satake, and T. Terauchi. Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs. In Proc. of POPL'18, 12, pp.12:1-12:29. ACM, January, 2018.