形式検証を活用した暗号システムの安全性証明技術 花谷 嘉一

形式検証を活用した暗号システムの安全性証明技術

花谷 嘉一

電気通信大学大学院情報理工学研究科

博士（工学）の学位申請論文

2012 年 3 月

形式検証を活用した暗号システムの安全性証明技術

論文審査委員会

主査： 太田 和夫 教授 

委員： 安藤 清  教授 

委員： 木田 雅成 教授 

委員： 吉浦 裕  教授 

委員： 﨑山 一男 准教授

著作権所有者 花谷嘉一 ２０１２

COPYRIGHT BY YOSHIKAZU HANATANI 2012

ALL RIGHTS ARE RESERVED

On Security Proof Technique for Cryptographic Systems Using Formal Verification

YOSHIKAZU HANATANI

In this thesis, we propose new three cryptographic protocols, and prove their com- putational security. For repressing mistakes in their security proofs and reducing their costs, we use a formal verification tool and devise the security proofs. In recent years, formal verification tools which verify computational security are de- veloped, however the capabilities of them are limited variously. A typical proof for the computational security is given by reducing an attack problem for a cryp- tographic protocol to a computational assumption. In this thesis, we reduce an attack problem for a cryptographic protocol to a computational security of a cryp- tographic primitive, and prove the computational security of the protocol. More- over, some part of several security proofs is proved by CryptoVerif which is a formal verification tool for the computational security, and the remaining part is proved manually. In short, we overcome a restriction of CryptoVerif by combin- ing manual proofs. In chapter 1, we show backgrounds, goals and contributions of this research. In chapter 2, we introduce techniques of the security proof. Es- pecially, we review two topics. First topic is a di ff erence of a symbolic security which is verified by typical formal verification tools and the computational se- curity. Second topic is a security proof by game hopping technique. By using the game hopping technique, we can tame complicated probability estimations.

In chapter 3, we introduce CryptoVerif. CryptoVerif semi-automatically converts

the game for a security proof by the game hopping. In chapter 4, we propose an

RFID authentication protocol with a desynchronization. The desynchronization

is important for passive RFID systems, however some RFID protocols e.g. OSK

protocol does not hold it. We define security requirements for RFID systems, and

show that the proposed protocol satisfies the security requirements. To overcome

a limitation of CryptoVerif, we consider a simplified protocol of the proposed

protocol, and prove its security using CryptoVerif. We then prove that the pro-

posed protocol is also secure if the simplified protocol is secure. In chapter 5,

we propose an untraceable electronic-cash system against strong insider attacks,

and define new security requirements. In order to simplify a security proof of our

e-cash system, we reduce a forgery problem of the e-cash to a forgery game for

Abe’s blind signature scheme. In chapter 6, we formalize random oracle models

with information leakage for CryptoVerif, and verify EUF-CMA security of FDH

signature in each random oracle model by CryptoVerif. Because of a limitation of

CryptoVerif, we cannot straightforwardly formalize existing random oracle mod-

els with information leakage i.e., LRO, TRO, and ERO. We cannot formalize

LRO, however we define computationally equivalent models for TRO and ERO

for CryptoVerif. Moreover, we succeed to prove the security of FDH signature

scheme in each model.

形式検証を活用した暗号システムの安全性証明技術 花谷 嘉一

暗号理論の黎明期には，暗号システムの安全性検証は設計者の勘と経験により 行われていた．そのため，設計者の想定外の攻撃により破られることがあるだ けでなく，第三者による暗号システムの安全性の再検証は困難という問題を抱 えていた．そのような背景から， 1980 年代に，安全性証明という技術が開発 された．安全性証明では，攻撃をモデル化し，そのモデルにおいて生じうる攻 撃に対して安全であることを数学的に証明する．モデルに属する全ての攻撃に 対して安全性が保証できるだけでなく，第三者により証明の正しさが再検証可 能であるという利点を持つ．

安全性証明は学術的にだけではなく，産業的にも重要である．特に，産業的 な立場からは，安全性証明中のミスの防止と負担の軽減が大きな課題となって いる．そこで，本研究では，安全性証明を備えた暗号システムの提案を行うだ けでなく，安全性証明の工夫と形式検証の活用によるミスの防止と負荷の軽減 を試みる．また，記号的安全性では，実用に供されているシステムとの隔たり が大きいため，より高い安全性を評価できる計算量的安全性の検証に焦点を当 てる．

通常の計算量的安全性の証明は，暗号システムへの攻撃問題を計算量的仮定 に帰着することで行われる．本論文では，人手による安全性証明の複雑さを緩 和するために，計算量的仮定まで帰着するのではなく，構成要素とする部品の 計算量的安全性に帰着する方法を活用し，その有用性を示す．具体的には，部 品の安全性までの帰着にとどめることで安全性証明中の議論が容易となる．さ らに，部品の安全性を経由することで，計算量的仮定への帰着も示すことが可 能であるため，従来の証明と同様に計算量的安全性を示すことができる．

さらに，形式検証ツールを活用することで，人為的なミスを防止し，信頼性

の高い安全性証明を与える方法を検討する．残念ながら，計算量的安全性を検 証する形式検証ツールは発展途上の段階であり，現状の形式検証ツールでは，

所望の性質を検証できないことも多い．そこで，形式検証ツールのみでは所望 の安全性を検証できない場合に対応するため，人手の証明と形式検証を組み合 わせることで安全性証明を与える方法を提案した．

具体的には，

1. 非同期耐性を備えた RFID システムの提案とその安全性証明への形式検 証の活用（ 4 章）

2. 内部者不正に体制を備えた追跡不可能電子現金システムの提案とその安 全性証明（ 5 章）

3. ハッシュ関数からの内部状態の漏えいを考慮した攻撃モデルでの形式検 証（ 6 章）

について検討した．各概要は下記のとおりである．

RFID システムでは， RFID タグの低コスト化のため，利用できるセキュリ ティ技術に強い制約がある．本論文では，そのような制約の下であっても，非 同期耐性と Forward-security を併せ持つ RFID システムを提案した．そして，

RFID システムの攻撃モデルを構築し，形式検証による安全性証明を検討した．

残念ながら，用いた形式検証ツールの制約により，所望の安全性を直接検証す ることはできなかった．そこで，提案方式を単純化し，単純化した攻撃モデル を構築して，形式検証を行い，単純化方式の安全性を証明した．そして，単純 化方式の安全性の下で，提案方式が所望の安全性を満たすことを人手により証 明した．安全性証明の一部に形式検証を活用することで，信頼性の高い安全性 証明を与えることができたと．

 従来の追跡不可能電子現金システムでは，発行機関の内部者の不正は考慮

されていなかった．また，その安全性解析も非形式的な議論にとどまっている

文献も多い状況であった． [HKOK06] は，発行機関の権限を複数に分散するこ

とで内部者による不正の被害を軽減した方式を提案し，さらに，厳密な安全性

証明を与えた初めての論文であった．本論文では， [HKOK06] で与えられた攻

撃モデルでは見落とされていた強力な結託攻撃が存在することを指摘し，その

ような攻撃をも包含する攻撃モデルを与えた．さらに，その攻撃モデルの下で

