形式手法の計算論的健全性
川本 裕輔

LIX, École Polytechnique & INRIA Saclay, France

概要
形式手法の「計算論的健全性」とは，形式手法を用いて安全性が証明された暗号プロトコルは，計算量理論の観点からも安全であるという性質である．

1

形式手法の計算論的健全性[数理的技法による情報セキュリティの検証]（p.244）でも述べたように，暗号プロトコルの安全性の解析には「形式手法」と「計算論的手法」がある．形式手法による解析は，計算論的手法による解析と異なり，プロトコルの部品として用いる暗号方式に対する攻撃の確率を考慮しない．このため，形式手法を用いて安全性が確かめられたプロトコルに対し，暗号の脆弱性に基づく攻撃が存在する可能性がある．
一方，暗号を破る攻撃の確率が十分小さい場
合，形式手法の計算論的健全性（すなわち，形式手法を用いて安全だと証明されたプロトコルは，計算論的手法における計算量的安全性を満たすという性質）を示せる．計算論的健全性は，暗号方式の安全性の種類，検証したいプロトコ
ルの安全性の種類，想定する攻撃者の種類に応じて，様々な結果が知られている．

2

受動的攻撃者のもとでの計算論的健全性

まず，受動的攻撃者（通信内容を傍受できるが，改竄できない攻撃者）を想定する場合の計算論的健全性 [1] を説明する．本節では逐次的にメッセージを送受信するだけのプロトコルを考える．プロトコル実行は，通信路上のメッセー
ジの連結で表現される．

2.1

構文論と記号的等価性

メッセージを項（記号表現）で表す．項として，鍵記号 K ，ビット 0 と 1，項の連結 (M, N )，項 M の鍵 K による暗号文 {M }K を記述できる．ここでは対称鍵暗号のみを扱う．項 M から読み取れる情報を表現するために，パターン
pat(M ) を定義する．

p(M, T ) = M(M ∈ K ∪ {0, 1} のとき)

