@techreport{oai:ipsj.ixsq.nii.ac.jp:00224742,
 author = {奥田, 哲矢 and 荒井, 研一 and 齋藤, 恆和 and 千田, 浩司 and 中林, 美郷 and 山村, 和輝 and 宮澤, 俊之 and 阿部, 正幸},
 issue = {66},
 month = {Feb},
 note = {本研究は，先行研究「トークン型電子現金方式の形式検証手法に関する初期検討」（第 99 回 CSEC 研究会）の続編である．近年，中央銀行デジタル通貨への期待が集まる中で，トークン型電子現金方式は，災害時や通信障害時のオフライン利用が可能となり得る点で注目されている．ただし，既知の事実としてトークン型電子現金方式では通貨が発行銀行に還収されるまで二重使用の検知が（一義的には）出来ないことが知られている．本論文では，まず，今回対象プロトコルについて，二重使用対策の仕組みを組み込む対象とすべきプロトコルのフェーズを考察するため，先行研究で定式化した通貨発行／引出／支払フェーズに加えて，両替／与信などの一時的なオンライン化のフェーズや，市中銀行への預入および発行銀行への還収のフェーズについて定式化を行った．さらに，先行研究で述べた通貨発行／引出／支払フェーズを含む，すべてのフェーズについて代表的な形式検証ツールである ProVerif による形式的な実装を行い，到達可能性 (reachability) を確認した．その上で，クライアント端末上のセキュアハードウェアによる二重使用対策について ProVerif による形式的な実装を行い，端末上の支払処理が正常終了した時に端末上では二重使用が発生しないことを確認した．さらに，二重使用検知などのコンプライアンスを重視した際にトレードオフとなるプライバシー要件として，仮名性（特定／追跡不可能性）について，ProVerif で観測等価性を表現する choice 文で記述する場合の方針について考察を行い，今回対象プロトコルにおける仮名性の検証結果が True（仮名／識別不可能）となることを確認した．},
 title = {トークン型電子現金方式の二重使用検知およびプライバシーに関する形式検証の考察},
 year = {2023}
}