G. Bana, M. Okada.
Semantics for “Enough-Certainty" and Fitting’s Embedding of Classical Logic in S4Proceedings 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 ProofsComputer 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.