バロウズ・アバディ・ニーダム論理

Burrows-Abadi-Needham ロジック( BAN ロジックとも呼ばれる) は、情報交換プロトコルを定義および分析するための一連のルールです。具体的には、BAN ロジックは、交換された情報が信頼できるか、盗聴から保護されているか、またはその両方であるかをユーザーが判断するのに役立ちます。BAN ロジックは、すべての情報交換が改ざんや公開監視に対して脆弱なメディア上で行われるという前提から始まります。これは、「ネットワークを信頼するな」という人気のセキュリティ マントラに発展しました。

典型的なBANロジックシーケンスには3つのステップが含まれます。^[1]

1. メッセージの発信元の検証
2. メッセージの鮮度検証
3. 発信元の信頼性の検証。

BAN ロジックは、すべての公理系と同様に、公理と定義を使用して認証プロトコルを分析します。BAN ロジックの使用は、プロトコルのセキュリティ プロトコル表記法の定式化を伴うことが多く、論文で紹介されることもあります。

BAN論理および同族の論理は決定可能である。つまり、BAN仮説と想定される結論を取り、その結論が仮説から導き出せるかどうかを答えるアルゴリズムが存在する。提案されたアルゴリズムはマジックセットの変種を使用する。^[2]

BAN ロジックは、GNY ロジックなど、他の多くの類似の形式主義に影響を与えました。これらのいくつかは、BAN ロジックの 1 つの弱点、つまり知識と可能な宇宙の観点から明確な意味を持つ優れたセマンティクスの欠如を修正しようとしています。しかし、1990 年代半ばから、暗号プロトコルはモデル チェッカーを使用して運用モデル (完全な暗号を想定) で分析され、BAN ロジックと関連する形式主義で「検証」されたプロトコルで多数のバグが見つかりました。^{[引用が必要]}場合によっては、プロトコルは BAN 分析によって安全であると推論されましたが、実際には安全ではありませんでした。^[3]これにより、BAN ファミリー ロジックは放棄され、標準的な不変性推論に基づく証明方法が採用されました。^{[引用が必要]}

定義とその意味は以下の通りです（PとQはネットワークエージェント、Xはメッセージ、K は暗号化キーです）。

• P はX を信じます。PはX が真実であるかのように行動し、他のメッセージでX を主張する場合があります。
• P はXに対して管轄権を持っています。Xに関するP の信念は信頼されるべきです。
• P はXを言いました: ある時点で、P はメッセージXを送信し (そして信じました) 、しかし、P はもはやX を信じていない可能性があります。
• P はX を見ます: P はメッセージXを受信し、X を読んで繰り返すことができます。
• { X } _K : XはキーKで暗号化されます。
• fresh( X ): Xはこれまでどのメッセージでも送信されていません。
• key( K , P ↔ Q ): PとQは共有キーKで通信できる

これらの定義の意味は、一連の仮定で表されます。

• Pがキー( K , P ↔ Q )を信じ、Pが{ X } _Kを見た場合、Pは( QはXを言った)を信じる。
• Pが（QはXを言った）を信じ、Pが（X ）を信じているなら、Pは（QはXを信じている）を信じている。

P は、ここでXが新しいものであると確信する必要があります。X が新しいものであることが不明な場合は、攻撃者によって再生された古いメッセージである可能性があります。

• Pが（ QはXに対して管轄権を持っている）と信じ、 Pが（QはXを信じている）と信じている場合、PはXを信じている。
• メッセージの構成に関係する他の技術的な公理がいくつかあります。たとえば、P がQ が⟨ X、Y ⟩ ( XとYの連結)を言ったと信じている場合、P はQ がX を言ったとも信じ、QがY を言ったとも信じます。

この表記法を使用すると、認証プロトコルの背後にある仮定を形式化できます。この仮定を使用すると、特定のエージェントが特定のキーを使用して通信できると信じていることを証明できます。証明が失敗した場合、通常、失敗のポイントはプロトコルを侵害する攻撃を示唆します。

非常にシンプルなプロトコルであるWide Mouth Frog プロトコルを使用すると、信頼できる認証サーバー S と同期されたクロックを使用して、 2 つのエージェントAとB が安全な通信を確立できます。標準表記法を使用すると、プロトコルは次のように指定できます。

A → S : A _、 { TA、KAB、B } _KAS​​

S → B : { T _S、K _AB、 A } _{K BS}

エージェント A と B は、S と安全に通信するための鍵K _ASとK _BSをそれぞれ 備えています。したがって、次の仮定が成り立ちます。

Aはキー( K _AS、A ↔ S )を信じる

Sは鍵( K _AS、A ↔ S )を信じる

Bは鍵( K _BS、B ↔ S )を信じる

