Dolev-Yao攻撃者モデルと記号暗号

1983年にDanny DolevとAndrew Yaoによって提案されたDolev-Yaoモデルは、記号プロトコル解析における標準的な攻撃者モデルです。攻撃者はネットワーク全体を制御します。

Dolev-Yao攻撃者は、任意のメッセージを傍受し、メッセージを保存し、古いメッセージをリプレイし、既知の構成要素から新しいメッセージを偽造できます。ただし、基盤となる暗号プリミティブを破ることはできません。

記号モデルでは、暗号化は完全なブラックボックスとして扱われます。攻撃者は鍵なしでは復号できず、大きな数を素因数分解できず、署名を偽造することもできません。この仮定によって解析は簡単になりますが、実装レベルの攻撃を見落とす可能性があります。

メッセージは項としてモデル化されます。enc(k, m)、sig(sk, m)、hash(m)、pair(a, b)などです。攻撃者は特定の項を知っており、定義された規則（推論規則）を使って新しい項を導出します。

攻撃者の知識は推論に関して閉じています。攻撃者が enc(k,m) と k を知っていれば、m を導出できます。pair(a,b) を知っていれば、a と b を導出できます。初期知識の閉包とは、攻撃者が学習できるすべての情報です。

プロトコルのセキュリティは、「到達可能な任意の状態において、攻撃者の知識に秘密 s が含まれることはない」と表現されます。秘匿性は到達可能性として捉えられます。認証は、特定の不正なトレースパターンが存在しないこととして表現されます。

2者間プロトコル：A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}。項代数では、Alice が enc(pubkey_B, pair(Na, A)) を送信すると表現します。実行後に Na を知っているのが B だけであることを検証します。

Applied Pi Calculus（応用π計算）は、Abadi と Fournet が 2001 年に提案した、プロトコルをモデル化するためのプロセス代数です。プロセスはチャネルを介して通信し、攻撃者は公開チャネルを制御します。ProVerif と Tamarin はこの形式体系を使用します。

Dolev-Yao モデルで安全なプロトコルでも、暗号の実装が弱ければ計算論的には安全でない可能性があります。計算論的健全性定理（Cortier ら）は、特定の暗号プリミティブのクラスについて、この隔たりを橋渡しします。

Dolev-Yao モデルでは、代数的性質（XOR の可換性など）、サイドチャネル攻撃、実装上のバグ、確率的な失敗をモデル化できません。等式理論モデルなどの拡張を使えば、一部の代数的性質を扱えます。

Dolev-Yao 攻撃者が持たない能力はどれですか。

Dolev-Yao モデルでは、攻撃者がネットワークを完全に制御できる一方、暗号は完全であると仮定します。メッセージは代数上の項として扱われ、セキュリティは到達可能性の特性として表現されます。Applied Pi Calculus は形式言語を提供します。限界として、代数的関係、サイドチャネル、実装上のバグをモデル化できません。