| 講演抄録／キーワード |
| 講演名 |
2004-08-02 16:15
状態マシンモデルに基づいたセキュリティプロトコルの仕様化
○板橋吾一（東北大/サイエンティア）・高橋 薫・加藤 靖（仙台電波高専）・菅沼拓夫・白鳥則郎（東北大） |
| 抄録 |
（和） |
セキュリティプロトコルの形式的検証を実現するために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 / / / / / |
| 文献情報 |
信学技報, vol. 104, no. 242, SS2004-12, pp. 37-39, 2004年8月. |
| 資料番号 |
SS2004-12 |
| 発行日 |
2004-07-26 (SS) |
| ISSN |
Print edition: ISSN 0913-5685 |
| PDFダウンロード |
|