日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)
日本応用数理学会2011年度年会FAISオーガナイズド・セッション
日本応用数理学会2011年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2011年度年会が 2011.9.14(水)〜2011.9.16(金) に同志社大学
今出川キャンパスにて開催されます:
[年会 ホームページ]
http://mathsci.doshisha.ac.jp/jsiam2011/
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします.
奮ってご参加下さいますようお願い申し上げます.
【日時】
2011.9.16(金) 13:00--15:30
(時間が変更されました. ご注意ください.)
【会場】
同志社大学 今出川キャンパス
【参加方法】
年会ホームページをご覧ください.
【プログラム】(○: 登壇者)
[セッション1]
座長: 山本 光晴 (千葉大学大学院理学研究科基盤理学専攻)
13:00--13:20 (20分)
Toward a Library of Verified Arithmetic Functions
○AFFELDT Reynald (産業技術総合研究所 情報セキュリティ研究センター)
13:20--13:40 (20分)
計算論的に完全な記号的攻撃者と健全なプロトコル検証法
(Computationally Complete Symbolic Adversary and Sound Verification
of Security Protocols)
○バナ・ゲルゲイ (NTT コミュニケーション科学基礎研究所)
ウベール・コモン-ルンド (ENS Cachan)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
講演資料
13:40--14:00 (20分)
暗号プロトコル評価フレームワークの国際標準ISO/IEC 29128とCRYPTRECにおける適用事例
○松尾 真一郎 (独立行政法人 情報通信研究機構)
大塚 玲 (独立行政法人 産業技術総合研究所)
宮崎 邦彦 (株式会社 日立製作所)
講演資料
14:00--14:30 (30分) 休憩
[セッション2]
座長: 花谷 嘉一 ((株)東芝 研究開発センター)
14:30--14:50 (20分)
途中計算情報の漏洩に対する認証鍵交換プロトコルの安全性考察
○米山 一樹 (NTT 情報流通プラットフォーム研究所)
講演資料
14:50--15:10 (20分)
量子テレポーテーションを利用した仲介者つき量子署名方式の改良
田中 裕輝 (千葉大学 理学研究科)
○多田 充 (千葉大学 総合メディア基盤センター)
15:10--15:30 (20分)
Schnorr署名の標準モデルでの証明不可能性
○川合 豊 (東京大学 新領域創成科学研究科)
講演資料
都合によりプログラムが変更になる可能性があります.
最新情報は FAIS 研究部会のホームページでご確認ください.
[JSIAM-FAIS 研究部会ホームページ]
http://fais.jsiam.org/
【備考】
FAIS OS での発表論文には, 電子ジャーナル JSIAM Letters 誌への投稿
機会が与えられます. ただし, 投稿資格は会員に限ります.
詳しくは JSIAM Letters 誌のホームページをご参照ください.
[JSIAM Letters ホームページ]
http://jsiam.amp.i.kyoto-u.ac.jp/letters/
【重要な日程】
＊重要な日程＊
2011年8月 5日(金) 講演予稿提出締切 (予稿は2ページ)
2011年9月14日(水) 年会
〜2011年9月16日(金)
【講演概要】
--------------------------------------------------------------------
Toward a Library of Verified Arithmetic Functions
○AFFELDT Reynald (産業技術総合研究所 情報セキュリティ研究センター)
[講演概要]
Most information security infrastructures are sustained by
cryptographic functions, implemented with low-level arithmetic
functions, whose formal verification therefore becomes a prerequisite
to firmly assess any security property. In previous work, we have
already formally verified several such arithmetic functions. In order
to build a reusable library, we have been extending this work, with,
among others, signed arithmetic. As a use-case, we are now tackling
the verification of an implementation of the binary extended gcd
algorithm. To hide details inherent to the formal verification of such
a large function, our approach consists in deriving its implementation
from pseudo-code. In this presentation, we report on the current
status of the library and on preliminary results regarding its
application.
--------------------------------------------------------------------
計算論的に完全な記号的攻撃者と健全なプロトコル検証法
(Computationally Complete Symbolic Adversary and Sound Verification
of Security Protocols)
○バナ・ゲルゲイ (NTT コミュニケーション科学基礎研究所)
ウベール・コモン-ルンド (ENS Cachan)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
[講演概要]
いわゆるDolev-Yaoの記号検証法では、記号モデルの攻撃者に可能なすべての
動作をルールとして記述する。しかし、この検証法の計算論的な健全性を示す
ためには、計算論的なモデルに強い仮定が必要である。本研究では、そのかわ
りに、記号モデルの攻撃者に、特定のルールに反しない限り、あらゆる動作を
許すようにする。すなわち、攻撃者に可能なことをルールとして記述するので
はなく、攻撃者に不可能なことを記述する。このようなルールは、計算論的モ
デルの攻撃者が多項式時間であることや、暗号プリミティブの計算論的な安全
性から導かれる。さらに、このようなルールとして、Needham-Schroeder-Lowe
のプロトコルの安全性を検証できるものについて議論する。
--------------------------------------------------------------------
暗号プロトコル評価フレームワークの国際標準ISO/IEC 29128とCRYPTRECにおける適用事例
○松尾 真一郎 (独立行政法人 情報通信研究機構)
大塚 玲 (独立行政法人 産業技術総合研究所)
宮崎 邦彦 (株式会社 日立製作所)
[講演概要]
暗号プロトコル安全性検証を行う際に必要となる評価のフレームワークと評価結
果のレベル分けを行うためのISO/IEC JTC1における国際標準ISO/IEC 29128が
FDIS段階に進み、標準化作業もほぼ完了してている状況である。一方で、電子政
府推奨暗号のための評価を行うCRYPTRECにおいて、エンティティ認証プロトコル
の評価が行われているが、ここで形式検証による脆弱性が発見されるなど、形式
化手法の情報システムに対する実適用に向けて環境と事例が整ってきている。本
発表では、ISO/IEC 29128のFDISの概要を示すとともに、CRYPTRECにおける評価
結果とその結果に基づく対応を示す。
--------------------------------------------------------------------
途中計算情報の漏洩に対する認証鍵交換プロトコルの安全性考察
○米山 一樹 (NTT 情報流通プラットフォーム研究所)
[講演概要]
SCN2010にて提案された認証鍵交換プロトコルSMQVの安全性の再考察を行う。
SMQVは途中計算情報の漏洩に対しても安全であると主張されているが、
本発表では安全性証明の誤りを指摘し、同一の数学的仮定の下では証明を
repairすることが困難であることを示す。また、従来のDiffie-Hellman型
認証鍵交換プロトコルを、途中計算情報漏洩に対して達成可能な安全性
レベルごとに分類し、（現状では）そのような漏洩に対して安全なプロトコル
が存在しないことを示す。
--------------------------------------------------------------------
量子テレポーテーションを利用した仲介者つき量子署名方式の改良
田中 裕輝 (千葉大学 理学研究科)
○多田 充 (千葉大学 総合メディア基盤センター)
[講演概要]
従来の量子署名方式は仲介者の無い真の署名方式にしようとすれば
まだ安全性が完全に証明されていない概念を必要とし，仲介者つきの
方式においては仲介者は絶対的に信用できるという前提を必要としていた．
今回新たに提案した方式は，仲介者を必要とするものの量子鍵配送と
one-time pad暗号に基づいた無条件安全性を持ち、検証に仲介者を
必要とするが、既存の方式とは違い，仲介者を絶対的に信頼できる
という前提をなくした、より現実的な設定で利用可能となっている。
--------------------------------------------------------------------
Schnorr署名の標準モデルでの証明不可能性
○川合 豊 (東京大学 新領域創成科学研究科)
[講演概要]
デジタル署名の代表例であるSchnorr署名は，離散対数問題が困難ならば，
ハッシュ関数を理想化したモデルであるランダムオラクルモデル（ROM）に
おいて安全であることが証明されている．しかしながら，ランダムオラクル
を仮定しないモデル（標準モデル）において安全かは証明されていない．
本稿では，安全性証明時の帰着がある制限を持っている場合は，いかなる
non-interactiveな計算量問題の困難さにも安全性を帰着することができない，
すなわち安全性を証明することができないことを示す．
--------------------------------------------------------------------
【問い合わせ先】
塚田 恭章 (NTTコミュニケーション科学基礎研究所)
tsukada.yasuyuki(at)lab.ntt.co.jp
最終更新: 2011.10.1
FAISホームページにもどる．