緒言

暗号プロトコルは，現実の情報システムで広く使われており，システムの複雑な安全性要件 を満たすための重要な構成要素となっている．システムを構築する際には，そのシステムが所

望の安全性を満たすことを検証せねばならない．形式上検証の理論とツールを上記の目的に利 用するために，過去30年にわたって多くの試みがなされてきた．そのような理論とツールの 活用を促進し，信頼性の高い情報システム提供するために，ISO/IEC 29128において，検証の 枠組みに関する国際標準化が行われている．ISO/IEC 29128は，情報システムの検証の信頼性 の基準を提供するもので，4レベルの信頼性の分類を持ち，安全性が形式的に記述され，それ を形式的に検証した情報システムは，高レベルの信頼性に分類される．これは，あくまでも検 証中に誤りが存在しうるかという観点でのレベルであり，高いレベルに分類されたとしても，

高い安全性を実現しているとは限らない．ISO/IEC 29128の標準化の過程で，計算量的安全性 を保証する検証ツールの使用と制約は，大きな課題とされた[70]．計算量的安全性を検証する ツールの開発は進められてはいるものの，現状では開発途上の段階であり，その能力には未知 の部分が多い．そのため，記号的安全性と計算量的安全性の観点でのレベル分けは，ISO/IEC

29128には導入されなかった．課題の解決には，現実の暗号プロトコルに対して，計算量的安

全性の検証ツールを適用した研究事例が不足している．

RFIDシステムとは，無線通信路を通じてRFIDタグに固有のIDを読み取り装置に伝える ことでサービスを提供するシステムの総称で，RFIDタグを商品に添付して商品の識別や管 理を行うなど，様々なサービスを実現できる．RFIDシステムの安全性を保証するためには，

RFIDタグと読み取り装置の間で，正しく認証を行う必要がある．ここでは，そのような認証 を行うプロトコルをRFID認証プロトコルと呼ぶ．商品の識別や管理にRFIDタグを活用する とき，RFIDタグは各商品に添付されるため，その価格を商品の価格に上乗せざるを得ない．

つまり，RFIDシステムを現実のサービスとして成立させるために，RFIDタグは非常に安価 に製造できることが重要である．そのために，RFIDタグの計算リソースやタグ内の秘密鍵の 保護技術に強い制限がある．

安全性の観点では，RFIDタグの用途と認証プロトコルの構成によって，様々な問題が生じ うることが指摘されている．例えば，先のRFIDタグによる商品の識別では，RFIDタグの出 力が固定値であったり，2つの通信が同じRFIDタグによってなされたものか否かを識別でき ると，RFIDタグの出力を盗聴することで，その商品の所有者を容易に追跡できる．そのため，

RFID認証プロトコルでは，通常の認証プロトコルとは異なり，プライバシーを保護する機能 が特に重視されている．また，有線ネットワーク環境と比べると，RFIDのような無線ネット ワーク環境では，攻撃者はman-in-the-middle攻撃や リプレイ攻撃を容易に実行できる．さら に，通信のエラーへの対策も考慮する必要がある．このように，RFID認証プロトコルでは，

通常の認証性のみではなく，用途に応じて様々な安全性が必要とされる．

既存の形式検証技術は，認証プロトコルの安全性検証の分野で，大きな成功を収めている．

例えば，ISO/IEC 9798で国際標準化されているエンティティ認証プロトコルを電子政府推奨

暗号[2]に登録する際に，それらの安全性検証に記号論的安全性を検証するツールScytherが 活用され，いくつかの安全性の欠陥が発見された[15]．過去に，RFIDプロトコルの安全性を 形式的に検証した研究があるが，それらは全て記号的安全性の検証にとどまっていた．

4.1.1 貢献

本章では，人手による検証と形式検証ツールを組み合わせた新しい検証法を，RFIDプロト コルに適用した事例を示す．検証対象のOMHSOプロトコル[77]は，OSKプロトコル[78]

に改良を施し，通信エラー対策を備えたものである．OSKプロトコルは，ハッシュ関数を利 用した認証を採用した方式で，公開鍵暗号を利用した認証と比較して，計算コストが非常に小 さいという利点がある．また，認証に用いる事前共有鍵を更新することで，強力なプライバ シーを実現している．さらに，OMHSOプロトコルは，読み取り装置側の処理を工夫すること で，OSKプロトコルが備えていなかった非同期耐性を実現した．非同期耐性とは，通信のエ ラーなどによりRFID認証プロトコルのあるセッションが途中終了したとしても，次回のセッ ションでは正常に実行できることを保証する性質である．現実の状況下では，通信のエラーは 日常的に生じるため，これに対する対策を施す必要がある．

