WEKO3
アイテム
SPINを用いたセキュリティプロトコルの安全性自動検証
http://hdl.handle.net/10076/12941
http://hdl.handle.net/10076/129414ae0a27e-e782-4626-99ba-dd0450aba1ae
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
2011M261.pdf (13.2 MB)
|
|
| Item type | 学位論文 / Thesis or Dissertation(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2013-06-11 | |||||||
| タイトル | ||||||||
| タイトル | SPINを用いたセキュリティプロトコルの安全性自動検証 | |||||||
| 言語 | ja | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_46ec | |||||||
| 資源タイプ | thesis | |||||||
| 著者 |
松田, 有司
× 松田, 有司
|
|||||||
| 抄録 | ||||||||
| 内容記述タイプ | Abstract | |||||||
| 内容記述 | セキュリティプロトコルは,悪意ある第二社（以降,攻撃者と呼ぶ）からユーザとサーバ間の通信路を,認証と時間や労力がかかり,見落としも生じる.一方,形式手法を用いた安全性検証では自動で正確な検証ができる.その中でもモデル検査法は,セキュリティプロトコルの安全性を専門家でなくても検証でき,脆弱性の原因を確認できる.本研究の目的は,モデル検査法で既存手法よりも多くのセキュリティプロトコルの安全J性を,現実時間で自動検証できる手法の提案である.モデル検査法を用いたセキュリティプロトコルの安全性自動検証には,Khan(2005)らの手法がある.Khanらは情報漏洩の有無や,セキュリティプロトコル上で扱える情報等を定義し,モデル検査器SPINを用いて特定のセキュリティプロトコルの脆弱性の発見に成功した.しかし,本研究によりKhanらの手法の定義の2つの問題点が明らかになる.1つ目は情報漏洩の定義が不適切であり,情報漏洩の誤検出や検出漏れが生じる問題である.2つ目はセキュリティプロトコル上で扱える情報の定義が不十分であり,僅かなセキュリティプロトコルの安全性しか検証できない問題である.そのため,本研究では情報漏洩の定義を見直し,セキュリティプロトコルの役割に応じて指定した機密情報が攻撃者に取得された時のみ情報漏洩であると再定義する.また,セキュリティプロトコル上で複数の構成要素からなる複雑な情報を扱うための解析・合成規則の定義を見直し,複雑な鍵情報やhash関数などの特別な関数から作成された情報もセキュリティプロトコル上で扱えるように再定義する.しかし,これらの新たな定義により,解析・合成規則で攻撃者の所持情報の中から組み合わせて作成できる機密情報の候補数が膨大になる.この候補数が膨大になる問題に対し,本研究では逆向き合成規貝Jを用いた新手法を提案する.この手法は,攻撃者の所持情報から解析・合成規則で機密情報を作成できるか判定するのではなく,機密情報から逆向き合成規則で機密情報を作成できる情報の組み合わせ候補を作成し,いずれかの組み合わせを攻撃者が所持しているか判定する.攻撃者の所持情報の組み合わせの数より,機密情報を作成できる情報の組み合わせの数が圧倒的に少ないため,この手法により計算時間とメモリ消費量を大幅に抑制できる. | |||||||
| 内容記述 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 三重大学大学院工学研究科博士前期課程情報工学専攻 | |||||||
| 内容記述 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 1, 40 | |||||||
| 書誌情報 |
発行日 2011-01-01 |
|||||||
| フォーマット | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | application/pdf | |||||||
| 著者版フラグ | ||||||||
| 出版タイプ | VoR | |||||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||||
| 出版者 | ||||||||
| 出版者 | 三重大学 | |||||||
| 修士論文指導教員 | ||||||||
| 寄与者識別子Scheme | WEKO | |||||||
| 寄与者識別子 | 23023 | |||||||
| 姓名 | 山田, 俊行 | |||||||
| 言語 | ja | |||||||
| 資源タイプ（三重大） | ||||||||
| 値 | Master's Thesis / 修士論文 | |||||||