安全性が証明できる方式を提案した．この安全性証明は，人手のみで与えてい るが，システムを構成する部品である Abe のブラインド署名の偽造困難性に 帰着することで，安全性証明中の議論を平易にし，人為的な誤りを抑止したと いう特徴を持つ．

 ハッシュ関数からの内部状態の漏えいを考慮した攻撃モデルは，近年の攻 撃技術の発展に伴い，重要性を増している．本研究では，既存の 3 つの漏えい モデルへの形式検証の適用を検討した．検討の結果，形式検証ツールの制約に より， 3 つのモデルを取り扱うことはできないことが分かった．しかし，うち 2 つのモデルについては，それらのモデルと計算量的に等価なモデルを構築し，

それらのモデルの下での FDH 署名の安全性を形式検証ツールで検証すること で，新たに構築した 2 つのモデルが機能することを確認した．残念ながら，残 された 1 つのモデルについては，形式検証手法を根本的に見直さなければ適用 できないと考えている．これは，情報漏えいを考慮したモデルを形式検証で取 り扱ううえで，有用な事例である．

  4 章と 5 章では，提案方式よりもシンプルな方式の安全性に帰着すること で，提案方式の安全性を証明している．また， 6 章では，既存の漏洩モデルを，

形式検証が適用可能なモデルに帰着することで，既存モデルでの安全性を形式

検証した．このように，複雑な攻撃モデル・暗号システムであっても，適切な

モデルを介することで既存の証明結果や形式検証を利用可能とし，証明中の議

論を平易にする方法を与えたこと，安全性証明技法としての本研究の貢献で

ある．

目次

第1章 序論 . . . 1

1.1 研究背景 . . . 1

1.2 本研究の目的 . . . 3

1.3 本研究の成果 . . . 3

1.4 論文構成 . . . 5

第2章 暗号システムの安全性証明 . . . 7

2.1 緒言 . . . 7

2.1.1 本章の構成 . . . 8

2.2 攻撃者のモデル . . . 9

2.2.1 記号的モデル . . . 9

2.2.2 計算量的モデル. . . 10

2.3 ゲーム列による安全性検証 . . . 11

2.3.1 ゲームを用いたモデル化 . . . 11

2.3.2 ゲーム列による検証 . . . 12

2.3.3 3タイプの変形 . . . 13

2.4 形式手法による計算量的安全性の検証. . . 15

2.4.1 間接的手法 . . . 16

2.4.2 直接的手法 . . . 17

第3章 CryptoVerif . . . 19

3.1 緒言 . . . 20

3.2 CryptoVerif . . . 21

3.2.1 概要 . . . 21

3.2.2 プロセス計算 . . . 22

3.2.3 観測等価性 . . . 22

3.2.4 CryptoVerifの動作例. . . 24

3.3 落とし戸付一方向性置換の定式化 . . . 25

3.3.1 一方向性の定式化 . . . 26

3.3.2 逆置換と単射性の定式化 . . . 32

3.4 ランダムオラクルの定式化 . . . 33

第4章 RFIDシステムの提案と安全性検証 . . . 35

4.1 緒言 . . . 36

4.1.1 貢献 . . . 38

4.1.2 関連研究 . . . 39

4.1.3 本章の構成 . . . 40

4.2 RFIDシステム . . . 41

4.2.1 構成 . . . 41

4.2.2 RFIDシステムに求められる安全性 . . . 42

4.3 安全性モデルと定義 . . . 43

4.3.1 攻撃モデル . . . 43

4.3.2 安全性要件の定義 . . . 44

4.4 OMHSOプロトコル . . . 47

4.4.1 仕組み . . . 49

4.5 CryptoVerifのための形式化と検証結果 . . . 50

4.5.1 OMHSOプロトコルの定式化 . . . 50

4.5.1.1 攻撃モデルの定式化 . . . 51

4.5.1.2 ランダムオラクルの定式化 . . . 51

4.5.1.3 補助関数testn,testh0,testh1 の定式化 . . . 53

4.5.1.4 サーバーオラクルの定式化 . . . 54

4.5.1.5 タグオラクルの定式化 . . . 54

4.5.1.6 チャレンジオラクルの定式化 . . . 54

4.5.2 CryptoVerifによる検証結果 . . . 56

4.6 人手による証明 . . . 58

4.6.1 定理 . . . 58

4.6.2 Forward-secureタグ識別不可能性 . . . 58

4.6.3 Forward-secureタグ成りすまし不可能性 . . . 68

4.6.4 Forward-secureサーバー成りすまし不可能性 . . . 72

4.6.5 非同期耐性 . . . 75

4.7 結論 . . . 77

第5章 電子現金システムの安全性検証 . . . 79

5.1 緒言 . . . 79

5.1.1 関連研究 . . . 81

5.1.2 本章の貢献 . . . 81

5.1.3 本章の構成 . . . 82

5.2 定義 . . . 82

5.2.1 準備 . . . 82

5.2.2 電子現金システムの攻撃シナリオ . . . 84

5.2.3 複数銀行による追跡不可能電子現金方式の安全性要件. . . 84

5.3 提案方式 . . . 87

5.3.1 初期設定 . . . 89

5.3.2 鍵生成プロトコル . . . 89

5.3.3 発行プロトコル. . . 90

5.3.4 支払いプロトコル . . . 91

5.3.5 清算プロトコル. . . 92

5.4 安全性 . . . 92

5.4.1 完全性 . . . 93

5.4.2 正直なユーザーの追跡不可能性 . . . 94

5.4.3 不正なユーザーの追跡可能性 . . . 98

5.4.4 (l,l+1)-偽造不可能性 . . . 99

5.5 効率 . . . 102

5.6 結論 . . . 103

第6章 ハッシュ関数からの情報漏洩を考慮した安全性の形式検証 . . . 105

6.1 緒言 . . . 106

6.1.1 本章の貢献 . . . 107

6.1.2 本章の構成 . . . 108

6.2 情報を漏えいするランダムオラクル . . . 108

6.2.1 ランダムオラクル(RO) [18] . . . 108

6.2.2 Leaky Random Oracle (LRO) . . . 109

6.2.3 Traceable Random Oracle (T RO)[74] . . . 109

6.2.4 Extension attack simulatable Random Oracle (ERO)[74] . . . 111

6.2.4.1 CryptoVerifのための定式化(rERO) . . . 112

6.3 情報漏えいを伴うランダムオラクルモデルにおける自動証明 . . . 116

6.3.1 FDH署名と安全性要件 . . . 117

6.3.2 CryptoVerifによるFDH署名の検証結果 . . . 119

6.3.2.1 今回の結果. . . 119

6.4 結論 . . . 121

第7章 結論 . . . 123

参考文献 . . . 125

謝辞 132

本論文に関連・参照した研究業績 134

全ての研究業績 136

著者経歴 143

第 1 章

序論

1.1 研究背景

安全にサービスを提供するために，様々な場面で暗号技術を応用した暗号システムが使われ ている．例えば，エンティティ認証技術や公開鍵暗号は，インターネットのように不特定多数 との通信を安全に行うにはなくてはならない技術である．また，電子決済システムや電子選挙 システムなどの社会インフラを提供する情報システムに対しても，暗号技術は欠かせないもの となっている．

システムを構築する際，構築したものが想定した動作を行うことを検証するのが重要であ る．同様に，暗号システムを構築する際には，構築したシステムが所望の安全性を満たすこと の検証が重要となる．さらに，暗号システムの信頼性を高めるためには，第三者にも理解でき る形で，所望の安全性を満たす証拠を提示できることが望ましい．

