トークン型電子現金方式の形式検証手法に関する初期検討

• Item type: SIG Technical Reports(1)
• 公開日: 2022-12-15
• タイトル: トークン型電子現金方式の形式検証手法に関する初期検討
• タイトル / 言語: en
• タイトル: Preliminary study on the formal verification of transferable electronic cash system
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: NTT社会情報研究所
• 著者所属: 長崎大学
• 著者所属: NTT社会情報研究所
• 著者所属: 群馬大学
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者名: 奥田, 哲矢; 荒井, 研一; 齋藤, 恆和; 千田, 浩司; 中林, 美郷; 山村, 和輝; 宮澤, 俊之; 阿部, 正幸
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本研究では，transferable electronic cash と呼ばれる，利用者の間でオフラインで流通可能な電子現金プロトコルの安全性検証の手法として形式検証を採用した手法を考察する．近年，中央銀行デジタル通貨への期待が集まる中で，口座型電子現金方式とトークン型電子現金方式が注目されている．特にトークン型電子現金方式は，災害時や通信障害時のオフライン利用が可能となり得る点がメリットとされる．本論文では，トークン型電子現金方式の安全性要件として，代表的な偽造不可能性／二重使用時追跡可能性／免責性／仮名性／追跡不可能性／結合不可能性に拡充を行った上で，これらを代表的な形式検証ツールである ProVerif で記述する場合の実装方針や課題について考察した．特に今回の初期検討においては，通貨の発行／引出／支払という各プロトコルフェーズにおいて，偽造不可能性／二重使用時追跡可能性の検証から着手した．その結果，今回対象としたオフライン型のトークン型電子現金プロトコルが，偽造不可能性を有すること，および，二重使用時追跡可能性を一義的には有しないことを，検証結果より再現するとともに，後者については追加の対応策の方針を論じた．さらに，実効性は高くないもののロンダリングに類する新しい攻撃ベクトルを発見したため，対応策を実装して，検証結果が安全となることを確かめた．
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11238429
• 書誌情報: 研究報告電子化知的財産・社会基盤（EIP）; 巻 2022-EIP-98, 号 24, p. 1-8, 発行日 2022-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8647
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会