本記事の内容は安永憲司著『暗号理論入門』（森北出版）第2章に基づいています。
前回の記事
では完全模倣性を紹介しました。完全秘匿な暗号では、攻撃者Aは暗号文cを受け取って一生懸命計算しても、暗号文を知らないシミュレータSに完全に真似されてしまいます。つまり暗号文は攻撃者にとって全く役に立たないわけです。
では完全秘匿性が崩れたとき、攻撃者は暗号文をどう役立てることができるのでしょうか？今回はその具体的な方法と、攻撃の「有利さ」を定量的に示します。そして驚くべきことに、鍵が平文より1ビット短ければ暗号方式がどんなものであっても攻撃者は必ず5/8以上の勝率を得られることが示せます。
推測ゲーム
攻撃者の有利さを測る道具として推測ゲームを導入します。ゲームの手順は次の通りです。
- 攻撃者は二つの平文$m_0, m_1$を選ぶ
- bが{0,1}から一様ランダムに選ばれ、$m_b (つまりbに応じてm_0 あるいはm_1)$が暗号化されて暗号文cが作られる
- 攻撃者は$c$を受け取り、それを元にbを予想してb'を出力する
- b = b'ならば攻撃成功
Lean4では以下のように定義しています。
def guessingGame (Enc : K → M → C) (Gen : PMF K) (m0 m1 : M) (A : C → PMF Bool) : PMF Bool := do
let b ← PMF.bernoulli (1/2) (by norm_num)
let c ← Enc_dist Enc Gen (if b then m1 else m0)
let b' ← A c
PMF.pure (b' == b)
攻撃者AはC → PMF Boolという型を持ちます。暗号文を受け取ってBoolを確率的に出力する関数です。この定式化は前回の記事でも見ました。
さて、完全秘匿な暗号ではこのゲームの勝率はちょうど1/2です。Aは暗号文をみて何やら計算をしてb'を出力しますがbと一致する確率がちょうど1/2ということです。これはコインを投げてb'を決めているのと同じですから、暗号文cは何の役にも立っていません。このことを以下のようにlean 4の定理として述べることができます。
theorem success_prob_eq_half
(Enc : K → M → C) (Gen : PMF K)
(h_pi : perfect_indistinguishability Enc Gen)
(m0 m1 : M) (A : C → PMF Bool) :
(guessingGame Enc Gen m0 m1 A) true = 1/2
仮定にh_pi : perfect_indistinguishability Enc Genが入っていることからEnc Genの完全秘匿性が前提となります。その時任意の$m_0, m_1$および任意の攻撃者Aについて前述の推測ゲームでb=b'がtrueになる確率はちょうど1/2であると述べています。直感的に当然の結論ですが、この定理はlean4で30行程度で形式証明済みです。
攻撃者の戦略
では完全秘匿性が崩れたとき、必ず攻撃が成功するわけではないのですが、b=b'となる確率を1/2よりも大きくする方法があれば、攻撃者にとっては大成功です。
攻撃者はどう動けば攻撃が成功するのでしょうか？ここでは鍵空間のサイズが平文空間のサイズより小さいことで完全秘匿性が失われたとします。鍵を全部試して暗号文cから復号で到達できる平文の集合S(Enc, c)を考えます。m1がこの集合に含まれない、つまり「どの鍵を使ってもm1の暗号化結果がcにならない」ならば、暗号文cはm0を暗号化したものだと判断できます。その場合には確実にfalseと答えられます。残念ながらある鍵でm1の暗号結果がcになる場合には、この判定法は使えないので適当に答えることにします。lean 4で書くとこんな感じです。
def S (Enc : K → M → C) (c : C) : Finset M :=
Finset.univ.filter (fun m => ∃ k, Enc k m = c)def proposedAdversary (Enc : K → M → C) (_m0 m1 : M) (c : C) : PMF Bool :=
if m1 ∈ S Enc c then
PMF.bernoulli (1/2) (by norm_num)
else
PMF.pure false
面白いことに、この攻撃者はm0を全く使っていません（_m0のアンダースコアがそれを示しています）。m1がcから到達可能かどうかだけを判定しています。
勝率の計算
この攻撃者の勝率を計算すると、eを「m0を暗号化したときにm1がS(Enc, c)に含まれない確率」として次の精密な等式が成り立ちます。
$$勝率=\frac{1}{2} + \frac{e}{4}$$
この等式をlean 4の形式で定理として述べると以下のようになります。
theorem guessing_game_success_prob
(Enc : K → M → C) (Gen : PMF K) (m0 m1 : M) :
(guessingGame Enc Gen m0 m1 (proposedAdversary Enc m0 m1)) true
= 1/2 + (e Enc Gen m0 m1)/4
e = (e Enc Gen m0 m1)は必ず0以上なので、この攻撃者はどんな暗号に対しても勝率1/2以上を達成します。success_prob_eq_halfと比べると、結論のguessingGameの第５引数に、任意のAではなく、先ほど定義したproposedAdversaryが入っていることに注意してください。また完全秘匿性の仮定が前提から抜けています。ちなみにこの定理guessing_game_success_probに完全秘匿性を条件として付け加えると(e Enc Gen m0 m1)=0から勝利確率は1/2となります。つまり完全秘匿性を仮定すると攻撃者がproposedAdversaryでも推測ゲームの勝利確率は1/2のままです。
そしてメインの結果です。鍵が平文より1ビット短い（|K|×2 = |M|）場合、暗号方式の具体的なアルゴリズムにかかわらず、e ≥ 1/2となるm0, m1の組が必ず存在し、それを上記の定理guessing_game_success_probの結論に代入することで勝率5/8以上が達成できます。Lean4の定理を見ると、仮定はEncの単射性と鍵空間と平文空間のサイズ比だけで、暗号アルゴリズムの詳細は一切問われていません。
theorem guessing_game_five_eighths
(Enc : K → M → C) (Gen : PMF K)
(h_inj : ∀ k, Function.Injective (Enc k))
(h_card : Fintype.card K * 2 = Fintype.card M) :
∃ m0 m1, (guessingGame Enc Gen m0 m1 (proposedAdversary Enc m0 m1)) true ≥ 5/8
この状況ではproposedAdversaryは暗号文cを有効活用することで攻撃に成功していると言えます。
なぜe ≥ 1/2が言えるのでしょうか。Enc kが単射で|K|×2 = |M|のとき、ある暗号文cから復号で到達できる平文の個数は|K|個、平文全体の個数は|M|個なので、m1が到達できる確率は平均的に高々|K|/|M|=1/2です。平均論法により、到達確率が1/2以下になるm1が必ず存在する——これがeの下限の本質です。この辺も含めてlean 4で厳密に証明できています。ここは「なんとなくそうなりそう」で済ませたくなりますがlean 4を使うことで証明の厳密性を維持できました。
5/8という数字はシンプルですが、「鍵が1ビット短いだけで、どんな暗号方式であっても攻撃者が暗号文を確実に役立てられる」という事実を明確に示しています。そしてこれらの証明はすべてLean4で形式的に検証されています。詳細はリポジトリをご覧ください。GussingGameというフォルダを新設してコードをおきました。
