Needham-Schroederプロトコルと攻撃

Needham-Schroederプロトコル（1978年）は、信頼できる第三者機関（TTP）を使用して暗号学的認証プロトコルを設計しようとした、最初期の正式な試みの1つです。目的は、長期鍵を各プリンシパルと共有する信頼できるAuthentication Server（AS）を使って、2者であるAliceとBobが相互に認証し、共有セッション鍵を確立できるようにすることでした。このプロトコルは公開鍵基盤よりも前に登場しましたが、鮮度を保証するノンスや、信頼できるサーバーを介した鍵配送といった概念を導入し、これらはKerberosなど現代のプロトコルでも中心的な役割を果たしています。NSとその失敗について理解することは、プロトコル解析という分野全体の形成につながりました。

NS対称鍵プロトコルは5つの手順で進みます。(1) Aliceは、Bobとの通信に使用するセッション鍵を要求するため、{A, B, Na}をASに送信します。(2) ASはAliceに、{Na, B, Kab, {Kab, A}_Kb}_Kaを返します。これはセッション鍵Kab、Bob宛てのチケット、およびそれらをすべてAliceの長期鍵Kaで暗号化したものです。(3) Aliceはチケット{Kab, A}_KbをBobに転送します。(4) Bobはチケットを復号してKabを取り出し、チャレンジとして{Nb}_KabをAliceに送信します。(5) Aliceは{Nb-1}_Kabを返し、Kabを保持していることを証明します。ノンスNbによって手順4のリプレイを防ぎます。このプロトコルには、DenningとSacco（1981）が示した既知のリプレイ攻撃に対する脆弱性があります。

DenningとSacco（1981）は、次の欠陥を発見しました。手順2のASの応答は新しいものではなく、サーバーが提供するタイムスタンプやノンスを含んでいません。過去のセッションを侵害して古いセッション鍵Kabを以前に傍受していた攻撃者Malloryは、古いチケット{Kab, A}_Kbを将来の任意の時点でBobにリプレイできます。Bobは、Aliceから正規に送られたように見えるチケットを受け取ると、侵害された鍵Kabをそのセッションで使用します。DenningとSaccoによる修正では、ASの応答とチケットにタイムスタンプを追加します。これはKerberosに採用され、チケットにタイムスタンプを埋め込んで有効期間を制限する方式になっています。

NS公開鍵プロトコル（同じく1978年）は、公開鍵暗号を使用して2者間の相互認証を行うために設計されました。(1) Aliceは、Bobの公開鍵で暗号化したノンスNaを含む{Na, A}_PKbをBobに送信します。(2) Bobは、Aliceの公開鍵で暗号化した2つのノンス{Na, Nb}_PKaを返します。(3) Aliceは、BobのノンスをBobの公開鍵で暗号化した{Nb}_PKbを返します。この交換の後、両者は両方のノンス（Na、Nb）を保持し、セッション鍵を導出できます。このプロトコルは17年間安全だと考えられていましたが、Loweによる1995年の攻撃が発見されました。

Gavin Lowe（1995）は、Failures in Compositional Reasoning（FDR）モデルチェッカーを使用して重大な欠陥を発見しました。Malloryは、正直なBobにメッセージを中継しながら、Aliceに対してBobになりすますことができます。手順1：Aliceは、Bobと通信していると思い、{Na, A}_PKmをMalloryに送信します。Malloryは{Na, A}_PKbをBobに転送します。手順2：Bobは{Na, Nb}_PKaを返します。Malloryはこれを復号してAlice向けに再暗号化します：{Na, Nb}_PKa。Aliceは復号してNbを取り出します。手順3：Aliceは、これがBobに送られると思い、{Nb}_PKmを送信します。Malloryは復号して{Nb}_PKbをBobに転送します。BobはAliceとの相互認証を完了したと信じますが、実際にはAliceはMalloryを認証しています。修正方法は、手順2でBobが自身の識別情報を含めることです：{Na, Nb, B}_PKa。

LoweによるNSPKプロトコルの修正は単純ですが、深い意味を持ちます。ステップ2でのBobの応答にはBobの識別情報Bを含め、{Na, Nb, B}_PKaとしなければなりません。これでAliceが応答を受け取ったとき、含まれている識別情報Bが、連絡しようとしていた相手と一致することを確認できます。Malloryは自身の応答を差し替えられません。Aliceの確認を通過する有効な{Na, Nb, M}_PKaを構成するには、MalloryはAliceの秘密鍵が必要になるためです。この教訓はNeedham-Abadi原則として一般化されています。認証メッセージでは、識別にコンテキストだけを頼るのではなく、送信者の識別情報を明示的に結び付けなければなりません。