現代暗号の黎明期には，暗号システムの安全性の検証は，設計者の勘と経験によりなされる 部分が大きく，攻撃法が発見されると，それに対してアドホックな対策を行うということが繰 り返されてきた．具体的な攻撃手順に対して都度対策を行うアプローチでは，未知の攻撃手順 への対策となっているとは限らず，常に脅威にさらされていると言える．また，勘と経験によ る検証は，第三者による妥当性の検証が困難という問題がある．

一方で，攻撃をモデル化して考え，そのモデルに包含されるすべての攻撃に対して安全性を 数理的に証明する安全性の証明技法が発展してきた．この技法の優れている点は，具体的な攻 撃手順を意識することなく，攻撃を一括して取り扱い安全性を示せることである．また，安全 性証明は数理的に与えられるため，第三者による再検証が可能という利点を備えている．共通 鍵暗号系などのように，安全性証明が困難であるが，非常に重要な要素技術に対しては，現在 においても設計者の勘と経験による検証が主流である．しかし，公開鍵暗号やデジタル署名な

どの公開鍵暗号系では，今日，数理的に安全性証明が与えられていない方式は信頼されないと 言っていい状況である．事実，電子政府推奨暗号や国際標準に選定される公開鍵暗号システム には，安全性証明が必須となっている．このように，安全性証明は暗号システムを普及・活用 していくために無くてはならないものとなりつつある．

典型的な安全性の証明技法では，攻撃者を確率的多項式時間Turing機械として攻撃をモデ ル化し，その攻撃者を利用すると，多項式時間で解くことが困難と信じられている問題—計算 量的仮定—を多項式時間で解くアルゴリズムが構成できること示すのが通常である．つまり，

攻撃者が存在すると，計算量的仮定に矛盾することを証明する．このようにして，計算量的仮 定の下では，暗号システムを多項式時間で破る攻撃者は存在しないことを数理的に証明でき る．この技法によって証明された安全性は，計算量的安全性と呼ばれ，暗号システムを構成す る要素技術—暗号プリミティブ—の脆弱性を考慮した，優れた安全性を評価できる．

安全性証明の問題点として，それ与えるためには，高度な専門知識と複雑な確率評価が必要 となることが挙げられる．さらに，与えられた安全性証明を理解するのも容易ではない．実 際，他人の証明の誤りを見つけられず，発表後に誤りが指摘された例も散見される．

また，近年では，暗号技術を高度に応用することで構築される様々な暗号システムが提案さ れている．このような高度化した暗号システムでは，達成すべき安全性要件も複雑になるた め，安全性証明の複雑さも増す．

さらに，1990年代半ばより，暗号の実装方式より漏えいする種々の情報を利用するして攻 撃を行うサイドチャネル攻撃が提案され，目覚ましい発展を遂げてきた．それまでのの安全性 証明は，暗号デバイスの入出力や通信路を利用した攻撃をモデル化したものが主流であり，物 理的解析などにより漏えいする情報は考慮されていなかった．そのため，安全性証明は与えら れているが，攻撃モデルでは考慮されていない物理的解析により暗号システムへの攻撃が可能 となる事態が生じうる状況となった．このような状況を受けて，物理的解析などにより，暗号 デバイスからの情報漏えいを考慮した攻撃モデルの構築が試みられている．しかし，このよう な攻撃モデルでは，安全性証明中で取り扱う事象が増えるため，安全性証明が複雑になる．

このように，暗号システムの高度化・複雑化や攻撃技術の目覚ましい発展に伴い，安全性証 明の複雑さも増す傾向にあり，証明中の誤りを見落とす可能性も増大している．そのため，証 明中の誤りを防止し，信頼性の高い安全性証明を与える方法が求められている．

一方で，暗号システムの安全性を形式検証の技法で行う研究も行われている．典型的な形式 検証として，攻撃者はあらかじめ定義された記号的操作のみを行うとして攻撃をモデル化し，

そのような攻撃者では暗号システムの安全性を破れないことを示す技法がある．このモデルは 記号的モデルと呼ばれ，計算量的なモデルと比べ，攻撃者に許された操作を書き下すので，攻 撃者の能力を制約した単純なモデルとなる．単純なモデルであるため，その検証の一部は自動

化可能であり，ソフトウェアで検証できるという利点がある．さらに，ソフトウェアを用いる ことで，安全性証明中の人為的な誤りを防止できるため，高い信頼性を持つ検証が実現でき る．しかし，単純化と引き換えに，攻撃者の能力に強い制約を置いているため，評価している 記号的安全性は，計算量的安全性と比較すると，限定された安全性となっている．近年，形式 検証を用いて，計算量的安全性を示す研究が盛んになっているが，計算量的安全性向けの検証 技術は開発途上の段階である．多様な安全性要件を検証するためには，さらなる研究の進展を 要する状況である．

このように，暗号システムの高度化・複雑化や攻撃技術の発展により，安全性証明のための 負担は増す一方であるが，暗号システムの信頼性を保つために，安全性証明は必須のものと なった．そのため，安全性証明を備えた方式の構築技術や，安全性証明中の誤りを防止するこ とでさらなる信頼性の向上を図ったり，安全性証明の負担を軽減する技術への需要が高まって いる．

1.2 本研究の目的

前節で述べたように，安全性証明は学術的にだけではなく，産業的にも重要な意味を持つ．

特に，産業的には，ただ安全性証明を与えるだけでなく，安全性証明中の誤りの防止と負担の 軽減が重要となる．そこで，本研究では，安全性証明を備えた暗号システムの提案を行うだけ でなく，安全性証明の工夫と形式検証の活用によるミスの防止と負荷の軽減を目的とする．ま た，記号的安全性では，実用に供されているシステムとの隔たりが大きいため，より高い安全 性を評価できる計算量的安全性の検証に焦点を当てる．

第2章では，既存の安全性の証明技術を計算量的安全性の観点で整理する．

第3章では，本論文で用いる形式検証ツールであるCryptoVerifを紹介する．

第5章では，匿名電子現金システムを提案し，その安全性証明を与える．

第4章では，RFID認証システムを提案し，その安全性証明を与える．

第6章では，情報を漏えいするランダムオラクルモデルの形式化と，それらのモデルでの形 式検証事例を与える．

1.3 本研究の成果

通常の計算量的安全性の証明は，暗号システムへの攻撃問題を計算量的仮定に帰着すること で行われる．本論文では，人手による安全性証明の複雑さを緩和するために，計算量的仮定ま で帰着するのではなく，暗号システムを構成する要素技術の計算量的安全性に帰着する方法を

活用し，その有用性を示す．具体的には，構成要素の安全性までの帰着にとどめることで安全 性証明中の議論が容易となる．さらに，構成要素の安全性を経由することで，計算量的仮定へ の帰着も示すことが可能であるため，従来の証明と同じ計算量的安全性を示すことができる．

さらに，構成要素の安全性を証明をするために，計算量的安全性を検証する形式検証ツール

CryptoVerifを活用する．残念ながら，計算量的安全性を検証する形式検証ツールは発展途上

の段階であり，現状の形式検証ツールでは，所望の性質を検証できないことも多い．本論文の 検証の対象も，形式検証ツールのみでは，所望の性質を検証することはできなかった．そこ で，前述のように，暗号システムの構成要素の安全性を形式検証ツールで検証し，構成要素の 安全性の下での所望の安全性を人手で証明することで，提案方式の安全性を保証する証明技法 を与えた．

