@techreport{oai:ipsj.ixsq.nii.ac.jp:00222915,
 author = {奥田, 哲矢 and 荒井, 研一 and 齋藤, 恆和 and 千田, 浩司 and 中林, 美郷 and 山村, 和輝 and 宮澤, 俊之 and 阿部, 正幸},
 issue = {24},
 month = {Dec},
 note = {本研究では，transferable electronic cash と呼ばれる，利用者の間でオフラインで流通可能な電子現金プロトコルの安全性検証の手法として形式検証を採用した手法を考察する．近年，中央銀行デジタル通貨への期待が集まる中で，口座型電子現金方式とトークン型電子現金方式が注目されている．特にトークン型電子現金方式は，災害時や通信障害時のオフライン利用が可能となり得る点がメリットとされる．本論文では，トークン型電子現金方式の安全性要件として，代表的な偽造不可能性／二重使用時追跡可能性／免責性／仮名性／追跡不可能性／結合不可能性に拡充を行った上で，これらを代表的な形式検証ツールである ProVerif で記述する場合の実装方針や課題について考察した．特に今回の初期検討においては，通貨の発行／引出／支払という各プロトコルフェーズにおいて，偽造不可能性／二重使用時追跡可能性の検証から着手した．その結果，今回対象としたオフライン型のトークン型電子現金プロトコルが，偽造不可能性を有すること，および，二重使用時追跡可能性を一義的には有しないことを，検証結果より再現するとともに，後者については追加の対応策の方針を論じた．さらに，実効性は高くないもののロンダリングに類する新しい攻撃ベクトルを発見したため，対応策を実装して，検証結果が安全となることを確かめた．},
 title = {トークン型電子現金方式の形式検証手法に関する初期検討},
 year = {2022}
}