Dolev-Yao モデル

Dolev -Yaoモデル^[1]は、その作者であるDanny DolevとAndrew Yaoにちなんで名付けられ、対話型暗号プロトコルの特性を証明するために使用される形式モデルです。 ^{[2] [3]}

ネットワークは、メッセージを交換できる一連の抽象マシンによって表されます。これらのメッセージは、形式的な用語で構成されています。これらの用語は、メッセージの内部構造の一部を明らかにしますが、一部の部分は敵対者にとって不透明なままであることが期待されます。

このモデルでは、攻撃者はあらゆるメッセージを盗聴、傍受、合成することができ、使用される暗号化方法の制約によってのみ制限されます。言い換えれば、「攻撃者がメッセージを運ぶ」ということです。

この全能性をモデル化することは非常に困難であり、多くの脅威モデルでは、ユビキタスコンピューティングにおける攻撃者の場合のように、これを単純化しています。^[4]

暗号プリミティブは、抽象演算子によってモデル化されます。たとえば、ユーザーに対する非対称暗号化は、暗号化関数と復号化関数によって表されます。これらの主な特性は、それらの構成が恒等関数( ) であり、暗号化されたメッセージはについて何も明らかにしないことです。現実世界とは異なり、攻撃者は暗号化のビット表現を操作することも、キーを推測することもできません。ただし、攻撃者は送信済みのメッセージを再利用して既知になる場合があります。攻撃者は、自分が知っている任意のキーを使用してこれらのメッセージを暗号化または復号化し、後続のメッセージを偽造できます。 ${\displaystyle x}$${\displaystyle E_{x}}$${\displaystyle D_{x}}$${\displaystyle D_{x}E_{x}=E_{x}D_{x}=1}$${\displaystyle E_{x}(M)}$${\displaystyle M}$

プロトコルは、クエリ (ネットワーク経由でメッセージを送信する) と応答 (ネットワークからメッセージを取得する) を交互に実行する一連の連続実行としてモデル化されます。

Dolev-Yaoモデルの記号的な性質により、計算モデルよりも扱いやすく、代数的手法にもアクセスしやすいものの、現実的ではない可能性があります。しかし、暗号プロトコルの両種類のモデルは関連しています。^[5]また、記号モデルは、攻撃者の能力に関する与えられた仮定の下で、プロトコルが安全ではなく、 破られていることを示すのに非常に適しています。

• 安全
• 暗号化プロトコル