{"id":224811,"updated":"2025-01-19T13:00:49.151018+00:00","links":{},"created":"2025-01-19T01:24:22.442168+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00224811","sets":["1164:2836:11158:11159"]},"path":["11159"],"owner":"44499","recid":"224811","title":["トークン型電子現金方式の二重使用検知およびプライバシーに関する形式検証の考察"],"pubdate":{"attribute_name":"公開日","attribute_value":"2023-02-27"},"_buckets":{"deposit":"e7697032-5aca-4158-99f6-d69ff8b0941d"},"_deposit":{"id":"224811","pid":{"type":"depid","value":"224811","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"トークン型電子現金方式の二重使用検知およびプライバシーに関する形式検証の考察","author_link":["593605","593611","593607","593606","593609","593610","593608","593604"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"トークン型電子現金方式の二重使用検知およびプライバシーに関する形式検証の考察"},{"subitem_title":"Formal verification of double spend identification and privacy for transferable electronic cash system","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"準同型暗号・暗号応用","subitem_subject_scheme":"Other"}]},"item_type_id":"4","publish_date":"2023-02-27","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"NTT社会情報研究所"},{"subitem_text_value":"長崎大学"},{"subitem_text_value":"NTT社会情報研究所"},{"subitem_text_value":"群馬大学"},{"subitem_text_value":"NTT社会情報研究所"},{"subitem_text_value":"NTT社会情報研究所"},{"subitem_text_value":"NTT社会情報研究所"},{"subitem_text_value":"NTT社会情報研究所"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/224811/files/IPSJ-DPS23194066.pdf","label":"IPSJ-DPS23194066.pdf"},"date":[{"dateType":"Available","dateValue":"2025-02-27"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-DPS23194066.pdf","filesize":[{"value":"301.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"34"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"c2952768-a519-4cf6-a49a-00b1efe44f1f","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2023 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"奥田, 哲矢"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"荒井, 研一"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"齋藤, 恆和"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"千田, 浩司"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"中林, 美郷"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"山村, 和輝"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"宮澤, 俊之"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"阿部, 正幸"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN10116224","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"2188-8906","subitem_source_identifier_type":"ISSN"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"本研究は，先行研究「トークン型電子現金方式の形式検証手法に関する初期検討」（第 99 回 CSEC 研究会）の続編である．近年，中央銀行デジタル通貨への期待が集まる中で，トークン型電子現金方式は，災害時や通信障害時のオフライン利用が可能となり得る点で注目されている．ただし，既知の事実としてトークン型電子現金方式では通貨が発行銀行に還収されるまで二重使用の検知が（一義的には）出来ないことが知られている．本論文では，まず，今回対象プロトコルについて，二重使用対策の仕組みを組み込む対象とすべきプロトコルのフェーズを考察するため，先行研究で定式化した通貨発行／引出／支払フェーズに加えて，両替／与信などの一時的なオンライン化のフェーズや，市中銀行への預入および発行銀行への還収のフェーズについて定式化を行った．さらに，先行研究で述べた通貨発行／引出／支払フェーズを含む，すべてのフェーズについて代表的な形式検証ツールである ProVerif による形式的な実装を行い，到達可能性 (reachability) を確認した．その上で，クライアント端末上のセキュアハードウェアによる二重使用対策について ProVerif による形式的な実装を行い，端末上の支払処理が正常終了した時に端末上では二重使用が発生しないことを確認した．さらに，二重使用検知などのコンプライアンスを重視した際にトレードオフとなるプライバシー要件として，仮名性（特定／追跡不可能性）について，ProVerif で観測等価性を表現する choice 文で記述する場合の方針について考察を行い，今回対象プロトコルにおける仮名性の検証結果が True（仮名／識別不可能）となることを確認した．","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"8","bibliographic_titles":[{"bibliographic_title":"研究報告マルチメディア通信と分散処理（DPS）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2023-02-27","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"66","bibliographicVolumeNumber":"2023-DPS-194"}]},"relation_version_is_last":true,"weko_creator_id":"44499"}}