@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00240935,
 author = {江島, 奨悟 and 木内, 柊汰 and 荒井, 研一 and 奥田, 哲矢 and 中林, 美郷 and 山村, 和輝 and Shogo, Eshima and Shuta, Kiuchi and Kenichi, Arai and Tetsuya, Okuda and Misato, Nakabayashi and Kazuki, Yamamura},
 book = {コンピュータセキュリティシンポジウム2024論文集},
 month = {Oct},
 note = {ProVerifは，Blanchetらが開発した形式モデル（Dolev-Yaoモデル）での暗号プロトコルの自動検証ツールであり，暗号プロトコルに要求される秘匿や認証などの安全性要件を自動で検証することができる．一方，マークルハッシュ木は，データの整合性とセキュリティを確保するためのデータ構造であり，データの改ざん防止が重要な場面で広く活用される．ProVerifでは，木構造をサポートしていないため，マークルハッシュ木を用いるプロトコルを検証する際には木構造と木構造に対する操作をユーザ定義で形式化する必要がある．著者らは，SCIS2018において，ProVerifを用いてCT (Certificate Transparency) を形式化するために，CTにおけるマークルハッシュ木を形式化する方法を提案した．本稿では，ProVerifを用いてマークルハッシュ木の構造および検証機能を表現する新たな手法を提案する．, 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.},
 pages = {1417--1424},
 publisher = {情報処理学会},
 title = {ProVerifを用いたマークルハッシュ木の形式化},
 year = {2024}
}