| 暗号および暗号に基づく情報セキュリティ技術は、現代のネット社会では必須機能となっており、その利用は拡大する一方である。このようなシステムに安全上の問題が生じた場合その社会的な損失は甚大であり、そこで用いられる暗号および暗号応用システムの安全性を検証することは実用上極めて重要である。現在、暗号および暗号応用システムの安全性を検証・証明する方法としては、計算量理論に基づく安全性証明手法 （計算論的技法） が暗号理論における標準的技法として確立している。一方、数理的技法 (暗号論的証明手法) の立場からの安全性証明も研究されてきたが、計算論的技法との関連については、あまり研究されていなかった。ところが最近、この数理的方法が、計算論的技法の簡明化・機械化に有効であることが次第に明らかになり、その研究が活発になりつつある。数理的技法の優れている点は、証明生成・検証 (の一部) を機械化することで、証明のモジュール化や透明性が高まることであり、今後さらに増大すると思われるより複雑な暗号応用システム・プロトコルの安全性証明の簡明化に貢献することが期待される。本講演では、まず計算論的技法における最新理論である汎用的結合可能性について紹介し、さらに数理的技法およびその計算論的技法に対する有効性 (健全性/完全性) などを紹介する。 |