京都大学数理解析研究所の勝股です。
3月26日11:00から、INRIA Paris-RocquencourtのGergei Bana氏に 以下の講演をしていただくことになりましたので、 ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 26 Mar, 2015 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (See 34) 京都大学 本部構内 総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)
Speaker: Gergei Bana (INRIA Paris-Rocquencourt)
Title: Formal Verification of Complexity-Theoretic Properties of Security Protocols
Abstract: Rigorous modeling of attackers to security protocols, and hence the prospect of proving the security of protocols has been developed from the 1980’s in two directions. One focused on automated proving and accordingly modeled protocol execution and attackers with a set of symbolic operations on symbolic terms, treating cryptographic primitives such as encryption as black-box operations (Dolev-Yao approach). The other took a complexity-theoretic approach, modeled protocol execution and attackers as probabilistic polynomial-time algorithms with the aim of deriving protocol security from hardness assumptions such as the DDH assumption (computational approach). While the first technique is convenient for automation and is effective in finding attacks, there is little guarantee that if there is no Dolev-Yao attack, then there is no real-life attack either. Computational approach approximates real life far closer, but is not convenient for automation, proving by hand is too laborious and error prone. From the beginning of the 2000’s there have been numerous research directions trying to unify the two approaches and provide automated verification of computational properties, with variable success. In this talk we briefly review the history of the unification process, the failed attempts, the currently available tools, and we give a more detailed account of our approach with Hubert Comon-Lundh of ENS Cachan and Mitsuhiro Okada of Keio University, which we call “computationally complete symbolic attacker”.