一般に，所望の安全性を証明するにあたって，適切な構成要素の安全性を見出す方法は確立 されていない．第4章と第6章では，形式検証で検証できる安全性を仲介物とし，所望の安全 性を示している．また，第5章では，既存の証明結果を利用して，所望の安全性を証明した．

形式検証や既存の証明結果を活用し，安全性証明中の議論を平易化できる，適切な構成要素を 見出す一手法を与えた点も，本研究の貢献といえる．

第4章で提案した方式は，外部から電力の提供を受けて動作するpassive型のRFIDシステ ムにおいて，RFIDタグ側の計算コストを維持したままで，Forward-securityと非同期耐性を 持つ．従来方式[78]は，非同期耐性を満たさないという脆弱性が指摘されていた．提案方式 は，サーバー側で非同期を検出可能な機構を備えることにより，非同期耐性を達成している．

さらに，提案方式に対して，計算量的安全性を検証するソフトウェアであるCryptoVerifを活 用して安全性証明を与えた．第3章で述べるように，CryptoVerifでは，他のセッションで生 成した値を用いる処理の記述は厳しく制約されている．その制約により，提案方式を記述する ことができなかったため，提案方式を単純化した方式を与え，単純化方式の単純化した安全性

をCryptoVerifで検証した．ここで，単純化方式も，提案方式と同様の方法で非同期耐性を提

供するため，従来方式と比べサーバー側の処理の条件分岐が複雑となる．そのため，サーバー 側の処理を素直に記述しても，CryptoVerifで正しく検証することはできなかった．そこで，

CryptoVerifで正しく検証できるよう，条件分岐の表現方法を工夫した記述を与えた．そして，

単純化方式が安全性を満たすならば，提案方式も所望の安全性を満たすことを人手により証明 した．形式検証ツールが発展途上である現時点では，人手と形式検証ツールを組み合わせた検 証手法は，特に産業的に有用である．

第5章で提案の電子現金システムは，電子現金発行機関を複数に分散することで，内部者の 不正に対しても耐性を実現した方式である．我々は同様のアプローチで内部者の不正に対する 耐性を持つ匿名電子現金システムを提案している[53]．文献[53]の方式が提案されるまでは，

匿名電子現金システムは厳密な安全性証明の対象とはされていなかった．この研究の貢献は，

匿名電子現金システムの攻撃モデルを定式化し，厳密な安全性証明を与えたことである．その 安全性証明は，計算量的仮定に直接帰着するのではなく，暗号システムの構成要素の安全性に 帰着している．このような手法をとることで，安全性証明の複雑さを緩和し，証明中の誤りを 抑制している点が特徴である．残念ながら，文献[53]で定義された攻撃モデルは，攻撃者に制 約があり，この攻撃モデルでは捉えきれない攻撃が存在する．そこで，第5章では，攻撃者に 制約がない攻撃モデルを与え，その攻撃モデルの下で安全性を満たす新しい電子現金方式を提 案する．また，その安全性証明は，文献[53]と同様のアプローチをとり，安全性証明の複雑さ を緩和している．

第6章では，情報を漏えいするランダムオラクルモデルを形式化し，それらのモデルにおけ るFDH署名の安全性をCryptoVerifを用いて検証した．第3章で述べるように，CryptoVerif では，他のセッションで作成した値を用いるための条件に制約が置かれている．そのため，既 存の定義を定式化することはできなかった．そこで，既存の定義と計算量的に等価な定義を与 え，その定義を用いてFDH署名の検証に成功した．この研究は，目覚ましい発展を遂げてい る物理的攻撃技術に対応するために複雑化する安全性証明への形式検証の活用を行った有用な 事例である．

1.4 論文構成

本論文は，7章で構成されている．

第1章は本章であり，本研究の背景，目的と成果を示した．第2章では，本研究で重要な技 術となる既存の安全性証明技法についてまとめる．特に，計算量的安全性と記号論的安全性の 違い，安全性証明中の確率評価を容易にする技術であるゲーム列による検証，計算量的安全性 を証明する既存研究を示す．第3章では，本研究で用いる形式検証ツールであるCryptoVeri の概要を示す．CryptoVerifは，ゲーム列による検証の一部を自動化するツールである．第 4 章では，RFID認証システムを提案し，その安全性証明を与える．第5章では，匿名電子現金 システムを提案し，その安全性証明を与える．第6章では，情報を漏えいするランダムオラク ルモデルの形式化と，それらのモデルでの形式検証事例を与える．第7章で，本論文の成果を まとめるとともに，今後の課題と展望を述べ，結論とする．

第 2 章

暗号システムの安全性証明

本章では，暗号システムの既存の安全性の証明技術を紹介する．暗号の安全性は，大きく分 けて，記号的安全性と計算量的安全性の2つに分けられる．記号的安全性では，記号的操作 のみを行う攻撃者に対して安全性を議論する．そのため，記号的安全性で保証される安全性と 暗号システムの実際の安全性との隔たりが大きいが，形式手法を用いてソフトウェアにより検 証を自動化できるという利点がある．計算量的安全性は，攻撃者を確率的多項式時間 Turing 機械とみなして安全性を議論する．そのため，実際の攻撃者が行う操作をモデル化しているた め，暗号プリミティブの脆弱性も考慮して暗号システムの安全性を評価できるが，攻撃の成功 確率を得るために確率事象の複雑な評価が必要となる．

特に，本章では，計算量的安全性の証明中の誤りを防止し，信頼性を高める手法である，ゲー ム列による検証と形式手法による検証を紹介する．

2.1 緒言

暗号システムが安全であるとは，あらゆる攻撃手段に対して，攻撃が成功しないことである．

しかし，攻撃の手段は無数に存在するため，そのようなことを示すことは非常に困難である．

暗号システムに対して具体的な攻撃手順を示し，その手順では攻撃が成功しないことを示し て，安全性を主張する方法もある．しかし，この方法では，別の攻撃手順に対する安全性は何 も示していない．そのため，システムを設計した際には想定していなかったり，見落としてい たりした攻撃により，安全性が破られる恐れがある．

そこで，具体的な攻撃手順に対して個別に安全性を議論するのではなく，攻撃をモデル化し て考え，そのモデルに包含されるすべての攻撃に対して安全性を数理的に示す安全性解析のフ レームワークが発展してきた．安全性証明の優れている点は，具体的な攻撃手順を意識するこ

となく，攻撃を一括して取り扱い安全性を示せることである．また，安全性証明は数理的に与 えられるため，第三者によるも再検証が可能である．

暗号システムの安全性解析のフレームワークは，大きく分けて，計算量的モデルを用いるも のと記号的モデルを用いるものの2つに分けられる．

計算量的モデルにおいて最も有名なフレームワークは，計算量的仮定への帰着による証明 可能安全性[16]で，暗号理論で頻繁に用いられている．このフレームワークにおける攻撃者 は確率的多項式時間Turing機械で，ある暗号プリミティブ/システムに対して定義される攻撃 ゲームに勝とうとする．計算量的な安全性は，次のような矛盾を導くことで証明される：も し，攻撃者が無視できない確率で攻撃ゲームに勝利するならば，well-definedな計算量的仮定 (一方向性や素因数分解問題の困難性など)は破られる．結果，暗号システムの安全性は計算量 的仮定を安全性の根拠とすることが示せる．このフレームワークは，現実の暗号システムが扱 うデータレベルのモデル化となっている．

