ゲーム列による安全性証明の形式化と自動化(<特集>数理的技法による情報セキュリティ)  [in Japanese] Formalization and Automation of Security Proof by Sequences of Games(<Special Topics> Formal Approach to Information Security)  [in Japanese]

Recently extensive research has been undertaken on the computational foundations of symbolic proof methods for security protocols. There are two approaches to providing such foundations. One is to give a probabilistic re-interpretation to existing symbolic methods such as the Dolev-Yao model and justify it computationally. The other is to re-formulate traditional computational arguments in an appropriate formal system and apply symbolic methods. The former approach is called indirect while the latter is called direct. This paper introduces the direct approach. Three studies on the direct approach are dealt with here, namely those by Corin and den Hartog, by Blanchet and Pointcheval, and by Canetti et al. They all formalize security proofs by sequences of games in different formal systems. We describe the formal systems they use, how they formalize probabilistic aspects and computational intractability assumptions, and the possibility of obtaining formal security proofs automatically.