トークン型電子現金方式の二重使用検知およびプライバシーに関する形式検証の考察

• Item type: SIG Technical Reports(1)
• 公開日: 2023-02-27
• タイトル: トークン型電子現金方式の二重使用検知およびプライバシーに関する形式検証の考察
• タイトル / 言語: en
• タイトル: Formal verification of double spend identification and privacy for transferable electronic cash system
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 準同型暗号・暗号応用
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: NTT社会情報研究所
• 著者所属: 長崎大学
• 著者所属: NTT社会情報研究所
• 著者所属: 群馬大学
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者名: 奥田, 哲矢; 荒井, 研一; 齋藤, 恆和; 千田, 浩司; 中林, 美郷; 山村, 和輝; 宮澤, 俊之; 阿部, 正幸
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本研究は，先行研究「トークン型電子現金方式の形式検証手法に関する初期検討」（第 99 回 CSEC 研究会）の続編である．近年，中央銀行デジタル通貨への期待が集まる中で，トークン型電子現金方式は，災害時や通信障害時のオフライン利用が可能となり得る点で注目されている．ただし，既知の事実としてトークン型電子現金方式では通貨が発行銀行に還収されるまで二重使用の検知が（一義的には）出来ないことが知られている．本論文では，まず，今回対象プロトコルについて，二重使用対策の仕組みを組み込む対象とすべきプロトコルのフェーズを考察するため，先行研究で定式化した通貨発行／引出／支払フェーズに加えて，両替／与信などの一時的なオンライン化のフェーズや，市中銀行への預入および発行銀行への還収のフェーズについて定式化を行った．さらに，先行研究で述べた通貨発行／引出／支払フェーズを含む，すべてのフェーズについて代表的な形式検証ツールである ProVerif による形式的な実装を行い，到達可能性 (reachability) を確認した．その上で，クライアント端末上のセキュアハードウェアによる二重使用対策について ProVerif による形式的な実装を行い，端末上の支払処理が正常終了した時に端末上では二重使用が発生しないことを確認した．さらに，二重使用検知などのコンプライアンスを重視した際にトレードオフとなるプライバシー要件として，仮名性（特定／追跡不可能性）について，ProVerif で観測等価性を表現する choice 文で記述する場合の方針について考察を行い，今回対象プロトコルにおける仮名性の検証結果が True（仮名／識別不可能）となることを確認した．
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11235941
• 書誌情報: 研究報告コンピュータセキュリティ（CSEC）; 巻 2023-CSEC-100, 号 66, p. 1-8, 発行日 2023-02-27
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8655
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会