記号的モデルにおいて最も有名なフレームワークは，Dolev-Yao [44]フレームワークで，こ のフレームワークも暗号プロトコルの安全性解析を行うことができる．Dolev-Yao フレーム ワークでは，暗号プリミティブ/システムが入出力する情報は全て記号で表現される．攻撃者 は，入手した記号に対して，あらかじめ定義された任意の記号的操作を行って，暗号プリミ ティブ/システムに入力し，新たな記号を入手できる．そして，攻撃者は，上記の操作を繰り返 し，攻撃成功の条件を満たす記号を導こうとする．通常，記号的操作には暗号プリミティブの 安全性を破る操作は含まれない．つまり，記号的な安全性検証は，暗号プリミティブは理想的 なブラックボックスとして扱う，非常に強い仮定の下での検証といえる．そのため，記号的安 全性が成り立ったとしても，計算量的安全性も成り立つとは限らない．一方で，このフレーム ワークでは，非常に強い仮定の下ではあるが，検証の対象を単純化しているため，形式検証に より，検証をソフトウェアで自動化することが可能という利点がある．

近年では，計算量的モデルにおける安全性を形式的検証で行おうとする研究が活発になって いる．

2.1.1 本章の構成

第2.2節では，攻撃をモデル化する方法について示す．安全性を数理的に解析するために は，攻撃のモデル化が必須である．特に，前述の計算量的安全性と記号論的安全性を対比する 形で，モデル化の方法を示す．

第2.3節では，ゲーム列による安全性検証法を紹介する．計算量的安全性は，暗号プリミ ティブの脆弱性まで考慮して暗号システムの安全性を評価できるという利点があるが，アドバ

ンテージを評価するために複雑な確率評価が必要であった．ゲーム列による検証を用いると，

評価対象の確率事象を絞り込むことで，アドバンテージの評価をシンプルにできる．そのた め，証明中の人為的な誤りを防止したり，誤りを発見しやすくしたりする効果が期待できる．

第2.4節では，形式手法を用いて，計算量的安全性を検証する既存研究を紹介する．形式手 法を利用するアプローチは，記号論的安全性を介する間接手法と計算量的安全性を直接示す直 接手法の2つに分けられる．

2.2 攻撃者のモデル

安全性証明では，暗号プロトコルが実行される状況をモデル化し，そのモデルに包含される あらゆる攻撃に対する安全性を理論的に保証する．

安全性証明を議論するためには，以下の3点を明確に定義する必要がある．

• ^暗号方式

• 設計者が達成したい安全性の目標

• ^{攻撃者に許された戦略}

安全性は，目標と戦略の組み合わせごとに定義される．攻撃者の目標が容易になればなるほ ど，戦略に制約が少なければ少ないほど，強力な安全性の定義となる．暗号方式自体は様々な 状況下で用いられることを想定して，できる限り強力な安全性を示すことが望ましい．

モデル化の方法は，大きく分けると2つに分類され，それぞれ記号的モデルと計算量的モデ ルと呼ばれる．

以下では，各モデルの概要を述べる．

2.2.1 記号的モデル

記号的モデルでは，攻撃者はあらかじめ定義された記号的操作をのみを行うとして攻撃をモ デル化する．代表的な記号的モデルである Dolev-Yaoフレームワークでは，暗号プリミティ ブ/システムが入出力する情報は全て記号で表現される．主に通信路を介して実行される暗号 システムが評価の対象で，攻撃者は通信路を流れるすべて情報に対して，盗聴・妨害・改ざん などが可能な状況をモデル化している．暗号システムを平行に動作するプロセスが通信路を介 して行う記号のやり取りとしてモデル化する．攻撃者は，通信路を流れる記号をすべて入手で き，その記号に対して任意の記号的操作を行い，その結果を通信路に流すことができる．そし て，攻撃者が上記の操作を繰り返し，攻撃成功の条件を満たす記号が導けるとき，その暗号シ

ステムは安全でないことが示せる．

記号的モデルは，攻撃者を記号的操作で定義されていない処理は実行できないよう制約して いるとみることができる．通常，記号的操作には暗号プリミティブの安全性を破る操作は含ま れない．例えば，Dolev-Yaoモデルでは，暗号文からその平文を取り出せるのは，復号用の鍵 を持っている場合に限られ，復号用の鍵を持っていないと，平文に関する情報が一切漏れない と解釈できる，つまり，記号的な安全性検証は，暗号プリミティブを理想的な安全性を持つブ ラックボックスとして扱う，非常に強い仮定の下での検証といえる．そのため，記号的安全性 が成り立ったとしても，計算量的安全性も成り立つとは限らない．一方で，このフレームワー クでは，検証の対象を抽象化することでシンプルに取り扱うことができるため，ソフトウェア により検証を自動化できるという利点がある．

2.2.2 計算量的モデル

計算量的モデルでは，攻撃者を確率的多項式時間Turing機械としてモデル化し，攻撃者は 与えられる情報に対して，多項式時間で実行可能なあらゆる操作を行うことができる．

代表的なモデルは，暗号システムへの攻撃者は確率的多項式時間Turing機械とし，攻撃に より入手できる情報はオラクルへの入出力で表現し，安全性は攻撃者の出力が満たす条件式と するものである．このモデルの下で，安全性を破る攻撃者が存在すると，困難と信じられてい る計算量的仮定を効率的に解くアルゴリズムが構成できることを示すことで，安全性が証明で きる．すなわち，計算量的仮定が成立するならば，攻撃者は存在しないことを証明している．

この方法は，帰着技法と呼ばれ，計算量的仮定を用いない情報量的な安全性証明と共に，現代 暗号の安全性証明によく用いられる技法の一種である．暗号プロトコルの安全性証明は，攻撃 者のアドバンテージ—悪意ある敵の攻撃成功確率と偶然攻撃が成功する確率の差—の上限を 評価することで行われる．一般的に，アドバンテージの評価には，依存しあった事象の確率評 価が必要となるため，複雑になることが多い．そのため，証明の誤りを見落としてしまい，証 明を発表後，数年たってから指摘された例もある[19, 85]．

そこで，第2.3節で紹介するゲーム列による安全性検証法を用いて，アドバンテージの評価 をシンプルにすることで，証明中の人為的な誤りを防止したり，発見しやすくしたりする方法 をとることもある．

2.3 ゲーム列による安全性検証

ゲーム列による検証[86, 79, 20]は，安全性証明において攻撃者のアドバンテージの評価を シンプルにする方法の1つである．ゲーム列による検証では，攻撃として許す戦略と攻撃の目 標を明確に定義し，攻撃の状況をゲームとしてモデル化する．そして，攻撃ゲームの一部を変 形した新たな攻撃ゲームを生成し，変形によって生じる差に注目して評価を行う．偶然でしか 攻撃が成功しない攻撃ゲームにいたるまで，攻撃ゲームの変形と評価を繰り返すことで，評価 対象の攻撃を評価する．評価対象の攻撃ゲームと偶然でしか攻撃が成功しない攻撃ゲームの差 が， 無視できるほど小さい とき，攻撃者のアドバンテージは十分小さいことが示せるため，

安全性が証明できる．ゲーム列による検証では，評価対象が複雑であっても，変形によって評 価対象を明確に絞り込むことで誤りを抑制しようとする．

