形式検証を活用した暗号システムの安全性証明技術 On Security proof Technique for Cryptographic Systems Using Formal Verification

この論文をさがす

著者

    • 花谷, 嘉一 ハナタニ, ヨシカズ

書誌事項

タイトル

形式検証を活用した暗号システムの安全性証明技術

タイトル別名

On Security proof Technique for Cryptographic Systems Using Formal Verification

著者名

花谷, 嘉一

著者別名

ハナタニ, ヨシカズ

学位授与大学

電気通信大学

取得学位

博士 (工学)

学位授与番号

甲第676号

学位授与年月日

2012-03-23

注記・抄録

博士論文

2011

暗号理論の黎明期には,暗号システムの安全性検証は設計者の勘と経験により行われていた.そのため,設計者の想定外の攻撃により破られることがあるだけでなく,第三者による暗号システムの安全性の再検証は困難という問題を抱えていた.そのような背景から,1980 年代に,安全性証明という技術が開発された.安全性証明では,攻撃をモデル化し,そのモデルにおいて生じうる攻撃に対して安全であることを数学的に証明する.モデルに属する全ての攻撃に対して安全性が保証できるだけでなく,第三者により証明の正しさが再検証可能であるという利点を持つ.安全性証明は学術的にだけではなく,産業的にも重要である.特に,産業的な立場からは,安全性証明中のミスの防止と負担の軽減が大きな課題となっている.そこで,本研究では,安全性証明を備えた暗号システムの提案を行うだけでなく,安全性証明の工夫と形式検証の活用によるミスの防止と負荷の軽減を試みる.また,記号的安全性では,実用に供されているシステムとの隔たりが大きいため,より高い安全性を評価できる計算量的安全性の検証に焦点を当てる.通常の計算量的安全性の証明は,暗号システムへの攻撃問題を計算量的仮定に帰着することで行われる.本論文では,人手による安全性証明の複雑さを緩和するために,計算量的仮定まで帰着するのではなく,構成要素とする部品の計算量的安全性に帰着する方法を活用し,その有用性を示す.具体的には,部品の安全性までの帰着にとどめることで安全性証明中の議論が容易となる.さらに,部品の安全性を経由することで,計算量的仮定への帰着も示すことが可能であるため,従来の証明と同様に計算量的安全性を示すことができる.さらに,形式検証ツールを活用することで,人為的なミスを防止し,信頼性の高い安全性証明を与える方法を検討する.残念ながら,計算量的安全性を検証する形式検証ツールは発展途上の段階であり,現状の形式検証ツールでは,所望の性質を検証できないことも多い.そこで,形式検証ツールのみでは所望の安全性を検証できない場合に対応するため,人手の証明と形式検証を組み合わせることで安全性証明を与える方法を提案した.具体的には,1. 非同期耐性を備えたRFID システムの提案とその安全性証明への形式検証の活用(4 章)2. 内部者不正に体制を備えた追跡不可能電子現金システムの提案とその安全性証明(5 章)3. ハッシュ関数からの内部状態の漏えいを考慮した攻撃モデルでの形式検証(6 章)について検討した.各概要は下記のとおりである.RFID システムでは,RFID タグの低コスト化のため,利用できるセキュリティ技術に強い制約がある.本論文では,そのような制約の下であっても,非同期耐性とForward-security を併せ持つRFID システムを提案した.そして,RFID システムの攻撃モデルを構築し,形式検証による安全性証明を検討した.残念ながら,用いた形式検証ツールの制約により,所望の安全性を直接検証することはできなかった.そこで,提案方式を単純化し,単純化した攻撃モデルを構築して,形式検証を行い,単純化方式の安全性を証明した.そして,単純化方式の安全性の下で,提案方式が所望の安全性を満たすことを人手により証明した.安全性証明の一部に形式検証を活用することで,信頼性の高い安全性証明を与えることができたと. 従来の追跡不可能電子現金システムでは,発行機関の内部者の不正は考慮されていなかった.また,その安全性解析も非形式的な議論にとどまっている文献も多い状況であった.[HKOK06] は,発行機関の権限を複数に分散することで内部者による不正の被害を軽減した方式を提案し,さらに,厳密な安全性証明を与えた初めての論文であった.本論文では,[HKOK06] で与えられた攻撃モデルでは見落とされていた強力な結託攻撃が存在することを指摘し,そのような攻撃をも包含する攻撃モデルを与えた.さらに,その攻撃モデルの下で安全性が証明できる方式を提案した.この安全性証明は,人手のみで与えているが,システムを構成する部品であるAbe のブラインド署名の偽造困難性に帰着することで,安全性証明中の議論を平易にし,人為的な誤りを抑止したという特徴を持つ. ハッシュ関数からの内部状態の漏えいを考慮した攻撃モデルは,近年の攻撃技術の発展に伴い,重要性を増している.本研究では,既存の3 つの漏えいモデルへの形式検証の適用を検討した.検討の結果,形式検証ツールの制約により,3 つのモデルを取り扱うことはできないことが分かった.しかし,うち2 つのモデルについては,それらのモデルと計算量的に等価なモデルを構築し,それらのモデルの下でのFDH 署名の安全性を形式検証ツールで検証することで,新たに構築した2 つのモデルが機能することを確認した.残念ながら,残された1 つのモデルについては,形式検証手法を根本的に見直さなければ適用できないと考えている.これは,情報漏えいを考慮したモデルを形式検証で取り扱ううえで,有用な事例である. 4 章と5 章では,提案方式よりもシンプルな方式の安全性に帰着することで,提案方式の安全性を証明している.また,6 章では,既存の漏洩モデルを,形式検証が適用可能なモデルに帰着することで,既存モデルでの安全性を形式検証した.このように,複雑な攻撃モデル・暗号システムであっても,適切なモデルを介することで既存の証明結果や形式検証を利用可能とし,証明中の議論を平易にする方法を与えたこと,安全性証明技法としての本研究の貢献である.

2アクセス

各種コード

  • NII論文ID(NAID)
    500000560220
  • NII著者ID(NRID)
    • 8000000562427
  • 本文言語コード
    • jpn
  • NDL書誌ID
    • 023851871
  • データ提供元
    • 機関リポジトリ
    • NDL-OPAC
ページトップへ