| Item type |
Symposium(1) |
| 公開日 |
2024-10-15 |
| タイトル |
|
|
言語 |
ja |
|
タイトル |
ProVerifを用いたマークルハッシュ木の形式化 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Formalization of Merkle Hash Tree in ProVerif |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
マークルハッシュ木, 形式検証, ProVerif, 再帰処理 |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
| 著者所属 |
|
|
|
長崎大学 |
| 著者所属 |
|
|
|
長崎大学 |
| 著者所属 |
|
|
|
長崎大学 |
| 著者所属 |
|
|
|
NTT社会情報研究所 |
| 著者所属 |
|
|
|
NTT社会情報研究所 |
| 著者所属 |
|
|
|
NTT社会情報研究所 |
| 著者所属(英) |
|
|
|
en |
|
|
Nagasaki University |
| 著者所属(英) |
|
|
|
en |
|
|
Nagasaki University |
| 著者所属(英) |
|
|
|
en |
|
|
Nagasaki University |
| 著者所属(英) |
|
|
|
en |
|
|
NTT Social Informatics Laboratories |
| 著者所属(英) |
|
|
|
en |
|
|
NTT Social Informatics Laboratories |
| 著者所属(英) |
|
|
|
en |
|
|
NTT Social Informatics Laboratories |
| 著者名 |
江島, 奨悟
木内, 柊汰
荒井, 研一
奥田, 哲矢
中林, 美郷
山村, 和輝
|
| 著者名(英) |
Shogo, Eshima
Shuta, Kiuchi
Kenichi, Arai
Tetsuya, Okuda
Misato, Nakabayashi
Kazuki, Yamamura
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
ProVerifは，Blanchetらが開発した形式モデル（Dolev-Yaoモデル）での暗号プロトコルの自動検証ツールであり，暗号プロトコルに要求される秘匿や認証などの安全性要件を自動で検証することができる．一方，マークルハッシュ木は，データの整合性とセキュリティを確保するためのデータ構造であり，データの改ざん防止が重要な場面で広く活用される．ProVerifでは，木構造をサポートしていないため，マークルハッシュ木を用いるプロトコルを検証する際には木構造と木構造に対する操作をユーザ定義で形式化する必要がある．著者らは，SCIS2018において，ProVerifを用いてCT (Certificate Transparency) を形式化するために，CTにおけるマークルハッシュ木を形式化する方法を提案した．本稿では，ProVerifを用いてマークルハッシュ木の構造および検証機能を表現する新たな手法を提案する． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
ProVerif is an automatic verification tool for cryptographic protocols in the formal model (so called Dolev-Yao model) developed by Blanchet et al. It can automatically verify security requirements such as secrecy and authentication required by cryptographic protocols. On the other hand, the Merkle hash tree is a data structure for ensuring data consistency and security, and is widely used in situations where tampering prevention of data is important. However, ProVerif does not support tree structures. When verifying protocols using Merkle hash trees, it is necessary to formalize the tree structure and operations on the tree structure by user definition. The authors proposed a method to formalize the Merkle hash tree in CT (Certificate Transparency) for ProVerif at SCIS2018. In this paper, we propose a new method to express the structure and verification function of the Merkle hash tree for ProVerif. |
| 書誌情報 |
コンピュータセキュリティシンポジウム2024論文集
p. 1417-1424,
発行日 2024-10-15
|
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-CSS2024189.pdf (379.3 kB)
