| 講演名 | 2004-08-02 状態マシンモデルに基づいたセキュリテイプロトコルの仕様化 板橋 吾一, 高橋 薫, 加藤 靖, 菅沼 拓夫, 白鳥 則郎, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | セキュリティプロトコルの形式的検証を実現するためにspi計算などの仕様化手法が提案されている.本研究ではspi計算よりも実装に近い状態マシンモデルによるセキュリティプロトコルの仕様化手法を提案する.提案手法において,セキュリティプロトコルは状態マシンの集まりとしてモデル化され,各状態マシンはチャネルを介して暗号化されたメッセージの通信を行う.我々の手法はセキュリティプロトコルでしばしば使われるタイムスタンプの表現も可能であり,これらの特徴を実際のセキュリティプロトコルに適用することでその有用性を示す. |
| 抄録(英) | Formal methods such as the spi calculus have been proposed in order to validate security protocols. In this paper, we propose a specification method that is closer to implementation than the spi calculus. A security protocol is modeled as a collection of state machines, which exchange encrypted messages via channels. Our method can express a timestamp that is often used in security protocols. These features are demonstrated by applying to real security protocols. |
| キーワード(和) | 状態マシンモデル / セキュリティプロトコル / 暗号 |
| キーワード(英) | State machine model / Security protocol / cryptography |
| 資料番号 | SS2004-12 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2004/7/26(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 状態マシンモデルに基づいたセキュリテイプロトコルの仕様化 |
| サブタイトル（和） | |
| タイトル（英） | Specification of a Security Protocol based on a State Machine Model |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 状態マシンモデル / State machine model |
| キーワード(2)（和/英） | セキュリティプロトコル / Security protocol |
| キーワード(3)（和/英） | 暗号 / cryptography |
| 第 1 著者 氏名（和/英） | 板橋 吾一 / Goichi ITABASHI |
| 第 1 著者 所属（和/英） | 東北大学大学院情報科学研究科,株式会社サイエンティア Graduate School of Information Sciences Tohoku University, Scientia Corporation |
| 第 2 著者 氏名（和/英） | 高橋 薫 / Kaoru TAKAHASHI |
| 第 2 著者 所属（和/英） | 仙台電波工業高等専門学校 Sendai National College of Technology |
| 第 3 著者 氏名（和/英） | 加藤 靖 / Yasushi KATO |
| 第 3 著者 所属（和/英） | 仙台電波工業高等専門学校 Sendai National College of Technology |
| 第 4 著者 氏名（和/英） | 菅沼 拓夫 / Takuo SUGANUMA |
| 第 4 著者 所属（和/英） | 東北大学電気通信研究所 Research Institute of Electrical Communication Tohoku University |
| 第 5 著者 氏名（和/英） | 白鳥 則郎 / Norio SHIRATORI |
| 第 5 著者 所属（和/英） | 東北大学電気通信研究所 Research Institute of Electrical Communication Tohoku University |
| 発表年月日 | 2004-08-02 |
| 資料番号 | SS2004-12 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 242 |
| ページ範囲 | pp.- |
| ページ数 | 5 |
| 発行日 | |