プログラム / 講演・テーマ展示一覧 /
テーマ展示
概要
暗号はセキュリティを支える重要な技術です．しかしどんなに強力な暗号を用いても，複雑化した情報システムでは，設計者が想定しない情報漏洩などがおこる危険性があります．一方フォーマルメソッドは，システムの正しさを数学の証明問題を解くのと同じ厳密さで検証することによって，高い安全性を実現する方法論です．フォーマルメソッドと暗号理論，別々に発達した2つの研究分野を融合することで，システムの安全性をより確実に保証します．
本テーマ展示では， という3項目について，ご紹介します．
本テーマ展示では， という3項目について，ご紹介します．
展示紹介ムービー
1分23秒
個別展示
フォーマルメソッドと暗号理論をつなぐ鍵 －論理学と確率論をつなぐ－
どんな研究？
高いセキュリティを持つ情報システムを実現する研究です．厳密な検証を目的とするフォーマルメソッドと，安全な仕組みを提供するために発展した暗号理論との融合で，情報セキュリティ分野の革新的新領域を創出します．
どこが凄い？
フォーマルメソッドの記号論理学的な表現と，暗号理論の確率的な概念の対応関係を明らかにしました．これにより，フォーマルメソッドによる暗号の安全性証明や，暗号理論による検証方法論の正当化などが可能になりました．
もたらされる変革
高度な暗号を駆使した情報システムの安全性を，フォーマルメソッドによって厳密かつ効率的に検証できるようになります．特に高い安全性を求められる電子政府などのシステムを実現するための，基礎技術を提供します．
関連文献
- 真野，櫻田，河辺，塚田，“ゲーム列による安全性証明の形式化と自動化”，応用数理，vol．17，no．4，pp．38-46，2007． [ Webpage ]
- 萩谷，塚田（編），数理的技法による情報セキュリティ，日本応用数理学会監修，シリーズ・応用数理，共立出版，2009 年刊行予定．
個別展示紹介ムービー
99.999…%安全です －フォーマルメソッドから暗号理論へ －
どんな研究？
「通信を行うシステムがフォーマルメソッドを用いた検証によって『安全である』とされた場合には，暗号学的な意味においても安全である」ということを証明しました．
どこが凄い？
「安全である」か「安全でない」かの二者択一の判定を行うフォーマルメソッドと，攻撃の成功確率と所要時間で安全性を測る暗号理論との関連性を明らかにし，双方の利点を活かしました．
もたらされる変革
フォーマルメソッドによるセキュリティ検証方法が暗号理論的にも十分信頼性が高いことを示しました．これにより，電子政府などのセキュリティの検証を厳密かつ簡単に行うことができます．
関連文献
- G. Bana, Y. Kawamoto, H. Sakurada, “Computational Soundness of (Interactive) Zero-Knowledge Proof Systems in the Presence of Active Adversaries,” Computational and Symbolic Proofs of Security, 2009. [ PDF ]
個別展示紹介ムービー
頑固なバグも楽々発見 － 暗号理論からフォーマルメソッドへ －
どんな研究？
秘密の漏洩，データの改ざんを防ぐセキュリティプロトコルの安全性を，計算機を使って正確に検証します．
どこが凄い？
実用的な時間で，プロトコルが「安全」か「安全でない」かを自動的に判別し，どこにバグがあるかも指摘します．
もたらされる変革
専門家でも苦労していたセキュリティプロトコルの安全性証明を，計算機で自動的に行うことができます．高度なプロトコルの設計効率を大幅に改善し，どのような不正攻撃に対しても安心なインターネットサービスを提供することができます．
関連文献
- T. Araragi and O. Pereira : Automatic Verification of Simulatability in Security Protocols, the 4th International Conference on Information Assurance and Security 2008, IAS 2008, pp.275―280, 2008.
個別展示紹介ムービー
[