Isabelle Tutorial その27

ついに最終章です。

10. Case Study: Verifying a Security Protocol

最後の章は、セキュリティプロトコルをモデル化し、その正しさを証明します。Needham-Schroeder公開鍵プロトコルを例として、Isabelleを使ったプロトコルの検証方法を見ていきます。

10.1 The Needham-Schroeder Public-Key Protocol

このプロトコルは公開鍵暗号を使用します。アリスがボブにメッセージを送るにはボブの公開鍵で暗号化し、ボブの持っている秘密鍵のみがこの暗号文を正しく復号することができます。

Needham-Schroederプロトコルには三つの重要なメッセージがあります。

$1. A \rightarrow B : \{|Na, A|\}_{Kb}$
$2. B \rightarrow A : \{|Na, Nb|\}_{Ka}$
$3. A \rightarrow B : \{|Nb|\}_{Kb}$

最初のメッセージは、アリスが作成したノンス(Na)とアリスの名前(A)を、ボブの公開鍵(Kb)で暗号化したメッセージをアリスからボブへ送信することを意味します。二つ目はNaとボブが作成したノンス(Nb)をアリスの公開鍵(Ka)で暗号化したメッセージをボブからアリスへ送信することを意味します。最後はアリスからボブへ、Nbをボブの公開鍵で暗号化し送信することを意味します。

最初のメッセージを復号しNaを取り出せるのはボブのみなので、二つ目のメッセージによってアリスはボブが最初のメッセージを受け取り返信してきたことを確認できます。同様に、三つ目のメッセージによってボブはメッセージを送ったのがアリスであることを確認します。このプロトコルが、NaとNbをアリスとボブのみが共有することを保証すると思われていました。しかし、これが間違いであることをLoweが発見しました。もしアリスが他のエージェント(チャーリーとします)に対して通信を始めると、チャーリーはボブのふりをすることができます。

$1. A \rightarrow C : \{|Na, A|\}_{Kc}$
　　　　 $1'. C \rightarrow B : \{|Na, A|\}_{Kb}$
$2. B \rightarrow A : \{|Na, Nb|\}_{Ka}$
$3. A \rightarrow C : \{|Nb|\}_{Kc}$
　　　　 $3'. C \rightarrow B : \{|Nb|\}_{Kb}$

メッセージ1と3において、チャーリーはアリスからのメッセージを復号し、ボブの公開鍵で暗号化し直してからボブへ送信しています。これによってボブは通信相手がアリスであると思い込み、ノンスが漏れていることには気付きません。これが、マン・イン・ザ・ミドルと呼ばれる攻撃方法の典型的なパターンです。

Loweはまたこの問題に対する対策も提案しています。それは、メッセージ2にボブの名前を入れることです。

$1. A \rightarrow B : \{|Na, A|\}_{Kb}$
$2. B \rightarrow A : \{|Na, Nb, B|\}_{Ka}$
$3. A \rightarrow B : \{|Nb|\}_{Kb}$

もしチャーリーが同じように攻撃しても、アリスは $\{|Na, Nb, C|\}_{Ka}$ を受け取るはずが $\{|Na, Nb, B|\}_{Ka}$ を受け取ることになり、攻撃されていることに気付くことができます。以下では、このプロトコルの正しさを証明していきます。

Loweはこのような攻撃手段があることをモデル検査器を使用して見つけられることを示しました。以下で見るように、プロトコルの正しさを証明で確かめることもできます。無限の状態を扱うことができるため、証明の方がよりパワフルです。まずシステムの操作的意味を形式的に表し、その性質を帰納的に証明していきます。

10.2 Agents and Messages

データ型agentは定数Server、Friend、そしてSpyを定義します。Friendは複数いる可能性があるので、引数にnatを取ります。

datatype agent = Server | Friend nat | Spy

鍵は自然数で表わします。関数invKeyは公開鍵から秘密鍵へ、またはその逆へのマップ関数です。

types key = nat
consts invKey :: "key => key"

データ型msgはメッセージの形を定義します。メッセージはエージェント名、ノンス、鍵、及びそれらの暗号化と合成から成ります。

datatype msg = Agent agent |
               Nonce nat |
               Key key |
               MPair msg msg |
               Crypt key msg