攻撃者が攻撃に成功する確率と攻撃に偶然成功する確率の差をアドバンテージと呼ぶ．アド バンテージの上限を評価し，アドバンテージの上限が十分に小さいとき，暗号プロトコルは安 全であるという．

ゲーム列による検証のアイディアは，GoldwasserとMicali [48, 47]やYao [88]の文献に登 場するHybrid argumentが起源となっている．

その後，ゲーム列による検証は，様々な文献で用いられており，帰着技法だけでなく，シ ミュレーションパラダイムと呼ばれる技法を駆使した安全性証明にも用いることができる．

2.3.1 ゲームを用いたモデル化

暗号方式の安全性は，一般的に 攻撃者と挑戦者によるゲーム として定義される．攻撃者 と挑戦者は，お互いに通信する確率的多項式時間Turing機械[46]であるため，ゲーム自体は 確率空間としてモデル化される．安全性証明のためには，ゲーム中でイベント S が起こると き，暗号方式の安全性が破られるように，ゲームをデザインする．安全性は，あらゆる 効率 的な 攻撃者に対して，イベントS が起こる確率が，ある ターゲット確率 と 非常に近 い ことを意味している． ターゲット確率 は，攻撃が偶然に成功する確率であることが多 い． ターゲット確率 の例としては，0，1/2のような具体的な値や，別のゲームにおいて同 じ攻撃者が別の挑戦者と対話してあるイベントT を起こす確率などが挙げられる．

厳密な定義では，セキュリティパラメータは整数で， 効率的な とはセキュリティパラメー タの多項式で制限された時間を意味し， 非常に近い とは差を表す関数が 無視できるほど 小さい ことをいう． 無視できるほど小さい 関数の厳密な定義は以下の通りである．

定義1 (Negligible) p(·) は正多項式とする．以下の条件を満たすとき，関数 µ : N → R ^は negligibleという．

∀p(·)∃N ∈Nsuch that∀n> N µ(n)< 1 p(n)

イベントS が起こる確率とターゲット確率の差をあらわすす関数がNegligibleとは，セキュ リティパラメータのあらゆる多項式の逆関数について，十分に大きなセキュリティパラメータ に対しては，あらゆる多項式よりも差をあらわす関数が小さいことを意味する．また， 無視 できる とは，0と 非常に近い ことを意味する．簡単のため以降では，攻撃者など全ての アルゴリズムには，セキュリティパラメータが暗に入力されているとする．

2.3.2 ゲーム列による検証

ゲーム列による検証は，安全性証明中で攻撃成功確率の評価を容易にする方法の1つであ る．様々な事象をオラクルを用いて抽象化し，オラクルの呼び出し順序に制限を設けるなどし て，絡み合った依存関係としてモデル化する．次に，モデル中のオラクルの処理を別の処理で 置き換えて変形を行い，新たなモデルを生成する．そして，変形によって生じるモデル間の攻 撃成功確率の差を評価する．例えば，偶然でしか攻撃に成功しないモデルまで変形を繰り返 し，各モデル間の差を評価して，生じた差をたしあわせることで，攻撃者のアドバンテージが 評価できる．モデル間の攻撃成功確率の差の評価を行うときは，変形による処理の違いに注目 する．あらかじめ，評価すべき事象を明確に絞り込むことで，事象の見落としを防止できる．

また，上手に変形することで，評価対象自体をシンプルにできるため，評価の誤りを抑制し，

可読性の高い証明が期待できる．

Game 0 Game 1 Game 2 Game n

Pr[S₀] Pr[S₁] Pr[S₂] Pr[S_n]

図2.1 ゲーム列

ゲーム列を用いた安全性の検証は以下のような手順で行われる．まず，イベントS が生じ たとき攻撃成功とし，イベントS が生じる確率と ターゲット確率 の差がnegligibleである とき，所望の安全性を達成するように，評価対象の暗号方式と攻撃者による攻撃ゲームGame 0をデザインする．

S をイベントS0 とする．そして，Game 0，Game 1，. . .^，Gamenのゲーム列を構成する．

i= 1, . . . ,nについて，Gameiにおける攻撃成功イベントS であるイベントS_i を考える．そし て，i=0, . . . ,nについて，Pr[S_i]とPr[S_i+1]の差がnegligibleであることと，Pr[S_n]が ター ゲット確率 と等しい(または差がnegligibleとなる)ことを証明する．nが定数であるとき，

negligibleな差を定数回積み重ねても その差はnegligibleであるため，Pr[S]と ターゲット確 率 の差はnegligible であることが示せる．Pr[S]と ターゲット確率 の差が negligibleで あるとき，安全性が成立するようにイベント S はデザインされているため，安全性を証明で きる．

2.3.3 3 タイプの変形

ゲーム間に生じる差がnon-negligibleならば安全性は成立しない．一方，差を評価できなけ れば安全性は示せない．よって，前述の証明を与えるゲーム列の構成法は，ゲーム間に生じる

差は，negligibleであり，簡単に評価できることが望ましい．

そこで，ゲーム列による検証では，初期ゲームGame 0に変形を加えてゲーム列を構成す る方法が取られる．Shoup[86]は，経験則に基づき，ゲームの変形を次の3つのタイプに分類 した．

• 識別不可能性に基づく変形

• 失敗イベントに基づく変形

• ^{橋渡し変形}

以下では，各変形の性質と評価方法を記す．

■識別不可能性に基づく変形 ゲーム間の差を識別できる攻撃者が存在するならば，その攻撃 者を利用して，(統計的または計算量的)識別不可能な二つの分布を識別する効率的な方法が構 成できる変形である．

例えば，この変形は，識別不可能な分布P1 とP2 について，攻撃者へのある入力を分布P1

で選ぶとGameiとなり，その入力を分布P2 で選ぶとGamei+1となるメタゲームGame H を構成することで行う．

|Pr[Si]−Pr[Si+1]|^がnegligibleであることを示すために，Game Hに対して，次のような効 率的な識別アルゴリズムDが構成できること示す．

• Game Hに付加入力を分布P1 で与えたとき，Pr[Si]で1を出力．

• Game Hに付加入力を分布P₂ で与えたとき，Pr[S_i+1]で1を出力．

もし，|Pr[S_i]−Pr[S_i+1]|^がnegligibleでないならば，D^はGame iとGamei+1を識別する．

Game iとGamei+1の違いは，Game Hへの付加入力の分布P₁,P₂ のみであるので，D^は P1 とP2 を識別するといえる．これは，P1 とP2 は識別不可能という条件に矛盾する．よっ て，|Pr[Si]−Pr[Si+1]|^がnegligibleであることが示せる．

Game i Game i+1

] S

