日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)

日本応用数理学会2006年度年会FAISオーガナイズドセッション

                   日本応用数理学会2006年度年会
              FAIS オーガナイズドセッションプログラム
                「数理的技法による情報セキュリティ」

下記の日程で, 日本応用数理学会2006年度年会
「数理的技法による情報セキュリティ」(FAIS)研究部会オーガナイズドセッション
を開催いたします. 奮ってご参加下さい. 

なお, 本オーガナイズドセッションは, 通常の FAIS 研究集会とは異なり参加費が
必要となります. 参加にあたっての詳細は, 年会のホームページをご覧下さい. 

【日時】

    2006年9月16日(土) 10:30〜12:00

【会場】

    筑波大学 春日キャンパス (茨城県つくば市春日)
    詳細は日本応用数理学会2006年度年会ホームページをご覧下さい. 
    
【プログラム】

    [座長] 藤原 融 (大阪大学)

    10:30--11:15  萩谷 昌己 (東京大学)
    [特別講演] 数理的技法によるセキュリティプロトコルの検証
    講演資料

    11:15--12:00  岡本 龍明 (NTT)
    [特別講演] 汎用的結合可能性と数理的技法への期待
    講演資料

    講演の概要については下記をご覧下さい. 

【問い合わせ先】

    塚田 恭章
    NTTコミュニケーション科学基礎研究所
    tsukada(at)theory.brl.ntt.co.jp

    FAIS 研究集会に関する情報はFAISホームページにてご覧いただけます. 

【講演概要】

    10:30--11:15  萩谷 昌己 (東京大学)
    [特別講演] 数理的技法によるセキュリティプロトコルの検証
    講演概要: 
    　暗号プロトコルに対する計算論的アプローチと記号論的アプローチを融合
    しようとする試みが盛んに行われている。前者は根底にある暗号の脆弱性も
    考慮に入れつつ、主として確率的多項式時間チューリング機械の枠組みを用
    いて暗号プロトコルの解析を行う。後者は、いわゆるDolev-Yaoモデルに代
    表されるように、根底にある暗号は絶対に破られないという仮定のもとで、
    通信路に流れるメッセージを記号（から作られる木構造）に理想化して暗号
    プロトコルの検証を行う。
    　いうまでもなく、前者のアプローチは実際の暗号プロトコルの実装に即し
    たものであり、暗号プロトコルの現実的な解析を行うためには必須である。
    しかしながら、このアプローチによる解析は確率的多項式時間チューリング
    機械の還元を中心にしたものになり、煩雑な議論が長々と続き機械化も容易
    ではない。実際に、正当性を証明したとされるプロトコルの間違いが後に見
    つかることがしばしばある。
    　これに対して、後者の記号論的なアプローチでは、数理的技法（formal 
    methods）における各種の技術を駆使する。特に並行システムの記述に用い
    られる並行計算や、ストランド空間（strand space）などの暗号プロトコル
    に特化した意味モデルに基づいて、汎用的なモデル検査系や専用の検証系を
    用いて、ある程度機械的に暗号プロトコルの検証が可能となっている。しか
    しながら、このアプローチは根底にある暗号を理想化しているため、暗号の
    特徴を利用した攻撃を扱うことができない。
    　そこで、この二つのアプローチを融合する試みが盛んになっている。特に、
    IEEE Computer Security Foundations Workshop、Theory of Cryptography 
    Conference、ICALP Track Cなどにおいて二つのアプローチを融合する研究
    が数多く発表されており、最近ではFormal and Computational Cryptography
    というこの分野に特化したワークショップも開催されている。
    　二つのアプローチを融合する方法は大きく二つに分類される。一つは計算
    論的な解析を形式体系の中で定式化した上で記号論的アプローチに基づく自
    動検証技術を導入するもの（いわゆる直接的方法）。もう一つは記号論的な
    推論に計算論的な解釈を与えるもの（いわゆる間接的方法）である。
    　本講演では、二つのアプローチを融合する試みについて概観し、その問題
    点や将来の方向性について議論したい。

    11:15--12:00  岡本 龍明 (NTT)
    [特別講演] 汎用的結合可能性と数理的技法への期待
    講演概要: 
    　暗号および暗号応用システムの安全性を検証する方法としては，計算量理
    論に基づく安全性証明手法（計算論的証明手法）が標準的手法として暗号理
    論において確立している．一方，それら安全性を数理的技法（記号論理的証
    明手法）の立場から捉えた研究も活発に行なわれてきた．しかし，従来これ
    ら二つの手法の相互関係についてはほとんど研究されていなかった．
    　最近，標準的安全性証明（計算論的証明）に対する数理的技法の有効性（
    健全性／完全性）などが研究されるようになり，数理的技法が，計算論的証
    明手法の簡明化・機械化に有効であることが明らかになりつつある．
    　本講演では，最近急速に進展しつつある新しい計算論的証明手法（汎用的
    結合可能性，ゲーム列による証明手法など）の立場から，これら数理的技法
    との関係を捉えると共に，数理的技法に対する期待を述べる．