{|X₁, ..., X_n-1, X_n|}はMPair X₁ ...(MPair X_n-1 X_n)の略記とします。

データ型の構成子は単射であることから、次の定理が得られます。

lemma "Crypt ka xa = Crypt kb xb ==> ka = kb & xa = xb"

暗号文を復号できる鍵は唯一であり、得られる平文も唯一です。現実には誤った鍵を使用して復号することもできますが、このモデルでは例えばチェックサムなどを使用して、間違った鍵による復号であることがわかると仮定します。

10.3 Modelling the Adversary

スパイもシステムの一部であり、モデルに含めなければなりません。スパイはネットワークを見張り、持っている鍵でメッセージを復号しようとします。そのために鍵とノンスを集め、新たなメッセージを作り、送信します。

二つの関数analzとsynthがこの振る舞いを形式化します。analz Hはスパイがメッセージの集合Hから得られる情報を表わします。

inductive_set
  analz :: "msg set => msg set"
  for H :: "msg set"
where
Inj [intro, simp]: "X : H ==> X : analz H" |
Fst:               "{|X, Y|} : analz H ==> X : analz H" |
Snd:               "{|X, Y|} : analz H ==> Y : analz H" |
Decrypt [dest]:    "[|Crypt K X : analz H; Key (invKey K) : analz H|] ==> X : analz H"

Decryptルールは、スパイが自分の持っている鍵のみで復号できることを示しています。規則帰納を用いて次の定理を証明することができます。

"G <= H ==> analz G <= analz H"　　　　(analz_mono)
"analz (analz H) = analz H"　　　　　　(analz_idem)

synth Hはメッセージの集合Hから作ることのできるメッセージの集合を表わします。よってスパイがHから偽造できるメッセージをsynth (analz H)で表わすことができます。

inductive_set
  synth :: "msg set => msg set"
  for H :: "msg set"
where
Inj [intro]:   "X : H ==> X : synth H" |
Agent [intro]: "Agent agent : synth H" |
MPair [intro]: "[|X : synth H; Y : synth H|] ==> {|X, Y|} : synth H" |
Crypt [intro]: "[|X : synth H; Key K : synth H|] ==> Crypt K X : synth H"

この集合にはすべてのエージェント名が含まれています。対して、鍵やノンスは推測できないと仮定しているので、Hに含まれていない限り使うことはできません。

analzと同様にsynthも単調性を持ち、冪等律を満たします。さらに、次の定理も満たします。

"analz (synth H) = analz H Un synth H"　　　　(analz_synth)

次の例のように規則の反転を使用することで、synthに関する証明がしやすくなります。

inductive_cases Nonce_synth [elim!]: "Nonce n : synth H"

三つ目の演算子partsは正当性を表わすのに便利です。parts HはHに含まれるメッセージに含まれるすべての要素を表わします。定義はanalzに似ていますが、Cryptに対応する規則のみが異なります。

Crypt K X : parts H ==> X : parts H

partsを使って例えば、信頼できるエージェントの秘密鍵はどのメッセージにも含まれないといった、プロトコルに関する整礎な性質を表わすことができます。

10.4 Event Traces

システムの振る舞いはイベントトレースの集合で形式化します。最も重要なイベントSays A B XはAからBへXを送信することを表わします。トレースは単にイベントの列です。他のイベントには、メッセージの受信や情報の記憶などがあります。

通信の中で、新たなノンスを生成しなければなりません。これを形式化するために、used evsはトレースevsに含まれるすべての要素の集合とします。この関数は帰納的に定義でき、例えばイベントSaysの場合は次のようになります。