p((M, N ), T ) = (p(M, T ), p(N, T ))({p(M, T )}K （K ∈ T のとき）
p({M }K , T ) =□（K ̸∈ T のとき）
pat(M ) = p(M, {K ∈ K | M ⊢ K})
ただし，K は全ての鍵記号の集合，□ は解読できない暗号文，{K ∈ K | M ⊢ K} は項 Mから導出できる全ての鍵記号の集合を表す．例
えば，{K ∈ K | ({{0}K1 }K2 , K2 ) ⊢ K} = {K2 }より，pat(({{0}K1 }K2 , K2 )) = ({□}K2 , K2 )．
次に，項の間の記号的等価性 ∼= を定義する．
項 N に現れる各鍵記号 K を σ(K) で置き換えたものを N σ と書く．項 M ，N に対し，K 上の全単射 σ が存在し，pat(M ) = pat(N σ) のとき，M ∼= N と書く．例えば，({0}K1 , {1}K2 ) ∼=({1}K3 , {0}K1 )．

2.2

計算論的意味論と計算量的識別不能性

以下では，記号列としての項に対し，ビット列の確率分布の族を対応付ける「解釈」を定義する．
対称鍵暗号方式 Π を，鍵生成，暗号化，復号アルゴリズムの三つ組 (K, E, D) と定義し，自然数 η をセキュリティ・パラメータ，τ を乱数テープとする．
項 M に対応するビット列 [[M ]]τΠ,η を，[[K]]τΠ,η = ⟨k, “key”⟩[[i]]τΠ,η = ⟨i, “bool”⟩(i ∈ {0, 1})[[(M, N )]]τΠ,η = ⟨[[M ]]τΠ,η , [[N ]]τΠ,η , “pair”⟩[[{M }K ]]τΠ,η = ⟨Eτ ([[M ]]τΠ,η , [[K]]τΠ,η ), “enc”⟩
で定める．k は τ の乱数と K で生成される鍵とし，E は τ の乱数を用いて暗号化する．末尾のタグでメッセージの種別を表す．τ をランダムに選んだときのビット列 [[M ]]τΠ,η の確率分布を[[M ]]Π,η とし，確率分布族 {[[M ]]Π,η }η∈IN を Mの解釈 [[M ]]Π とする．
確率分布族 D = {Dη }η∈IN と D′ = {Dη′ }η∈IN ，任意の確率的多項式時間（PPT）アルゴリズ
ム A に対し，次の関数 ε が無視できる1 とき，D と D′ が計算量的に識別不能であるといい，D ≈ D′ と書く．

攻撃者の動作として，参加者の集合 a による新しいセッションの生成 new (a) と，セッションs への項 t の送信とそれに対するの応答の受信
send (s, t) を扱う．攻撃者は，受信した項の集合 H から導出できる項のみを送信する．H から項 t が導出できるとき，攻撃者のラベル l を用いて {t}lpk(ai ) を導出できる．H から {t}lpk(ai )と sk(ai ) を導出できるとき，t を導出できる．
受信した項の集合 Hj と攻撃者の動作 Ej の列
Eε(η) = Pr [x ← Dη : A(x) = 1]
− Pr x ← Dη′ : A(x) = 1

2.3

記号的等価性の計算論的健全性

ビット列 m の鍵 k による暗号文を受信した
受動的攻撃者が，m や k についていかなる情報も多項式時間で得られないとき，type-0 安全であるという．
項 {K}K や {{K1 }K2 }K1 のように，暗号化に用いる対称鍵が暗号化されるメッセージの中に含まれることを鍵循環という．
定理 1 M と N を鍵循環を含まない項とし，対称鍵暗号方式 Π が type-0 安全であるとする．
M∼= N ならば [[M ]]Π ≈ [[N ]]Π である．
二つのプロトコル実行を表す項の間の記号的等価性を示しさえすれば，定理 1 より，計算論的手法における受動的攻撃者のもとでの計算量的安全性（プロトコル実行の間の計算量的識別不能性）が導かれる．

能動的攻撃者のもとでの計算論的健全性

3

次に，能動的攻撃者（メッセージの改竄や順序の入れ替えもできる攻撃者）を考える．Cortierと Warinschi の研究 [5] に基づき，公開鍵暗号の場合について述べる．

3.1

記号モデル

記号モデルでは項として，i 番目の参加者の名前 ai ，ai の公開鍵 pk(ai ) と秘密鍵 sk(ai )，ノンス nj ，鍵 pk(ai ) による t の暗号文 {t}lpk(ai )を扱う．ラベル l は，同じ平文と鍵による暗号文の区別に用いる．
自然数から実数への関数 ε が，∀c > 0 ∃N ∀η ≥ Nε(η) ≤ η −c を満たすとき，ε が無視できるという．
1En−1

0
H0 −−→
H1 · · · −−−→ Hn で記号トレースを定義する．秘密鍵を含むメッセージを参加者が送信しないようなプロトコル Π を考える．Π
を実行した記号トレース全体の集合を Exe sΠ と書く．

3.2

計算論的モデル

計算論的モデルでも，攻撃者の動作 new とsend を扱うが，項の代わりにビット列を扱う．
攻撃者は，受信ビット列の集合 H から PPT 計算可能なビット列を送信する．受信ビット列集
合と攻撃者の動作の列で計算論的トレースを定義する．PPT 攻撃者 A のもとでプロトコル Πを実行した計算論的トレースは，ノンスと鍵の生成や暗号化の乱数により確率的に定まる．セキュリティ・パラメータ η に対し，計算論的トレースの確率分布を Exe cΠ,A (η) で表す．

3.3マッピング補題と計算論的健全性マッピング補題（mapping lemma）は，計算論的トレースに対して記号トレースが対応しない確率が無視できるという性質である．ビット列集合から項集合への部分関数 c に対し，計算論的トレース tr c に現れる各ビット列 m を c(m)で置き換えたものを c(tr c ) と書く．単射な部分関数 c が存在し，c(tr c ) が記号トレース tr s であるとき，tr s ⪯ tr c と書く．
補題 2 公開鍵暗号が IND-CCA2 安全2 のとき，任意の PPT 攻撃者 A に対し，次が無視できる．

Pr tr c ← Exe cΠ,A (η) : ∀tr s ∈ Exe sΠ tr s ̸⪯ tr c
プロトコル Π の安全性を，望ましいトレースの集合で表す．Π が記号トレースの集合 P s で表される安全性を満たすことを Exe sΠ ⊆ P s で定2

能動的攻撃者のもとでの安全性定義のひとつ

義する．Π が計算論的トレースの集合 P c で表される安全性を満たすことを任意の PPT アルゴ
リズム A に対し，Pr tr c ← Exe cΠ,A (η) : tr c ̸∈ P sが無視できることとする．P s が P c に対応する（c−1 (P s ) ⊆ P c である）とき，補題 2 から次が導かれる．
定理 3 Π が記号モデルで安全性 P s を満たすならば，Π は計算論的モデルで安全性 P c を満たす．
つまり，記号モデルで Π の安全性を示せば，定理 3 により，Π の計算論的実行の安全性が導かれる．
同様の考え方で，汎用的結合可能性での安全性が記号的安全性から導かれることが示されている [2]．

4

その後の計算論的健全性の研究

匿名性のように，等価性で表せてもトレース集合で表せない安全性は，定理 3 を適用できない．能動的攻撃者のもとでの等価性の計算論的健全性は，2.3 項の等価性の健全性と 3.3項のマッピング補題を発展させた議論で導かれる [3, 4]．

参考文献
[1] M. Abadi and P. Rogaway. Reconciling two views of cryptography (thecomputational soundness of formal encryption). Journal of Cryptology, 15(2),pp.103 – 127, 2002.
[2] R. Canetti and J. Herzog. Universallycomposable symbolic analysis of mutual authentication and key-exchange
protocols. In Proc. TCC’06, Springer
Lecture Notes in Computer Science,Vol. 3876, pp.380–403, 2008.
[3] H. Comon-Lundh and V. Cortier. Computational soundness of observationalequivalence. In Proc. ACM CCS’08,pp.109–118, 2008.
[4] H. Comon-Lundh, M. Hagiya, Y.
Kawamoto and H. Sakurada. Computational soundness of indistinguishability properties without computableparsing. In Proc. ISPEC’12, Springer
Lecture Notes in Computer Science,Vol. 7232, pp.63–79, 2012.

[5] V. Cortier and B. Warinschi. Computationally sound, automated proofs forsecurity protocols. In Proc. ESOP’05,
Springer Lecture Notes in Computer
Science, Vol. 3444, pp.157–171, 2005.