| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2025-01-12 10:25 グラフデータベースを用いたセキュリティプロトコル向け形式検証の提案 ○毛利寿志・米持一樹・三澤 学（三菱電機）  MSS2024-43 SS2024-22 |
|
| 抄録 | （和） | システムの安全性やセキュリティを保証する仕組みの一つとして，形式手法を用いた検証がある．既存のモデル検査器は専用言語を習得する必要があり，導入が比較的困難という課題があった．さらに，対象システムが複雑になると状態爆発を起こすという課題もあった．本研究では，一般に広く利用されているグラフデータベースを用い，状態数を抑えたセキュリティプロトコルに対するモデル検査手法を提案する．また，脆弱性が発見されているNSPK プロトコルを対象として提案手法を用いて検証し，既知の脆弱性が検出できることを示す． |
| （英） | A model checking method using graph database software is investigated. A technique to ensure functional safety and security of systems is formal verification. An example of systems is a security protocol. Using existing verification tools is relatively difficult because it requires acquisition of specialized languages. This paper proposes a model checking method for security protocols using graph databases, which are widely used. By using the proposed method to verify the NSPK protocol, which has known vulnerabilities, it is shown that the proposed method can detect the known attacks. |
|
| キーワード | （和） | 形式検証 / モデル検査 / グラフデータベース / セキュリティプロトコル / 認証 / / / |
| （英） | formal verification / model checking / graph database / security protocol / authentication / / / | |
| 文献情報 | 信学技報, vol. 124, no. 326, SS2024-22, pp. 7-12, 2025年1月. | |
| 資料番号 | SS2024-22 | |
| 発行日 | 2025-01-05 (MSS, SS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2024-43 SS2024-22 |
|
| 研究会情報 | |
| 研究会 | MSS SS |
| 開催期間 | 2025-01-12 - 2025-01-13 |
| 開催地（和） | 鹿児島大学郡元キャンパス |
| 開催地（英） | |
| テーマ（和） | システム数理と応用，ソフトウェアサイエンスおよび一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2025-01-MSS-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | グラフデータベースを用いたセキュリティプロトコル向け形式検証の提案 |
| サブタイトル（和） | |
| タイトル（英） | Proposal for Security Protocol Verification using Graph Database |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 形式検証 / formal verification |
| キーワード(2)（和/英） | モデル検査 / model checking |
| キーワード(3)（和/英） | グラフデータベース / graph database |
| キーワード(4)（和/英） | セキュリティプロトコル / security protocol |
| キーワード(5)（和/英） | 認証 / authentication |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 毛利 寿志 / Hisashi Mori / モウリ ヒサシ |
| 第1著者 所属（和/英） | 三菱電機株式会社 (略称： 三菱電機) Mitsubishi Electric Corporation (略称： Mitsubishi Electric) |
| 第2著者 氏名（和/英/ヨミ） | 米持 一樹 / Kazuki Yonemochi / ヨネモチ カズキ |
| 第2著者 所属（和/英） | 三菱電機株式会社 (略称： 三菱電機) Mitsubishi Electric Corporation (略称： Mitsubishi Electric) |
| 第3著者 氏名（和/英/ヨミ） | 三澤 学 / Manabu Misawa / ミサワ マナブ |
| 第3著者 所属（和/英） | 三菱電機株式会社 (略称： 三菱電機) Mitsubishi Electric Corporation (略称： Mitsubishi Electric) |
| 講演者 | 第1著者 |
| 発表日時 | 2025-01-12 10:25:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | MSS2024-43, SS2024-22 |
| 巻番号（vol） | vol.124 |
| 号番号（no） | no.325(MSS), no.326(SS) |
| ページ範囲 | pp.7-12 |
| ページ数 | 6 |
| 発行日 | 2025-01-05 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]