国立大学法人東北大学電気通信研究所公式ウェブサイト|Research Institute of Electrical Communication Tohoku University

コンピュータサイエンス研究会 講演会

研究会名:コンピュータサイエンス研究会 講演会
開催日:2009年9月15日 (火) 15:00~17:00
題目:暗号プロトコルの形式的検証の計算論的健全性
講師:川本 裕輔(東京大学)
開催場所:東北大学電気情報系3号館206号室


コンピュータサイエンス研究会 講演会の御案内

コンピュータサイエンス研究会
主査   小林直樹

下記のようにコンピュータサイエンス研究会の講演会を開催いたしますので,ご案内申し上げます.

  • 日時:2009年9月15日(火)15:00~17:00
  • 場所:東北大学 電気情報系3号館 206号室
  • 題目:暗号プロトコルの形式的検証の計算論的健全性
  • 話者:川本 裕輔(東京大学)
  • 概要:暗号プロトコルの安全性の検証手法には、計算論的手法と形式的手法(formal method)があり、それぞれ独立に発展してきた。計算論的手法は、暗号プリミティブの脆弱性を考慮に入れ、計算量理論に基づいて解析するため、現実世界に忠実だが複雑で間違いやすい。一方、形式的手法は、暗号プリミティブの理想的な安全性を仮定し、メッセージや攻撃を記号表現に抽象化し、数理論理学に基づいて解析するため、単純で自動化しやすいが現実世界に忠実でない。
    近年、両手法を関連付けて双方の長所を生かすために、プロトコルの形式的検証の「計算論的健全性」に関する研究が、Abadi とRogaway による研究に始まり、数多く行われている。形式的検証の計算論的健全性とは、「形式的手法によるプロトコルの安全性証明が計算量理論に基づく安全性を保証する」という性質である。つま り、ある形式的手法が計算論的に健全であれば、その形式的手法を用いて安全であると確かめれたプロトコルは、必ず計算論的手法による解析によっても安全であるといえる。そのため、計算論的健全性は、形式的手法の既存の検証技術を活用する上で重要な性質である。
    本講演では、公開鍵暗号とハッシュ関数を扱えるapplied pi-calculusの計算論的健全性、すなわち二つのプロセスが観測同値であるとき、能動的攻撃者の下で計算量的に識別不能であることを示す。能動的攻撃者を扱ういかなる先行研究においても、計算論的健全性の証明では、ビット列を受け取り記号表現を返すパーズ関数が多項式時間計算可能であることを必要としていたが、そのために、ハッシュ関数や排他的論理和などの暗号プリミティブが扱えなかったり、ハッシュ関数を扱うために、シミュレータがランダムオラクルをシミュレートできるという強い仮定が必要だった。そこで、本研究では、パーズ関数が多項式時間計算可能であることを必要としない新たな証明技法を用いて、計算論的健全性を示す。
    なお、本講演では計算論的手法や計算論的健全性についての知識を前提とせず、講演の前半にこれらを詳しく説明する予定である。

問い合わせ先

小林  直樹

koba ecei.tohoku.ac.jp