| Item type |
Symposium(1) |
| 公開日 |
2024-10-15 |
| タイトル |
|
|
言語 |
ja |
|
タイトル |
スマートフォン環境を想定したOptimistic Fair Exchangeプロトコルの形式検証 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Formal Verification of Optimistic Fair Exchange Protocol for Smartphone Environment |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
フォーマルメソッド, ProVerif, Optimistic Fair Exchange（OFE），SmartOFE |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
| 著者所属 |
|
|
|
長崎大学 |
| 著者所属 |
|
|
|
長崎大学 |
| 著者所属 |
|
|
|
長崎大学 |
| 著者所属 |
|
|
|
NTT社会情報研究所 |
| 著者所属 |
|
|
|
NTT社会情報研究所 |
| 著者所属(英) |
|
|
|
en |
|
|
Nagasaki University |
| 著者所属(英) |
|
|
|
en |
|
|
Nagasaki University |
| 著者所属(英) |
|
|
|
en |
|
|
Nagasaki University |
| 著者所属(英) |
|
|
|
en |
|
|
NTT Social Informatics Laboratories |
| 著者所属(英) |
|
|
|
en |
|
|
NTT Social Informatics Laboratories |
| 著者名 |
木内, 柊汰
江島, 奨悟
荒井, 研一
中林, 美郷
奥田, 哲矢
|
| 著者名(英) |
Shuta, Kiuchi
Shogo, Eshima
Kenichi, Arai
Misato, Nakabayashi
Tetsuya, Okuda
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
ProVerifは，Blanchetらが開発した形式モデルの一つであるDolev-Yaoモデルでの暗号プロトコルの安全性検証ツールであり，秘匿や強秘匿, 認証などの要件を自動で検証することができる．一方，複数のパーティ間で公平に価値を交換するために，Fair Exchangeプロトコルが提案されている．Fair Exchangeプロトコルの中でも公平性を保つために必要な信頼のおける第三者（TTP:Trustes Third Party）がプロトコルの正常時は関与せず，TTPとのやり取りがResolveおよびAbortの要求時のみである災害時やネットワーク障害時を想定してTTPとのやり取りを最小限にしたものをOptimistic Fair Exchange（OFE）プロトコルと呼ぶ．本稿では，DICOMO2024においてのOFEプロトコルのバリエーションとして提案された，スマートフォン上で多様な価値を公平かつプライバシを考慮した形で交換するためのOFEプロトコル（SmartOFEプロトコル）について，ProVerifを用いて形式化，及び，安全性検証を行う． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
ProVerif is a security verification tool for cryptographic protocols in the Dolev-Yao model, developed by Blanchet et al. It can automatically verify requirements such as secrecy, strong secrecy, and authentication. On the other hand, Fair Exchange protocols have been proposed to fairly exchange values between multiple parties. Among Fair Exchange protocols, those that minimize interactions with a trusted third party (TTP) during normal protocol operations and only involve the TTP during disaster or network failure scenarios, such as when requesting Resolve or Abort, are called Optimistic Fair Exchange (OFE) protocols. This paper formalizes and verifies the security of an OFE protocol (SmartOFE protocol) proposed at DICOMO2024, which allows for the fair and privacy-conscious exchange of various values on smartphones using ProVerif. |
| 書誌情報 |
コンピュータセキュリティシンポジウム2024論文集
p. 1425-1432,
発行日 2024-10-15
|
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-CSS2024190.pdf (442.8 kB)
