[logic-ml] Talk by Gergei Bana (26 Mar 11:00-)

[Shinya Katsumata]

京都大学数理解析研究所の勝股です。

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”.