@techreport{oai:ipsj.ixsq.nii.ac.jp:00227015,
 author = {埜口, 裕矢 and 中林, 美郷 and 奥田, 哲矢},
 issue = {8},
 month = {Jul},
 note = {FlexToken は電子権利の移送時の原本性保証を目的としたプロトコルである．電子権利を権利の内容や条件を定義する権利定義と，原本性を保証するトークンに分離した状態で扱うことで，権利を扱う IC カードなどのデバイスの記憶容量や入出力性能に制限があっても様々な内容の電子権利を扱うことができる．本論文では，近年の多様で進歩したデバイス環境を十分に活用するため，FlexToken プロトコルの安全性についての再検討を行う．近年のデバイス環境として，トークンの移送をスマートフォンなどに搭載されたセキュアなハードウェア上で，トークン以外の権利定義や信任情報などのデータの移送を左記のハードウェアを搭載したスマートフォンなどの端末上で行う想定とする．また，正常にプロトコル仕様に従うデバイスのみでなく，ネットワーク上で改ざんなどを行う能動的な攻撃者のデバイスを想定する．左記の前提で，改竄防止，偽造防止，複製防止，公平性の確保について，形式検証ツール ProVerif を用いて検証を行った．その結果，それぞれの安全性を満たしていることを確認した．これまで形式的に検証されていなかった FlexToken の安全性について，各安全性要件を満たすことを形式的に明らかにした．加えて，権利定義の改竄防止や信任情報の偽造防止に関する工夫点などの新たな知見を発見した．これら検証結果の考察および FlexToken プロトコルの利用方法に関する工夫点について述べる．},
 title = {FlexTokenプロトコルの形式手法を用いた安全性検証},
 year = {2023}
}