Pr[ _i Pr[ S _{i + 1} ]

Game H

P

P

D

図2.2 識別不可能性に基づく変換の評価

最小限の確率事象に着目してゲームを変形するなど，上手に変形を行うことで，通常，上記

のようなGame Hの識別アルゴリズムD^{を容易に構成できる．}

■失敗イベントに基づく変形 GameiとGamei+1は，ある 失敗イベントF が生じる場 合を除いて，完全に同じに実行される変形である．

F が生じないとき完全に同じ実行となることを明確に示すためには，二つのゲームは同じ確 率空間上に定義されているのが望ましい．例えば，二つのゲーム間の違いは，あるランダムな 変数の計算法のみである変形が扱いやすい．このような変形を行うと，二つのゲームはイベ ント F が生じる場合を除いて完全に同じ実行となることが示せるので，イベントS_i∧ ¬F と Si+1 ∧ ¬F は 同じ である．これを

S_i∧ ¬F ⇐⇒S_i+1∧ ¬F

と書く．このとき，次の補題が適用できる．

補題1 (Difference Lemma)A,B,Fは同じ確率分布上に定義されたイベントとし，A∧ ¬F ⇐⇒

B∧ ¬F であるとする^*1．このとき，|Pr[A]−Pr[B]| ≤Pr[F]が成立する．

*1この補題はPr[A∧ ¬F]=Pr[B∧ ¬F]が成立していれば導けるため，A,B,Fの確率空間が異なる場合に一般化 できる．しかし，評価をシンプルに行うためには，同一の確率空間上に定義されていることが望ましい．

証明：A∧ ¬F ⇐⇒B∧ ¬Fなので，Pr[A∧ ¬F]=Pr[B∧ ¬F]が成り立つ．一方，Pr[A∧F]と Pr[B∧F]は，0≤ Pr[A∧F],Pr[B∧F]≤ Pr[F]である．よって，

|Pr[A]−Pr[B]|= |Pr[A∧F]+Pr[A∧ ¬F]−Pr[B∧F]−Pr[B∧ ¬F]|

= |Pr[A∧F]−Pr[B∧F]|

≤ Pr[F].

よって，Pr[Si]とPr[Si+1]が極めて近いことを証明するには，Pr[F]がnegligible であるこ とを証明すれば十分である．この証明には，安全性の仮定を用いることが多い．例えば，イベ ントFが生じたとき，攻撃者はハッシュ関数の耐衝突性やMACの偽造不可能性などを破るこ とを示して，イベントFが生じる確率はnegligibleであることを示す．また，情報理論的な議 論が用いられることもある^*2．

通常，イベント Fは二つの隣接したゲームの1つのランダムな値に関して定義され，評価 される．イベント F の決め方は任意であるが，明解な証明を行うためには適切に決定する必 要がある．

また，一方のゲームにおけるイベント F の評価は難しい場合があることに注意が必要であ る．事実，イベント F を評価するためゲーム列を構成したり，イベントF を評価するための ゲーム列とイベントS を評価するためのゲーム列が一致する必要がある場合などがあり，そ のときPr[F]は j>i+1なるGame jで初めて評価できる．

■橋渡し変形 ゲーム中のある手順を，完全に等価な手順で置き換える変換である．このと き，Pr[S_i] =Pr[S_i+1]となる．前の2つのタイプの変換を行うための準備として，この変換を 行う．原理的には，橋渡し変換は必要ないように思えるかもしれないが，橋渡し変換を行うこ とで，以降の評価を容易にできる場合がある．

2.4 形式手法による計算量的安全性の検証

第2.2節で述べたように，記号的モデルで安全性を保証したとしても，計算量的モデルでも 安全性が保証されるかは明らかではなかった．計算量的モデルは，現実の暗号システムがやり 取りするデータレベルでの抽象化を行ったモデルであるため，暗号システムは計算量的安全性 が保証されていることが望ましい．

記号的モデルで安全ならば計算量的モデルでも安全性が保証されるとき，その検証法は「計 算量的健全性」を満たすという．近年では，両モデルの長所をあわせ持った計算量的健全性を

*2例えば，[40]を参照されたい．

満たす検証法の研究が盛んになっている．そのような手法は，間接的手法と直接的手法の2つ に大別される．本節では，2つの手法に関する代表的な研究を紹介する．

2.4.1 間接的手法

Dolev-Yaoモデルでは，暗号プロトコルの構成要素である暗号プリミティブに理想的な安全

性を仮定して記号的検証を行うため，その検証結果が，計算量的な意味で安全かどうかは明ら かではなかった．このような問題意識の下で，記号的安全性の解析結果より，計算量的安全性 を示す研究が行われている．

AbadiとRogaway[5]は，共通鍵暗号を用いた暗号プロトコルに対して，ある前提条件のも

とで，Dolev-Yaoモデルによる記号的安全性が計算量的安全性を保証することを示した前提と

した条件は，理想的な安全性を持つ共通鍵暗号方式で，暗号文から読み取れる情報の等価性を 記号的に定義し，暗号文が等価ならば計算量的に識別不可能であることを示した．すなわち，

記号的に定義された暗号文の識別不可能性の計算量的健全性を示した．しかし，これらの結果 は限定的で，強い仮定(共通鍵暗号はDolev-Yaoモデルと同様に非常に理想的な安全性を持っ ている．)と限定された暗号プロトコル(Key cycleがない)の下でしか成り立たない．

計算量的健全性の対偶は，「計算量的モデルで無視できない確率で攻撃が成功するならば，

記号的モデルでも攻撃が成功する」である．この対偶を利用して計算量的健全性を示す方法が

ある[73, 39, 58]．この方法では，「計算量的モデルで無視できない確率で起こりうるプロトコ

ル実行（攻撃）は，記号的モデルでも起こりうる」ことを主張するマッピング補題（mapping

lemma）を示す．計算量的モデルと記号的モデルで「攻撃が成功する」ことの定義が同じ意味

であるならば，マッピング補題から健全性を導くことができる．マッピング補題は，暗号やデ ジタル署名などの暗号プリミティブが安全であることを仮定して導かれている．

文献[5]の結果は受動的攻撃者に限定した場合の計算量的健全性に留まっていたが，その結 果を拡張し，適応的な攻撃者に対する健全性が示されている[66]．また，公開鍵暗号を用いた 認証プロトコルのUniversal Composability [29, 30]の意味での計算量的健全性[33]，リング署 名の匿名性に対する計算量的健全性[63]，再暗号化可能暗号の安全性であるIND-RCCA安全 性の計算量的健全性[64]など，さまざまな性質の計算量的健全性が示されている．このよう に，計算量的健全性が成り立つ性質や方式に関する研究が進められているが，依然として，未 解決の問題も多く残されている．

2.4.2 直接的手法

既存の形式検証のフレームワークに確率の概念などを導入して拡張することで，計算量的 安全性を直接取り扱うことができる形式的検証のフレームワークの研究が進められている．

CorinとHartogは，確率Hoare論理[42]を用いて，ElGamal暗号のゲーム列による安全性証 明を形式化した．Hoare論理は，プログラムが正しいことを証明するための論理体系である．

正しさの証明は，{p}s{q}^{という形の}3項組で表現される．これは，Hoareの3つ組と呼ばれ，

sはプログラム，pとqはそれぞれ事前条件および事後条件と呼ばれる．Hoareの3つ組の直 観的な意味は，「事前条件 pが成り立つ状態において，プログラムsを実行すると，その実行 後の状態では事後条件qが成り立つ」ということである．この場合，状態とはプログラム変数 への値の割り当てである．確率Hoare論理は，これに確率に関する拡張を施したものである．

プログラミング言語に関して，s₁⊕ρs₂ が導入される．直観的な意味は，s₁とs₂をそれぞれ確 率ρ^と1−ρで選択して実行するということである．また，状態は，Hoare論理における状態 の確率分布となる．Corinらの証明は，変換前後のゲームを与えられたときに，その変換が正 しいことを検証している．しかし，変換前のゲームから変換後のゲームをいかに導くかという ことには十分に答えていない．

Canettiらは，暗号システムの検証を目的として，タスク構造確率I/Oオートマトン(タスク

PIOA)を用いるフレームワークを提案した[31]．タスクPIOAフレームワークはは，オートマ

トン理論を応用した検証技法である．従来より，オートマトン理論は，分散アルゴリズムや通 信プロトコルのモデル化や解析に用いられてきた．確率I/Oオートマトン(PIOA)は，確率的 選択と日決定的選択の両方を行うことができるという利点から，ランダム性を伴うアルゴリズ ムの機能的正当性を検証するのに有効である．PIOAは，状態集合，アクション集合，繊維集 合からなる．PIOAフレームワークでは，非決定的選択によって現在の状態から次に遷移する アクションを決定し，確率的選択によって繊維後の状態を決定する．これら2つの選択によっ て，暗号システムで想定される複雑な状況を表現できる．残念ながら，PIOAフレームワーク は，機能的正当性を検証することを目的としており，そのまま安全性検証に適用すると，無限 の計算能力を持つ攻撃者に対する検証となってしまう．そのため，計算量的安全性の検証には 用いることができない．タスクPIOAフレームワークは，PIOAフレームワークにアクション の同値類の集合である「タスク」を加えたものである．タスクの直観的な意味は，「本質的に 同じ動作とみなすことができるアクションをひとまとめにしたもの」である．タスクの列とし てスケジューラを構成することで，過去の実行における動的な値の変化に依存せず非決定的選 択を解決できる．これにより，遷移の仕方から攻撃者に対して秘密情報が漏れる可能性を考え

なくても良くなるため，秘匿性などの安全性検証にもタスクスケジューラを適用できる．さら

に，Canettiらは，計算量的安全性を扱うために，時間制限タスクPIOAフレームワーク[32]

を考案した．PIOAの各ステップに時間制限を課すことで，計算能力が制限された機器や攻撃 者を表現する．同様に，タスクスケジューラにも時間制限を課す．これにより，計算量的安全 性を取り扱うことができる．Canettiらは，時間制限タスクPIOAを用いて，ある紛失通信プ ロトコルの安全性証明の例を示している．

Blanchetらは，確率プロセス計算を拡張して，ゲーム列による検証を行うフレームワークを

提案した[21, 22]．さらに，Blanchetのフレームワークを実装したソフトウェアCryptoVerifを 開発している．CryptoVerifを用いることで，一方向性の下で署名のEF-ACMA安全，Message Authentication Code(MAC)のEF-ACMA安全，ストリーム暗号のIND-CPA安全，公開鍵暗 号のIND-CPA安全と IND-CCA2安全が自動証明できることが知られている．CryptoVerif は，本研究で用いたソフトウェアであるため，詳細な説明を第3章で説明する．

近年では，定理証明支援システムを利用し，暗号システムの形式検証を行うフレームワーク

[10, 9, 13, 14]も提案されている．これらのフレームワークは，定理証明支援システムの機能

を生かし，信頼性の高い検証が実現できるという利点があるが，検証に手間がかかるという問 題がある．しかし，最近盛んに研究されており，今後の発展が期待されるアプローチである．

第 3 章

CryptoVerif

計算量的仮定を取り扱うことができるフレームワークのひとつとして，Blanchetのフレーム

ワーク[21, 24]があり，そのフレームワークに基づく検証を行うソフトウェアCryptoVerifが

公開されている^*1．

Blanchetのフレームワークでは，計算量的仮定を以下で定義する観測等価性による関係式と

して定式化する．例えば，BlanchetのフレームワークのためにComputational Diffie-Hellman 仮定 (CDH仮定)を定式化する際には，CDH問題に対する能動的攻撃モデルを定式化しなけ ればならない．

Blanchetはゲーム列による証明 [86] を記述するためのプロセス計算を定義し，それを用

いた形式的検証のフレームワークを提案した．このフレームワークにおける安全性証明は，

Blanchetのプロセス計算で攻撃モデルと書き換えルールを記述し，攻撃モデルを書き換えルー

ルに従って変換し，安全性要件を満たすモデルに変換可能か評価することで構成される．

書き換え規則は，観測等価性を満たす二つのプロセスで記述される．大雑把にいうと，観測 可能な値からは二つのプロセスを一定以上の確率で識別できないとき，観測等価性を満たすと いう．

プロセス計算で表現された攻撃モデルの書き換え規則の下での安全性証明はCryptoVerifに よって自動化されているが，現在のところ，書き換え規則の設定や観測等価性の証明は人間が 行わなければならない．

*1 http://www.cryptoverif.ens.fr/

3.1 緒言

暗号プロトコルの安全性証明は，攻撃者のアドバンテージ—悪意ある敵の攻撃成功確率と偶 然攻撃が成功する確率の差—の上限を評価することで行われる．一般的に，攻撃者のアドバ ンテージの評価は，依存しあった事象の確率評価が必要となるため，複雑になることが多い．

ゲーム列による検証では，安全性証明において，評価の対象とする確率事象を明確に絞り込む ことで，誤りを抑制しようとする．適切にゲーム列を構成すれば，シンプルな評価を積み重ね ることで，攻撃者のアドバンテージが評価できる．

安全性証明のテクニックの一つとして，ゲーム列による検証がある．ゲーム列による検証で は，攻撃として許す戦略と攻撃の目標を明確に定義し，攻撃の状況をゲームとしてモデル化す る．そして，攻撃ゲームの一部を変形した新たな攻撃ゲームを生成し，変形によって生じる差 に注目して評価を行う．偶然でしか攻撃が成功しない攻撃ゲームに至るまで，攻撃ゲームの変 形と評価を繰り返すことで，評価対象の攻撃を評価する．評価対象の攻撃ゲームと偶然でしか 攻撃が成功しない攻撃ゲームの差が， 無視できるほど小さい とき，攻撃者のアドバンテー ジは十分小さいことが示せて，安全性が証明できる．

ゲーム列による検証を形式的に行うフレームワークの研究が盛んに行われており，注目を集 めている．Blanchetらは，そうしたフレームワーク [24, 21]の一つを提案しており，そのフ レームワークに基づいた検証を行うソフトウェアCryptoVerifを開発している．

CryptoVerifによる安全性証明は，まず，人手によりBlanchetのプロセス計算[21, 24]で攻 撃モデルと書き換えルールを記述する．それらを，CryptoVerifに入力すると，攻撃モデルを 書き換えルールに従って変形し，安全性要件を満たすモデルに変形可能か評価する．変形可能 であった場合，変形に用いた書き換え規則より，攻撃者のアドバンテージを評価する．

書き換えルールは，観測等価性という関係を満たす二つのプロセスで記述される．大雑把 に言うと，観測可能な値からは二つのプロセスを一定以上の確率で識別不可能なとき，観測 等価であるという．証明に必要な計算量的仮定は，プロセス間の観測等価性で表現される．

CryptoVerifを用いることで，暗号プロトコルの安全性証明の一部が自動化できるため，証明

の手間の軽減や，人為的な誤りの防止による信頼性の向上が期待されている．

これまで，CryptoVerifのバグにより正しい検証結果が得られないという指摘が何度かなさ れているが，その都度，修正が行われている[23, 91, 90]．

CryptoVerifを用いた安全性証明に成功した方式として，FDH署名や公開鍵暗号方式[18]な

どがある．