| 講演名 | 2004-12-17 イベント順序証明システムの正当性の形式的証明 小川 瑞史, 堀田 英一, 小野 諭, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では,NTTで開発した単一攻撃点のないイベント順序証明システムのモデルの基本的な性質の証明についてのべる.このモデルはインクリメンタルなMerkle木の構成に基づくものであり,その(1)完全化および(2)インクリメンタルなサニティチェックの正当性を示す.証明は主として定理証明系MONAを用いて構成しており,特に(2)インクリメンタルなサニティチェックの正当性については本稿で初めて証明を与えた. |
| 抄録(英) | This paper proves two basic properties of the model of the single attack point-free event ordering system, developed by NTT. This model is based on an incremental construction of a Merkle tree, and we show correctness of (1) completion and (2) incremental sanity check. They are mainly proved under assistance of theorem prover MONA ; especially, this paper gives the first proof of correctness of incremental sanity check. |
| キーワード(和) | 時刻認証 / 定理証明系 / イベント順序証明システム |
| キーワード(英) | Temporal authentication / theorem prover / event-ordering system |
| 資料番号 | ISEC2004-105 |
| 発行日 |
| 研究会情報 | |
| 研究会 | ISEC |
|---|---|
| 開催期間 | 2004/12/10(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Information Security (ISEC) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | イベント順序証明システムの正当性の形式的証明 |
| サブタイトル（和） | |
| タイトル（英） | Formal proof of correctness of scalable event-ordering system |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 時刻認証 / Temporal authentication |
| キーワード(2)（和/英） | 定理証明系 / theorem prover |
| キーワード(3)（和/英） | イベント順序証明システム / event-ordering system |
| 第 1 著者 氏名（和/英） | 小川 瑞史 / Mizuhito OGAWA |
| 第 1 著者 所属（和/英） | 北陸先端科学技術大学院大学 Japan Advanced Institute of Science and Technology |
| 第 2 著者 氏名（和/英） | 堀田 英一 / Eiichi HORITA |
| 第 2 著者 所属（和/英） | NTT情報流通プラットフォーム研究所 NTT Information Sharing Platform Laboratories |
| 第 3 著者 氏名（和/英） | 小野 諭 / Satoshi ONO |
| 第 3 著者 所属（和/英） | NTT情報流通プラットフォーム研究所 NTT Information Sharing Platform Laboratories |
| 発表年月日 | 2004-12-17 |
| 資料番号 | ISEC2004-105 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 527 |
| ページ範囲 | pp.- |
| ページ数 | 10 |
| 発行日 | |