Formalization and Automation of Security Proof by Sequences of Games(<Special Topics> Formal Approach to Information Security)

DOI Web Site 13 References

Bibliographic Information

Other Title
  • ゲーム列による安全性証明の形式化と自動化(<特集>数理的技法による情報セキュリティ)
  • ゲーム列による安全性証明の形式化と自動化
  • ゲームレツ ニ ヨル アンゼンセイ ショウメイ ノ ケイシキカ ト ジドウカ

Search this article

Abstract

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.

Journal

References(13)*help

See more

Details 詳細情報について

Report a problem

Back to top