Sは鍵( K _BS , B ↔ S )を信じる

エージェントA はBとの安全な会話を開始したいと考えています。そのため、 Bとの通信に使用するキーK _{AB を}作成します。 A は、このキーを自分で作成したため、このキーが安全であると信じています。

Aはキー( K _AB、A ↔ B )を信じる

B は、このキーがAから来たものであると確信している限り、このキーを受け入れる用意があります。

Bは（Aは鍵（K、A↔B）に対する管轄権を持っている）と信じている

さらに、BはS がAからの鍵を正確に中継することを信頼しています。

Bは（ Sは（ Aは鍵（K、A↔B）を信じている）に対する管轄権を持っている）と信じている

つまり、A が特定のキーを使用してBと通信したいと考えていることをSが信じていることをB が信じている場合、B はS を信頼し、それを信じることになります。

目標は

Bはキー( K _AB、A ↔ B )を信じる

A は時計を読み取り、現在の時刻tを取得し、次のメッセージを送信します。

1 A → S : { t ,キー₍ KAB _, A↔B ) } _KAS

つまり、選択したセッション キーと現在の時刻を、秘密認証サーバー キーK _ASで暗号化してSに送信します。

S はkey( K _AS、A ↔ S )を信じており、{ t 、 key( K _AB、A ↔ B )} _{K AS}を見ているので、SはAが実際に{ t、 key( K _AB、A ↔ B )}と言ったと結論付けます。 (特に、S はメッセージが何らかの攻撃者によって捏造されたものではないと信じています。)

時計は同期しているので、

Sは新鮮だと信じている( t )

S はfresh( t ) を信じ、Aが{ t、 key( K _AB、A ↔ B )}と言ったと信じているため、S はAが実際にkey( K _AB、A ↔ B )を信じていると信じます。 (特に、S は、メッセージが過去のある時点でそれをキャプチャした攻撃者によって再生されていないと信じています。)

次に、 S はキーをBに転送します。

2 S → B : { t、A、A はキー( K _AB、A ↔ B ) を信じる} _{K BS}

メッセージ 2 はK _BSで暗号化されており、B はkey( K _BS、B ↔ S )を信じているため、B はS が{ t、A、Aは key( K _AB、A ↔ B ) を信じている}と発言したと信じるようになります。 クロックは同期されているため、B はfresh( t ) を信じ、したがって fresh( A はkey( K _AB、A ↔ B ) を信じている) となります。B はSの発言が最新であると信じているため、B はS が( A はkey( K _AB 、 A ↔ B )を信じている) と信じていると信じているため、 B は ( A はkey( K AB 、A ↔ B )を信じている) と信じています。B はSがA の信じていることについて権威を持っていると信じているため、B は( A はkey( K _AB、A ↔ B )を信じている) と信じています。 B はA がAとB間のセッション キーについて権威を持っていると信じているため、B はkey( K _AB、A ↔ B )を信じています。 B はK _{AB を}秘密セッション キーとして 使用して、 Aに直接連絡できるようになりました。

ここで、クロックが同期しているという仮定を放棄すると仮定しましょう。その場合、S はAから{ t、 key( K _AB、A ↔ B )}を含むメッセージ 1 を受け取りますが、tが新しいとはもはや結論付けることができません。S は、A がこのメッセージを過去のある時点で送信したことは知っていますが ( K _ASで暗号化されているため)、これが最近のメッセージであることは知らないため、 S はA が必ずしもキーK _{AB を}使い続けたいとは考えません。これは、プロトコルへの攻撃を直接示しています。メッセージをキャプチャできる攻撃者は、古いセッション キーの 1 つK _{AB を}推測できます(これには長い時間がかかる場合があります)。次に、攻撃者は古い{ t、 key( K _AB、A ↔ B )}メッセージを再生し、 Sに送信します。クロックが同期していない場合 (おそらく同じ攻撃の一部として)、S はこの古いメッセージを信じて、B に古い侵害されたキーをもう一度使用するように要求する可能性があります。

オリジナルの「Logic of Authentication」論文 (下記リンク) には、この例と、Kerberosハンドシェイク プロトコルの分析、Andrew Project RPC ハンドシェイクの 2 つのバージョン (そのうちの 1 つは欠陥があります) など、他の多くの例が含まれています。

• Burrows, Michael ; Abadi, Martín ; Needham, Roger (1989). 「認証の論理」. Proceedings of the Royal Society of London, Series A . 426 (1871): 233. Bibcode :1989RSPSA.426..233B. CiteSeerX  10.1.1.115.3569 . doi :10.1098/rspa.1989.0125. S2CID  6937380.
• 出典: バロウズ・アバディ・ニーダムの論理