日本応用数理学会2014年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2014年会が 2014.9.3(水)〜2013.9.5(金) に
政策研究大学院大学にて開催されます:
[年会 ホームページ]
http://jsiam2014.jsiam.org/
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします.
今回はFAIS研究会 初の試みとしてチュートリアル講演も企画しました.
プロトコルの結合可能安全性やツールを使った自動検証などの基本的な内容に
加え、最近盛んになっている両者の融合研究(Dahl & Damgard, Eurocrypt2014)
についても解説します。
奮ってご参加下さいますようお願い申し上げます.
【日時】
9月5日(金) 9:30-10:50
【会場】
政策研究大学院大学 (東京都港区六本木)
【参加方法】
年会ホームページをご覧ください.
【プログラム】(○: 登壇者)
研究部会OS：数理的技法による情報セキュリティ ［9月5日：09:30-10:50：D会場］
座長: 花谷 嘉一 （(株)東芝 研究開発センター）
9:30-9:50
可変長情報源符号化順定理の形式化
○小尾 良介 (千葉大学大学院理学研究科)
[概要]
現代数学における証明は膨大な長さになりつつあり、証明の信頼性の問題が発
生している。定理証明支援系を用いた形式的検証は、これらの証明の正当性を
保証するための解決策として近年現れた。長い証明を形式的に検証する前に、
形式的な定義、定理の確立されたライブラリを構築する必要がある。我々は既
存のライブラリに「可変長情報源符号化順定理」を加えることによってどう情
報理論の形式化に貢献したのかを説明する。
9:50-10:10
チュートリアル：暗号プロトコルの結合可能安全性とその形式検証
○米山 一樹 (NTTセキュアプラットフォーム研究所)
[概要]
高機能なシステムを実現するためには、複数の暗号プロトコルを組み合わせる
必要があるが、一般に個別には安全なプロトコルであっても、組み合わせたシ
ステムが安全とは限らない。組み合わせても安全性が損なわれない性質を、結
合可能安全性 と呼ぶ。しかし、結合可能安全性の証明は一般に複雑であるた
め、証明を形式検証で行う技術が提案されている。本発表では、結合可能安全性
とその形式検証技術についての過去の研究を紹介する。
10:10-10:30
チュートリアル：結合可能安全性の形式検証における最近の研究動向
○吉田 真紀 (情報通信研究機構)
[概要]
結合可能安全性の形式検証の提案以降、様々な拡張が試みられている。最近、
Eurocrypt2014で、形式検証の枠組みが整備され、結合可能安全性の定式化に近
い形で検証対象を定義可能となった。さらに検証 対象が拡張され、新たに準同
型暗号などを用いたプロトコルが検証可能となり、紛失通信プロトコルに適用
されている。本発表では、上記成果を解説し、今後の研究の展望について紹介
する。
10:30-10:50
チュートリアル：ProVerifによる結合可能安全性の形式検証
○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
[概要]
セキュリティ・プロトコルの安全性を自動的に検証するツールとして広く用い
られているProVerifについて解説する。プロトコルの記述のしかたや安全性の
記述のしかた、検証結果の読みかたに加え、検証において注意すべき点などに
ついても述べる。ProVerifは認証や秘匿性などを含むいくつかの種類の安全性
を検証できるが、ここでは特に、結合可能安全性の自動検証に用いられた観測
等価性の検証について述べる。
最新情報は年会のホームページでご確認ください.
【問い合わせ先】
櫻田 英樹 (NTTコミュニケーション科学基礎研究所)
sakurada.hideki(at)lab.ntt.co.jp
最終更新: 2014.9.8