used (Says A B X # evs) = parts {X} Un used evs

関数knowsはエージェントの知識を形式化します。多くの場合はスパイの持っている知識を考慮すればよく、knows Spy evsはトレースevsからスパイが得られる情報の集合を表わします。イベントSaysに対して、スパイは送信されたメッセージを記憶します。

knows Spy (Says A B X # evs) = insert X (Knows Spy evs)

次のように、関数を組み合わせて他のメッセージ集合を表わすことができます。

analz (knows Spy evs)はevsから復号によってスパイが得られるすべてのメッセージを表わします。
synth (analz (knows Spy evs))はスパイが生成できるすべてのメッセージを表わします。

関数pubKはエージェントからその公開鍵への関数です。関数priKはエージェントからその秘密鍵への関数です。

consts pubK :: "agent => key"
abbreviation priK :: "agent => key"
where "priK x == invKey (pubK x)"

集合badは秘密鍵をスパイに知られているエージェントの集合とします。

公開鍵に関する二つの公理、異なるエージェントが同じ公開鍵を持つことはない、そして秘密鍵が公開鍵とは異なることを定義します。

axioms
  inj_pubK:      "inj pubK"
  priK_neq_pubK: "priK A ~= pubK B"

10.5 Modelling the Protocol

Loweによって修正されたNeedham-Schroeder公開鍵プロトコルを形式化します。プロトコルのそれぞれのステップは帰納的に定義されます。イベントトレースはevent list型とし、イベントトレースの集合ns_pubicを次のように帰納的に定義します。

inductive_set ns_public :: "event list set" where
Nil:  "[] : ns_public" |
Fake: "[|evsf : ns_public; X : synth (analz (knows Spy evsf))|]
       ==> Says Spy B X # evsf : ns_public" |
NS1:  "[|evs1 : ns_public; Nonce NA ~: used evs1|]
       ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) # evs1 : ns_public" |
NS2:  "[|evs2 : ns_public; Nonce NB ~: used evs2;
         Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2|]
       ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) # evs2 : ns_public" |
NS3:  "[|evs3 : ns_public;
         Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
         Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) set evs3|]
       ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"

ルールNilは空列が含まれることを定義します。Fakeは過去のメッセージを元に偽造したメッセージをスパイが送信できることを定義しています。最後の三つのルールはプロトコルが定義する正しいステップを表わしています。NS2において送信者がAではなくA'となっているのは、受信者Bはそのメッセージの送信者が誰であるか知らないためです。また、変数に単なるevsではなくevs1やevs2を使用しているのは、証明中のサブゴールを見やすくするためであり、本質的ではありません。

10.6 Proving Elementary Properties

機密性に関する典型的な例はX ~: analz (knows Spy evs)、つまりXがスパイに知られてはいないというものです。この証明はanalzについて解かなければならないことから、かなり困難です。これと比べると、Xがまったく現れないことの証明は簡単になります。この場合は、analzの代わりにpartsを使用します。

次の補題は、Aの秘密鍵がスパイに漏れる可能性があるのは、Aが集合badに含まれているとき、かつその時に限るということを表わしています。ここでpartsが使われているのは、暗号化されているかどうかに関わらず、Aの秘密鍵がメッセージに含まれているかという点にのみ注目しているからです。証明はプロトコルに関する他の証明と同様、メッセージトレースに関する帰納法を使用します。

lemma Spy_see_priK [simp]:
  "evs : ns_public
   ==> (Key (priK A) : parts (knows Spy evs)) = (A : bad)"
apply(erule ns_public.induct, simp_all)

帰納法によって五つのサブゴールに別れます。正当なメッセージに暗号鍵が含まれていないことは明らかであり、問題となるのはFakeのみです。単純化の結果次のサブゴールのみが残ります。

 1. !!evsf X.
      [|evsf : ns_public;
        (Key (priK A) : parts (knows Spy evsf)) = (A : bad);
        X : synth (analz (knows Spy evsf))|]
      ==> (Key (priK A) : parts (insert X (knows Spy evsf))) =
          (A : bad)

by blast

もしpriK AがXで拡張したトレースに含まれるならば、(1)元のトレースに含まれていたか、(2)スパイによって生成されたメッセージに含まれていたかのどちらかであり、どちらの場合も前提から証明することが可能です。

単一性は特定の要素がトレースの中に一度だけ現れることを示します。次の補題は、スパイに知られない限り、ノンスの値は唯一であることを示しています。証明は帰納法、単純化、そしてblastのみで可能です。最初にrev_mpを使用するのは、メタ前提に含まれる二つの仮定を含意の前提に移動して帰納法を適用するためです。

lemma no_nonce_NS1_NS2:
  "[|Crypt (pubK C) {|NA', Nonce NA, Agent D|} : parts (knows Spy evs);
     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (knows Spy evs);
     evs : ns_public|]
   ==> Nonce NA : analz (knows Spy evs)"
