FlexTokenプロトコルの形式手法を用いた安全性検証

• Item type: SIG Technical Reports(1)
• 公開日: 2023-07-17
• タイトル: FlexTokenプロトコルの形式手法を用いた安全性検証
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: CSEC
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学
• 著者所属: NTT社会情報研究所
• 著者所属: NTT社会情報研究所
• 著者名: 埜口, 裕矢; 中林, 美郷; 奥田, 哲矢
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: FlexToken は電子権利の移送時の原本性保証を目的としたプロトコルである．電子権利を権利の内容や条件を定義する権利定義と，原本性を保証するトークンに分離した状態で扱うことで，権利を扱う IC カードなどのデバイスの記憶容量や入出力性能に制限があっても様々な内容の電子権利を扱うことができる．本論文では，近年の多様で進歩したデバイス環境を十分に活用するため，FlexToken プロトコルの安全性についての再検討を行う．近年のデバイス環境として，トークンの移送をスマートフォンなどに搭載されたセキュアなハードウェア上で，トークン以外の権利定義や信任情報などのデータの移送を左記のハードウェアを搭載したスマートフォンなどの端末上で行う想定とする．また，正常にプロトコル仕様に従うデバイスのみでなく，ネットワーク上で改ざんなどを行う能動的な攻撃者のデバイスを想定する．左記の前提で，改竄防止，偽造防止，複製防止，公平性の確保について，形式検証ツール ProVerif を用いて検証を行った．その結果，それぞれの安全性を満たしていることを確認した．これまで形式的に検証されていなかった FlexToken の安全性について，各安全性要件を満たすことを形式的に明らかにした．加えて，権利定義の改竄防止や信任情報の偽造防止に関する工夫点などの新たな知見を発見した．これら検証結果の考察および FlexToken プロトコルの利用方法に関する工夫点について述べる．
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11235941
• 書誌情報: 研究報告コンピュータセキュリティ（CSEC）; 巻 2023-CSEC-102, 号 8, p. 1-8, 発行日 2023-07-17
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8655
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会