受動的RFIDタグのように，その内部に電源を搭載せず外部からの提供される電波を電力に 変えて動作するタグを用いる場合，セッションが途中終了すると，読み取り装置とRFIDで共 有する内部状態の同期がずれ，以降のセッションでは認証に成功しなくなる恐れがある．その ため，我々は，受動的RFIDプロトコルを現実の状況で使用する場合，非同期耐性は必須の性 質であると考えている．

我々の主な貢献は，下記の2点である．

1. OSKプロトコル[78]を改良し，非同期耐性を備えた新しいRFID認証プロトコルを提

案した．

2. man-in-the-middle攻撃者と通信エラーを取り扱うことができる安全性モデルを形式的

に定義した．このモデルは，鍵交換プロトコルの安全性モデルと同じように，攻撃の成 功確率を厳密に見積もるのに適している．

3. 前述のモデルにおいて，OMHSOプロトコルが成りすまし不可能性とプライバシーを満 たすことを証明した．安全性の証明は，形式検証ツールの一種であるCryptoVerifを用 いた検証と，人手による証明が組み合わせることで行われている．

第3章で説明したように，CryptoVerifで，他のプロセスで定義された項を利用した処理は，

f ind文を利用して条件を満たす配列のインデックスを探索し，そのインデックスを用いて記

述せねばならなかった．OMHSOプロトコルでは，ハッシュ関数を連鎖的に用いた，ハッシュ 鎖による共有鍵の更新方法を採用している．つまり，あるプロセス1で用いる共有鍵は，他の プロセス2で定義される項である．よって，OMHSOプロトコルの記述には，f ind文を用い て，所望の共有鍵が生成されたプロセスのインデックスを特定しなければならない．しかし，

OMHSOプロトコルは，プライバシーを保護するために，他のプロセスで定義された項を推測

できない構成となっているため，f ind文を用いたとしても，所望の共有鍵のインデックスを特 定することができなかった．そのため，CryptoVerifを用いて所望の安全性を直接的に検証す ることができなかった．

そこで，OMHSOプロトコルから共有鍵の更新処理を省いた単純化OMHSOプロトコルを

構成し，その安全性要件を形式化し，それらの安全性をCryptoVerifを利用して検証した．単

純化OMHSOプロトコルは，非同期耐性を実現するための機構を備えているため，OSKプロ

トコルよりもサーバー側の処理が複雑である．そのため，単純化 OMHSOプロトコルを愚直 に形式化したとしても，CryptoVerifでは正しく検証できず，条件分岐をシンプルに記述する 工夫が必要であった．最終的に，人手の証明により，単純化OMHSO方式が単純化した安全 性を満たすならば，検証対象の方式は所望の安全性を満たすことを示した．

本章の結果は，RFIDの分野において，安全性要件を定義し，形式検証ツールを活用して計 算量的安全性を議論した，初めてのものである．また，今回の結果は，計算量的安全性の形式 検証の活用事例としても重要な意味を持つ．すなわち，OMHSOプロトコルのように，現実 の状況下での活用を想定したプロトコルに対しても，計算量的安全性の形式検証の活用が可能 で，信頼性の高い検証が実現できることを示した．

4.1.2 関連研究

現在では，プライバシーを保護する安全なRFIDプロトコルが数多く提案されており，文 献[1]にまとめられている．JuelsとWeisはRFID認証プロトコルのプライバシーを初めてモ デル化した[60]．VaudenayはRFIDタグの認証に求められるプライバシーの概念を分類した

[87]．PaiseとVaudenayは，プライバシーを保証した相互認証の安全性概念を分類した[82]．

HanckeとKuhnは，リプレイ 攻撃に対して耐性を持ち，distance-boundingプロトコルを使う タイプのRFID認証プロトコルを導入した[54]．このプロトコルは，多くのラウンドの通信を 必要とするため，OMHSOプロトコルは別の構成法を採用している．

通信を途中で妨害するなどし，あるセッションが正しく実行できなかったとしても，各セッ ションごとに共有鍵を更新することで，タグの追跡を防ぐ方式が提案されている[59]．Juels の方式では，タグはセッション開始時にハッシュ連鎖による共有鍵の更新を行い，サーバーは