apply(erule rev_mp, erule rev_mp)
apply(erule ns_public.induct, simp_all)
apply(blast intro: analz_insertI)+
done

次の補題は、ノンスNAが漏れていないならば、NAを含むメッセージ1は唯一であることを表わしています。証明の手順は上と同様です。

lemma unique_NA:
  "[|Crypt (pubK B)  {|Nonce NA, Agent A |} : parts (knows Spy evs);
     Crypt (pubK B') {|Nonce NA, Agent A'|} : parts (knows Spy evs);
     Nonce NA ~: analz (knows Spy evs); evs : ns_public|]
   ==> A=A' & B=B'"

10.7 Proving Secrecy Theorems

元のプロトコルで問題となっていた、ボブに関する機密性の確認が特に重要となります。ボブとアリスの情報に漏洩がないならば、ボブがアリスへメッセージ2を送ってもボブのノンスがスパイに漏れることはないことを示します。

theorem Spy_not_see_NB [dest]:
  "[|Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) : set evs;
    A ~: bad; B ~: bad; evs : ns_public|]
   ==> Nonce NB ~: analz (knows Spy evs)"

適用できる形に変形してから帰納法を適用し、単純化します。

apply(erule rev_mp, erule ns_public.induct, simp_all)

メッセージ1に関するサブゴールのみを詳細に見てみます。

 1. !!evs1 NAa Ba.
       [|A ~: bad; B ~: bad; evs1 : ns_public;
         Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
         : set evs1 -->
         Nonce NB ~: analz (knows Spy evs1);
         Nonce NAa ~: used evs1|]
       ==> Ba : bad -->
           Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
           : set evs1 -->
           NB ~= NAa

単純化の中で次の場合分けルールが使われています。これは、復号のための鍵を持っているかどうかで場合分けします。

analz (insert (Crypt K X) H) =
(if Key (invKey K) : analz H
 then insert (Crypt K X) (analz (insert X H))
 else insert (Crypt K X) (analz H))　　　　　　　　　(analz_Crypt_if)

このサブゴールは、最後のメッセージが次のようだった場合を考えています。

$1. A' \rightarrow B' : \{|Na', A'|\}_{Kb'}$

このメッセージによってNbが漏れるのは、Nb = Na'かつB'の秘密鍵が漏れている場合です。サブゴールの中では変数名としてNB、NAa、Baが使われています。Nb ~= Na'を証明するのは簡単です。前提Nonce NAa ~: used evs1からNAaが新しいノンスであり、既に使われているNBと異なることが導けます。

エージェントは同時に複数のエージェントと通信しなければならず、その同時に進行する通信の狭間に攻撃されることがよくあります。これがモデル検査においては状態爆発の原因となり、証明においては複雑さの原因となります。特にメッセージ2は多くの場合分けが必要になります。しかし今回の証明では、補題no_nonce_NS1_NS2とメソッドblastによってすべてのサブゴールが証明できます。

残りの定理の証明はそれほど難しくはありません。次は真正性、すなわちBがAにメッセージ2を送信し、その返事が返ってきたならば、確かにAからの応答であることを証明します。

theorem B_trust_NS3:
 "[|Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) : set evs;
    Says A' B (Crypt (pubK B) (Nonce NB)) : set evs;
    A ~: bad; B ~: bad; evs : ns_public|]
  ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"

これも帰納法によって証明できます。

同様の前提から、AがノンスNAを使ってメッセージ1を送信したことも証明できます。この定理では、結論は次のようになります。

Says A B (Crypt (pubK B) {|Nonce NA, agent A|}) : set evs

ノンスNAの機密性と、メッセージ2を送信したのが確かにBであることも同様に証明できます。

この章での説明は以上です。現実のプロトコルは上で見た例より長く複雑ですが、プロトコル検証の流れは理解できたと思います。更なる詳細は参考文献*1 *2を参照してください。また、証明の全容はIsabelleのインストールディレクトリのsrc/HOL/Authを参照してください。

*1:Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.

*2:Lawrence C. Paulson. Inductive analysis of the Internet protocol TLS. ACM Transactions on Information and System Security, 2(3):332–351, August 1999.