LoweによるNSPKの欠陥の発見には、FDR (Failures-Divergences Refinement)モデル検査器が役立ちました。FDRは、攻撃者による介入を含む、プロトコルのあらゆる実行可能性を網羅的に探索します。これをきっかけに、形式的なプロトコル解析ツールの開発が進みました。応用π計算に基づくProverifは、無限セッションにおける認証性や秘匿性の性質を証明または反証できます。Tamarin Proverはマルチセット書き換えを使用し、TLS 1.3やSignalのような複雑なプロトコルにも対応しています。AVISPAとScytherも別のツールです。現在のプロトコル設計（TLS 1.3、Signal、Noise）では、配備前に形式検証が行われます。これはNS/Lowe事件が直接もたらした遺産です。

NS攻撃によって、認証の目標の違いが明確になりました。エンティティ認証とは、ある当事者が現在も有効であり、プロトコルに参加していることを証明することです（新鮮性が重要になります）。データ起源認証とは、特定のメッセージが特定の当事者によって作成されたことを証明することです（ライブネスを意味しない場合があります）。Loweの攻撃はエンティティ認証を破ります。AliceはBobとの認証を行っていると信じていますが、実際には、Bobへの中継を行っているMalloryと認証しています。現在のプロトコル仕様では、「このセッションの開始者として、AliceがBobに対して認証されている」のように、目標を正確に記述します。曖昧な目標は、非公式なレビューには通っても形式解析には失敗する、あいまいな仕様につながります。

NSに関連する攻撃には、リフレクション攻撃という別の種類もあります。MalloryがAliceからのメッセージをAlice自身に送り返す攻撃です。プロトコルが対称的で、両当事者が同じ鍵とメッセージ形式を使用している場合、Aliceは自分自身のチャレンジをBobからの有効な応答として受け入れてしまう可能性があります。対策としては、鍵の方向を分ける（方向ごとに暗号化鍵と復号鍵を別々にする）か、メッセージに役割を示す情報を含めます（暗号化側がメッセージに "I am initiator" を含めるなど）。TLSのような現代のプロトコルでは、HKDFから導出する鍵に役割固有のラベル文字列（クライアントには "c e traffic"、サーバーには "s hs traffic"）を含め、リフレクションを防いでいます。

インターリービング攻撃は、複数の同時進行するプロトコルセッションのメッセージを組み合わせて、認証を偽造します。Aliceが2つのセッションを同時に実行している場合、Malloryは両方のメッセージを混在させ、一貫しているように見えるものの無効な統合セッションを作り、Mallory自身を認証させる可能性があります。対策はセッション結合です。各メッセージをセッションのコンテキストに暗号学的に結び付ける必要があります（たとえば、セッションIDを含めるか、セッションごとに一意の鍵を使用します）。TLSでは、現在のセッションの完全なトランスクリプトに対するMACであるFinishedメッセージによってインターリービングを防ぎます。インターリーブされたメッセージが1つでもあるとトランスクリプトが変わるため、Finishedの値が無効になります。

Needham-Schroederプロトコルは、Kerberos（リプレイを防ぐタイムスタンプ。Denning-Saccoの修正から取り入れられました）、TLS（FinishedのトランスクリプトMACによってインターリービングとリフレクションを防止）、Signal Protocol（ラチェット状態によるセッション結合）、Noise Protocol Framework（ハンドシェイクパターンにおける識別情報の結合）の設計に直接影響を与えました。NS攻撃は、非公式な安全性の議論だけでは不十分であることを示しました。すべてのプロトコルは、ネットワークを制御し、メッセージのリプレイ、並べ替え、変更を行える能動的な攻撃者に対して解析しなければなりません。この攻撃者モデル（Dolev-Yaoモデル）は、現在では形式的なプロトコル検証の標準となっています。

LoweがNS公開鍵プロトコルの脆弱性を修正するために提案した単純な変更は何ですか。

Needham-Schroeder対称鍵プロトコル（1978年）は、TTPベースのセッション鍵配布を導入しました。Denning-Sacco攻撃（1981年）によってリプレイの脆弱性が発見され、Kerberosではタイムスタンプによって修正されました。NSPK公開鍵プロトコルは、Loweがモデル検査によって発見したMITM攻撃（1995年）に対して脆弱であり、メッセージに送信者の識別情報を含めることで修正されました。これらの攻撃によって、形式検証（Proverif、Tamarin）がプロトコル設計に不可欠なものとなりました。重要な教訓は、メッセージで送信者の識別情報を結び付けること、セッションを互いに分離すること、方向別の鍵導出によってリフレクション攻撃を防ぐこと、トランスクリプトMACによってインターリービング攻撃を防ぐことです。