Vol. 45 No. 0  情報処理学会論文誌  2004

セキュリティプロトコルの略式記法から spi 計算への変換

住井英二郎^{†} 立沢秀晃^{††} 米澤明憲^{††}

セキュリティプロトコルは往々にして非形式的な略式記法で定義されるが、この記法は明確な意味論がなく、プロトコルが正常に完了する場合のメッセージ列しか記述していない。そのためにプロトコルが誤って解釈されたり、形式的検証の妨げとなるおそれがある。

我々はこの問題に対処するべく、略式記法の構文を形式化し、 Abadi と Gordon の spi 計算への半自動的な変換を定義する。 spi 計算は、暗号プロトコルの形式的記述・検証においてもっとも成功している枠組みの一つである。変換の基本方針は、プロトコルの各時点における各参加者の知識 (どのような鍵、ノンス、識別子を知っているか) にもとづき、各参加者の動作を明確化することである。

Translating Security Protocols from Informal Notation into Spi Calculus

Eijiro Sumii,^{†} Hideaki Tatsuzawa^{^{†}^{†}} and Akinori Yonezawa^{^{†}^{†}}

Security protocols are often defined in informal notations which have no clear semantics and only describe the message sequence when the protocol is successfully completed. This can be a source of incorrect interpretations of protocols as well as an obstacle to their formal verification.

To address this problem, we formalize the syntax of the informal notations and present their semi-automatic translation into Abadi and Gordon’s spi-calculus, one of the most successful frameworks for the formal specification and verification of cryptographic protocols. Our main idea is to make the actions of each principal explicit on the basis of its knowledge, i.e., what keys, nonces and names it knows at each point in a protocol.

1. 序論

セキュリティプロトコルとは、暗号を使用したメッセージのやりとりにより、相手の認証や秘密の伝達といった目的を達成するためのアルゴリズムである。セキュリティプロトコルはしばしば以下のような外見の記法（略式記法ということにする）によって定義される。

\begin{aligned}1. & B & → & A & : & N_{B} \\ 2. & A & → & B & : & \{N_{B}, B\}_{K_{AB}} \end{aligned}

これは ISO 対称鍵 2 パス一方向認証プロトコルという例である^{9)}。このプロトコルの目的は、参加者 (principal) B が参加者 A の生存を確認することにある。そのために、 B はまず一度だけ使用される適当な乱数であるノンス (nonce) N_{B} を新規に生成し、 A ; に送信する。 A はそれを受信し、 B の名前と一緒に共 ; 有鍵 K_{AB} で暗号化して、 B に返信する。 B はそれを ; K_{AB} で復号化し、受信したノンスが以前に生成した ; N_{B} と一致していること、また、受信した名前が B で ; あることを確認する。 ; しかし、以上のような動作を前述の略式記法だけか ; ら理解する方法は自明でない。というのは、略式記法 ; では ; • まず、 B が A にノンス N_{B} を送る ; • 次に、 A は B に暗号文 {N_{B}, B}_{K_{AB}} を送る ; という動作しか明示されておらず、 ; • 1. において、 B は N_{B} を新規に生成する ; • 2. において、 B は受信した N_{B} と B が本当に N_{B} ; と B であることを確認する ; という動作を推測しなければならないためである。こ ; のような問題があるために、略式記法は一見すると簡 ; 潔でわかりやすいにもかかわらず、プロトコルを記述 ; するための言語として実際の理論やシステムでは（非 ; 形式的な説明以外には）あまり使用されてこなかった。 ; けれども十分な経験のある人間ならば、自然言語に

† ペンシルバニア大学コンピュータ情報科学科

Department of Computer and Information Science, University of Pennsylvania †† 東京大学情報理工学系研究科コンピュータ科学専攻

Department of Computer Science, Graduate School of Information Science and Technology, University of Tokyo

2  情報処理学会論文誌  2004

よる記述がなくても略式記法だけからプロトコルの動作を推測することが可能である。これはまったくの直観だけによるわけではなく、ある程度の規則が存在すると想像される。たとえば、先の例の 2. において B が N_{B} と B を確認するのは、それらの値をすでに知っていて、特定のメッセージを受信することを期待しているためである。同様に、 1. において B が N_{B} を新規に生成するのは、その値を知らない（まだ存在しない）のに送信することになっているからである。このように値の新規生成や確認といった、送信・受信に付随する暗黙の動作は、参加者がその値を知っているかどうかによって決まるように思われる。

以上のような考察にもとづき、本稿では参加者の知識 (knowledge) にもとづいて略式記法の意味論を定義する方法を提案する。鍵となるアイディアは次の 4 つである。

• 知識にない値を送信するときは、新規に生成して、知識に追加する。

• 知識にある値を受信したときは、受信した値が知識にある値と同一であることを確認する。

• 知識にない値を受信したときは、知識に追加する。

• 鍵を知っている暗号文を受信したときは、その暗号文を復号化し、平文を受信したものとみなす。

ただし、各参加者の初期知識は外部からの入力として所与であると仮定する。

たとえば、先の例で A と B の初期知識をいずれも {A, B, K_{AB}} とする。 1. において、 B は N_{B} を知らないので、新規に生成して送信する。 A も N_{B} を知らないので、受信したら知識に追加する。さらに 2. では、 A は N_{B}, B, K_{AB} をいずれも知っているので、 {N_{B}, B}_{K_{AB}} を送信する。 B は K_{AB} を知っているので、 {N_{B}, B}_{K_{AB}} を復号化し、さらに N_{B} と B も知っているので、知識にある N_{B} や B と同一であることを確認する。これらの動作は自然言語による記述とも合致している。

本稿では、略式記法の意味を定義するための表示言語として spi 計算^{6),21)} を使用する。略式記法から spi 計算への変換を定義することにより、略式記法で記述したプロトコルについて、 spi 計算における双模倣^{5),7),8)} や型検査^{1),3),11),12)} といった様々な解析・検証の手法を適用することが可能となる。

以降の構成は次の通りである。 2 節では略式記法の抽象構文を、 3 節では spi 計算の抽象構文を定義する。 4 節では略式記法の意味を spi 計算への変換により定義する。 5 節では、複数のクライアントに応答するサーバのように、相手の特定できないプロトコルを変換す

\begin{aligned}プロトコル & π & ::= & α_{1}; …; α_{n} \\ 行動 & α & ::= & X → Y : M_{1}, …, M_{n} \\ メッセージ & M, N & ::= & v \\ & & | & op(M_{1}, …, M_{n}) \\ & & | & \{M_{1}, …, M_{n}\}_{M} \\ & & | & M^{+} \\ & & | & M^{−} \\ 変数 & v & ::= & X_{Y_{1}...Y_{n}} \\ 原子記号 & X, Y & ::= & A, B, S, x, y, K, N, … \end{aligned}

図 1 略式記法の抽象構文
Fig. 1 Abstract Syntax of Informal Notation

るための拡張について説明し、 6 節では関連研究と今後の課題について議論する。

2. 略式記法

我々の略式記法の抽象構文は図 1 の通りである。プロトコル π は 0 個以上の行動 α の列である。行動 X → Y : M_{1}, …, M_{n} は、参加者 X から参加者 Y へメッセージ列 M_{1}, …, M_{n} を送信することを表現している。ただし、 n は 0 以上の整数であり、以後も同様とする。メッセージ M は、変数 v、算術演算 op(M_{1}, …, M_{n})、鍵 M によるメッセージ列 M_{1}, …, M_{n} の暗号化 {M_{1}, …, M_{n}}_{M}、メッセージ M にもとづく非対称鍵 M^{+}, M^{−} のいずれかである。直観としては、 M^{+} で暗号化されたメッセージは M^{−} によってのみ復号化でき、また、 M^{−} で署名されたメッセージは M^{+} によってのみ確認できる。変数 v は X_{Y_{1}...Y_{n}} (n ≥ 0) という形をしており、たとえば A, K_{AB}, N_{B} などが含まれる。算術演算 op(M_{1}, …, M_{n}) としては、ハッシュ関数 hash(M_{1}, …, M_{n}) や整数定数 i、ノンスに 1 を加える succ(M) などが考えられる。

3. spi 計算

本稿で使用する spi 計算の抽象構文を図 2 に示す。プロセス P は、

• 何もしないプロセス 0

• 値を新規に生成し、 v に束縛してから P を実行するプロセス νv. P

• 通信チャンネル v に M_{1}, …, M_{n} を送信してから P を実行するプロセス\overline{v}⟨M_{1}, …, M_{n}⟩. P

• 通信チャンネル v からメッセージ列を受信し、 v_{1}, …, v_{n} に束縛してから P を実行するプロセス v(v_{1}, …, v_{n}). P

• P と Q を並列に実行するプロセス P | Q プロセスP, Q ::=

0

| νv. P
| \overline{v}⟨M_{1}, …, M_{n}⟩. P
| v(v_{1}, …, v_{n}). P
| P | Q
| !P

| if M = N then P

| case M of {v_{1}, …, v_{n}}_{N} in P
図 2 spi 計算の抽象構文
Fig. 2 Abstract Syntax of spi-Calculus

• P | P | P | … に相当する無限の並列な複製のプロセス !P

• M と N が同一の場合だけ P を実行するプロセ

ス if M = N then P

• 暗号文 M を鍵 N で復号化し、成功したら平文を v_{1}, …, v_{n} に束縛してから P を実行するプロセス case M of {v_{1}, …, v_{n}}_{N} in P

のいずれかである。簡便のために、 P_{1} | … | P_{n} のような並列実行を ∏_{1≤i≤n} P_{i} のように表記する。また、 M̂^{+} = M^{−}, M̂^{−} = M^{+}, M̂ = M （それ以外の場合）と定義する。

プロセスの文脈 (context) C とは、任意のプロセスにおいて一個の部分プロセスを穴 (hole) [ ] でおきかえたものである。文脈 C の穴にプロセス P を代入したプロセスを C[P] と表記する。たとえば C = νx. νy. [ ] は文脈であり、 C[\overline{z}⟨x, y⟩. 0] = νx. νy. \overline{z}⟨x, y⟩. 0 である。

spi 計算の形式的な意味論についてはオリジナルの文献^{6)} を参照されたい。

4. 変換

略式記法のプロトコル π から spi 計算のプロセス P への変換 P = T (π) を図 3 のように定義する。ただし、 I は各参加者から初期知識（メッセージの集合）への写像であり、外から与えられているものとする。また、条件が重複する定義は「上から下へ」適用し、下の定義はそれより上の定義が適用できなかった場合のみ適用できるものとする。

まず、プロトコルの全体 π は、各参加者 X を表現するプロセス T_{X}(π) の並列実行に変換される。 T_{X}(α_{1}; …; α_{n}) は、それぞれの行動 α_{i} を変換した文脈 C_{i} の合成に変換される。変換にあたっては、行動 α_{i} によって X の知識が ρ_{i−1} から ρ_{i} へ増加していくことに注意する。（一般に知識 ρ とは、略式記法におけるメッセージから、それに対応する spi 計算におけるメッセージへの部分写像である。） After_{X}^{σ} は、プロトコルが終了した以降の X の動作を表現するプロセスであり、我々の変換では特定しない。

X の行動 α の変換 T_{X}(ρ, α) は、 X がメッセージを送信するか、受信するか、あるいはどちらもしないかによって場合わけされる。 X がメッセージ M_{1}, …, M_{n} を送信する場合は、それぞれのメッセージ M_{i} について、知識にない値を新規に生成する文脈 C_{i} と、実際に送信するメッセージ N_{i} を、 S_{X}(ρ_{i−1}, M_{i}) により計算していく（1 行目）。 X がメッセージ M_{1}, …, M_{n} を受信する場合は、知識にある値と同一かどうか確認する文脈 C_{i} を、 R_{X}(ρ_{i−1}, M_{i}) により計算していく（2 行目）。 X が送信も受信もしない場合は、何もしない空の文脈 [ ] に変換される（3 行目）。

S_{X}(ρ_{,}M) は、メッセージ M を知識 ρ から作成する。 M 自体が ρ で定義されている場合は、それを使用する（1 行目）。そうでない場合は、まず M の部分式を再帰的に作成し、そこから M を作成する（2〜5 行目）。ただし、 1 節で説明したように、知識にない変数は新規に生成する（6 行目）。

R_{X}(ρ, M) は、メッセージ M を知識 ρ から作成できる場合は、受信した x が M と同一であることを確認する（1 行目）。また、メッセージが暗号文 {M_{1}, … M_{n}}_{M} であり、 M を ρ から作成できる場合は、復号化して再帰的に平文 M_{1}, … M_{n} を処理する（2 行目）。どちらでもない場合は、メッセージを知識に追加する（3 行目）。

map_{X}(ρ, M) は、メッセージ M を知識 ρ から作成する。知識にない変数を新規に生成しない（したがって知識も増加しない）こと以外は、 S_{X}(ρ, M_{i}) と同様である。

なお、 S_{X}(ρ_{,}M), R_{X}(ρ, M), map_{X}(ρ, M) の X は図 3 の定義で使用されていないが、次節の拡張で必要となる。

例 1 1 節で例に挙げた ISO 対称鍵 2 パス一方向認証プロトコル

\begin{aligned}1. & B & → & A & : & N_{B} \\ 2. & A & → & B & : & \{N_{B}, B\}_{K_{AB}} \end{aligned}

を初期知識 I(A) = I(B) = {A, B, K_{AB}} で変換すると以下のようになる。

T (π)  = ∏_{X∈dom(I)} T_{X}(π)
T_{X}(α_{1}; …; α_{n})  = C_{1}[… [C_{n}[After_{X}^{σ}]]]

if T_{X}(ρ_{0}, α_{1}) = (ρ_{1}, C_{1}), …, T_{X}(ρ_{n−1}, α_{n}) = (ρ_{n}, C_{n}) for ρ_{0} = {M ↦ M | M ∈ I(X)} and σ = ρ_{n} \ {M ↦ M | any M}

T_{X}(ρ, X → Y : M_{1}, …, M_{n}) = (ρ_{n}, C_{1}[… [C_{n}[\overline{chan_{Y}} ⟨N_{1}, …, N_{n}⟩. [ ]]]])

if Y ≠ X and S_{X}(ρ, M_{1}) = (ρ_{1}, C_{1}, N_{1}), …, S_{X}(ρ_{n−1}, M_{n}) = (ρ_{n}, C_{n}, N_{n})

T_{X}(ρ, Y → X : M_{1}, …, M_{n}) = (ρ_{n}, chan_{X}(x_{1}, …, x_{n}). C_{1}[… [C_{n}[ ]]])

if Y ≠ X, x_{1}, …, x_{n} fresh, and R_{X}(ρ, x_{1}, M_{1}) = (ρ_{1}, C_{1}), …, R_{X}(ρ_{n−1}, x_{n}, M_{n}) = (ρ_{n}, C_{n})

T_{X}(ρ, Y → Z : M_{1}, …, M_{n}) = (ρ, [ ])

if Y ≠ X and Z ≠ X

S_{X}(ρ, M)  = (ρ, [ ], ρ(M))

if M ∈ dom(ρ)

S_{X}(ρ, op(M_{1}, …, M_{n}))  = (ρ_{n}, C_{1}[… [C_{n}[ ]]], op(N_{1}, …, N_{n}))

if S_{X}(ρ, M_{1}) = (ρ_{1}, C_{1}, N_{1}), …, S_{X}(ρ_{n−1}, M_{n}) = (ρ_{n}, C_{n}, N_{n})

S_{X}(ρ, M^{+})  = (ρ′, C[ ], N^{+})

if S_{X}(ρ, M) = (ρ′, C, N)

S_{X}(ρ, M^{−})  = (ρ′, C[ ], N^{−})

if S_{X}(ρ, M) = (ρ′, C, N)

S_{X}(ρ, {M_{1}, …, M_{n}}_{M})  = (ρ_{n}, C[C_{1}[… [C_{n}[ ]]]], {N_{1}, …, N_{n}}_{N})

if S_{X}(ρ, M) = (ρ_{0}, C, N) and S_{X}(ρ_{0}, M_{1}) = (ρ_{1}, C_{1}, N_{1}), …, S_{X}(ρ_{n−1}, M_{n}) = (ρ_{n}, C_{n}, N_{n})

S_{X}(ρ, v)  = ((ρ, v ↦ v), νv. [ ], v)
R_{X}(ρ, x, M)  = (ρ, C[if x = N then [ ]])

if map_{X}(ρ, M) = (C, N)

R_{X}(ρ, x, {M_{1}, …, M_{n}}_{M})  = (ρ_{n}, C[case x of {y_{1}, …, y_{n}}_{N} in C_{1}[… [C_{n}[ ]]]])

if map_{X}(ρ, _{M}) = (C, N)

and R_{X}(ρ, y_{1}, M_{1}) = (ρ_{1}, C_{1}), …, R_{X}(ρ_{n−1}, y_{n}, M_{n}) = (ρ_{n}, C_{n})

R_{X}(ρ, x, M)  = ((ρ_{n}, M ↦ x), [ ])
map_{X}(ρ, M)  = ([ ], ρ(M))

if M ∈ dom(ρ)

map_{X}(ρ, op(M_{1}, …, M_{n}))  = (C_{1}[… [C_{n}[ ]]], op(N_{1}, …, N_{n}))

if map_{X}(ρ, M_{1}) = (C_{1}, N_{1}), …, map_{X}(ρ, M_{n}) = (C_{n}, N_{n})

map_{X}(ρ, M^{+})  = (C[ ], N^{+})

if map_{X}(ρ, M) = (C, N)

map_{X}(ρ, M^{−})  = (C[ ], N^{−})

if map_{X}(ρ, M) = (C, N)

map_{X}(ρ, {M_{1}, …, M_{n}}_{M})  = (C_{1}[… [C_{n}[C[ ]]]], {N_{1}, …, N_{n}}_{N})

if map_{X}(ρ, M) = (C, N) and map_{X}(ρ, M_{1}) = (C_{1}, N_{1}), …, map_{X}(ρ, M_{n}) = (C_{n}, N_{n})

図 3 略式記法から spi 計算への変換
Fig. 3 Translation from Informal Notation to spi-Calculus

chan_{A}(x). \overline{chan_{B}}⟨\{x, B\}_{K_{AB}} ⟩. After_{A}^{N_{B}↦x}

| νN_{B}. \overline{chan_{A}}⟨N_{B}⟩.

chan_{B}(y). case y of {z_{1}, z_{2}}_{K_{AB}} in

if z_{1} = N_{B} then if z_{2} = B then After_{B}^{∅}

このプロセスを簡約すると

νN_{B}. (After_{A}^{N_{B}↦N_{B}} | After_{B}^{∅})

になり、プロトコルが正常に実行されることがわかる。なお、通信チャンネル chan_{A} と chan_{B} が ν によって束縛されずオープンであることは、プロトコルの実行されるネットワークが公開されており盗聴や改竄が可能であるという通常の仮定^{10)} を反映している。

例 2 2 人の参加者 A, B が相互に認証することを目的とする Needham-Schroeder 公開鍵プロトコル^{18)}

\begin{aligned}1. & A & → & B & : & \{N_{A}, A\}_{K_{B}^{+}} \\ 2. & B & → & A & : & \{N_{A}, N_{B}\}_{K_{A}^{+}} \\ 3. & A & → & B & : & \{N_{B}\}_{K_{B}^{+}} \end{aligned}

を、初期知識 I(A) = {A, B, K_{A}^{+}, K_{A}^{−}, K_{B}^{+}}, I(B) = {A, B, K_{A}^{+}, K_{B}^{+}, K_{B}^{−}} で変換すると以下のようになる。この変換結果は、人間の直観による通常の表現^{2)} と等価である^{☆}。

νN_{A}. \overline{chan_{B}}⟨\{N_{A}, A\}_{K_{B}^{+}}⟩.

chan_{A}(y). case y of {y_{1}, y_{2}}_{K_{A}^{−}} in

       if y_{1} = N_{A} then

\overline{chan_{B}}⟨\{y_{2}\}_{K_{B}^{+}}⟩. After_{A}^{N_{B}↦y_{2}}
| chan_{B}(x). case x of {x_{1}, x_{2}}_{K_{B}^{−}} in

       if x_{2} = A then

νN_{B}. \overline{chan_{A}}⟨\{x_{1}, N_{B}\}_{K_{A}^{+}}⟩.
chan_{B}(z). case z of {z_{1}}_{K_{B}^{−}} in

       if z_{1} = N_{B} then After_{B}^{N_{A}↦x_{1}}

公開鍵による暗号化 {N_{A}, A}_{K_{B}^{+}}, {N_{A}, N_{B}}_{K_{A}^{+}}, {N_{B}}_{K_{B}^{+}} とその復号化が変換される方法に注意されたい。このプロセスは簡約すると

νN_{A}. νN_{B}. (After_{A}^{N_{B}↦N_{B}} | After_{B}^{N_{A}↦N_{A}})

となる。なお、このプロトコルは使用の方法によっては欠陥があることで有名である^{15)}。これについては次節で議論する。

例 3 2 人の参加者 A, B が相互に認証し、さらに鍵 K′_{AB} とノンス N′_{B} を共有することを目的とする Andrew Secure RPC プロトコル^{9)}

1. A → B : A, {N_{A}}_{K_{AB}}
2. B → A : {succ(N_{A}), N_{B}}_{K_{AB}}
3. A → B : {succ(N_{B})}_{K_{AB}}
4. B → A : {K′_{AB}, N′_{B}}_{K_{AB}}

を、初期知識 I(A) = I(B) = {K_{AB}, A, B} で変換すると以下のようになる。

νN_{A}. \overline{chan_{B}}⟨A, \{N_{A}\}_{K_{AB}} ⟩.
chan_{A}(y). case y of {y_{1}, y_{2}}_{K_{AB}} in
if y_{1} = succ(N_{A}) then
\overline{chan_{B}}⟨\{succ(y_{2})\}_{K_{AB}} ⟩.
C_{A}(w). case w of {w_{1}, w_{2}}_{K_{AB}} in
After_{A}^{N_{B}↦y_{2},K′_{AB}↦w_{1},N′_{B}↦w_{2}}
| chan_{B}(x_{1}, x_{2}). if x_{1} = A then
case x_{2} of {x_{3}}_{K_{AB}} in
νN_{B}. \overline{chan_{A}}⟨\{succ(x_{3}), N_{B}\}_{K_{AB}} ⟩.
chan_{B}(z). case z of {z_{1}}_{K_{AB}} in
if z_{1} = succ(N_{B}) then
νK′_{AB}. νN′_{B}. \overline{chan_{A}}⟨\{K′_{AB}, N′_{B}\}_{K_{AB}} ⟩.
After_{B}^{N_{A}↦z_{1}}

この例題では算術演算 succ(N_{A}), succ(N_{B}) が変換される方法に注意されたい。上述のプロセスを簡約すると

νN_{A}. νN_{B}. νK′_{AB}. νN′_{B}.
After_{A}^{N_{B}↦N_{B},K′_{AB}↦K′_{AB},N′_{B}↦N′_{B}} |
After_{B}^{N_{A}↦N_{A}}

となる。なお、このプロトコルはメッセージ 4. に A の確認できるノンスが存在しないので、リプレイ攻撃が可能である。実際に、上述の変換結果 P について

P | P | chan_{A}(x_{4}). \overline{chan_{A}}(x_{4}). \overline{chan_{A}}(x_{4}). 0

を簡約すると、単一の K′_{AB}, N′_{B} について After_{A} が二回、重複して実行されうる。また、 Needham-Schroeder 公開鍵プロトコルと同様の問題も存在する。例 4 参加者 B がサーバ S を経由して参加者 A を認証することを目的とする、 Woo と Lam の認証プロトコル Π^{9)}

\begin{aligned}1. & A & → & B & : & A \\ 2. & B & → & A & : & N_{B} \\ 3. & A & → & B & : & \{N_{B}\}_{K_{AS}} \\ 4. & B & → & S & : & \{A, \{N_{B}\}_{K_{AS}} \}_{K_{BS}} \\ 5. & S & → & B & : & \{N_{B}\}_{K_{BS}} \end{aligned}

を、初期知識 I(A) = {A, B, S, K_{AS}}, I(B) = {A, B, S, K_{BS}}, I(S) = {A, B, S, K_{AS}, K_{BS}} で変換すると以下のようになる。 \overline{chan_{B}}⟨A⟩. chan_{A}(y). \overline{chan_{B}}⟨\{y\}_{K_{AS}} ⟩. After_{A}^{N_{B}↦y}

☆ただし、文献^{2)} では解析の都合により、\overline{v}⟨…⟩. P という形の

プロセスを許さず、かわりに\overline{v}⟨…⟩ | P という形のプロセスを

用いている点が異なる。

| chan_{B}(x). if x = A then νN_{B}. \overline{chan_{A}}⟨N_{B}⟩.

chan_{B}(z). \overline{chan_{S}}⟨\{A, z\}_{K_{BS}} ⟩. chan_{B}(u). case u of {u_{1}}_{K_{BS}} in if u_{1} = N_{B} then After_{B}^{{N_{B}}_{K_{AS}} ↦z}

| chan_{S}(w). case w of {w_{1}, w_{2}}_{K_{BS}} in

if w_{1} = A then case w_{2} of {w_{3}}_{K_{AS}} in

\overline{chan_{B}}⟨\{w_{3}\}_{K_{BS}} ⟩. After_{S}^{N_{B}↦w_{3}}

B は K_{AS} を知らないので、 3. で受信したメッセージを復号化せず、暗号文のままで 4. のメッセージの一部として送信することに注意されたい。このプロセスを簡約すると

νN_{B}.

After_{A}^{N_{B}↦N_{B}} | After_{B}^{{N_{B}}_{K_{AS}} ↦{N_{B}}_{K_{AS}}} |

After_{S}^{N_{B}↦N_{B}}

となる。

5. 変換の拡張

Needham-Schroeder 公開鍵プロトコルの次のような使い方を考える。

\begin{aligned}1. & B & → & A & : & B \\ 2. & A & → & B & : & \{N_{A}, A\}_{K_{B}^{+}} \\ 3. & B & → & A & : & \{N_{A}, N_{B}\}_{K_{A}^{+}} \\ 4. & A & → & B & : & \{N_{B}\}_{K_{B}^{+}} \end{aligned}

これは、サーバ A がクライアント B からのリクエストにより相互認証を開始する、というシステムである。

もし A の初期知識に特定の名前 B があるとすると、 A を変換したプロセスは

chan_{A}(x). if x = B then … となるから、 A はその B からのリクエストしか処理できない。では、もし A の初期知識に B がなければ、 A は複数の B からのリクエストを処理できるのだろうか? I(A) = {A, K_{A}^{+}, K_{A}^{−}, K_{B}^{+}} として、図 3 の定義にしたがい実際に変換してみると、以下の結果がえられる。

chan_{A}(w).
νN_{A}. \overline{chan_{B}}⟨\{N_{A}, A\}_{K_{B}^{+}}⟩.
chan_{A}(y). case y of {y_{1}, y_{2}}_{K_{A}^{−}} in

       if y_{1} = N_{A} then

\overline{chan_{B}}⟨\{y_{2}\}_{K_{B}^{+}}⟩. After_{A}^{N_{B}↦y_{2}}
| \overline{chan_{A}}⟨B⟩.
chan_{B}(x). case x of {x_{1}, x_{2}}_{K_{B}^{−}} in

       if x_{2} = A then

νN_{B}. \overline{chan_{A}}⟨\{x_{1}, N_{B}\}_{K_{A}^{+}}⟩.
chan_{B}(z). case z of {z_{1}}_{K_{B}^{−}} in

       if z_{1} = N_{B} then After_{B}^{N_{A}↦x_{1}}

しかし、この結果には問題がある。 A は任意の B すなわち w からのリクエストを処理したいにもかかわらず、特定の B の通信チャンネル chan_{B} および公開鍵 K_{B}^{+} を使用するからである。直観としては chan_{w} ないし K_{w}^{+} のように表記したいところだが、このようなパラメタのある変数は、 spi 計算の操作的意味論の範疇から逸脱している。

そこで本稿では変換を拡張し、 w のような変数から chan_{w} ないし K_{w}^{+} のような通信チャンネルや公開鍵を動的に検索するための、いわば「データベース」に相当するプロセスを生成・使用する。たとえば、上の例は以下のように変換される。

       νgetc. νgetk.

!getc(r, x). ∏_{Z∈dom(I)∧Z∉I(A)}

           if x = Z then \overline{r}⟨chan_{Z}⟩ |

!getk(r, x). ∏_{K_{Z}^{+}∈I(A)∧Z∉I(A)}

if x = Z then \overline{r}⟨K_{Z}^{+}⟩ |

chan_{A}(w).

νN_{A}. νr_{1}. \overline{getc}⟨r_{1}, w⟩. r_{1}(c). νN_{B}. νr_{2}. \overline{getk}⟨r_{2}, w⟩. r_{2}(k). \overline{c}⟨\{N_{A}, A\}_{k}⟩. chan_{A}(y). case y of {y_{1}, y_{2}}_{K_{A}^{−}} in

         if y_{1} = N_{A} then

\overline{c}⟨\{y_{2}\}_{k}⟩. After_{A}^{N_{B}↦y_{2}}

| …

プロセス !getc(r, x)…. が名前 x から通信チャンネル chan_{x} を、プロセス !getk(r, x)…. が名前 x から鍵 K_{x}^{+} を動的に検索するためのデータベースに相当する。ただし、 r は返信のための通信チャンネルである。すなわち、 getc ないし getk に、通信チャンネル r と参加者の名前 Z を送信すると、 r に chan_{Z} ないし K_{Z}^{+} が返信される。ここでは νr_{1}. \overline{getc}⟨r_{1}, w⟩. r_{1}(c) と νr_{2}. \overline{getk}⟨r_{2}, w⟩. r_{2}(k) が、そのような動的な検索

T_{X}(α_{1}; …; α_{n})  = νget_{XY_{1}}. . . . . νget_{XY_{m}}.

νget+_{XY_{1}}. . . . . νget+_{XY_{m}}.

∏_{i,n}!get_{XY_{i}}(r, x_{1}, …, x_{n}).

∏Y_{i}_{Z1...Zn} ∈I(X)∪{chan_{Z} |Z∈dom(I)}∧{Z_{1},...,Z_{n}}\I(X)≠∅

if x_{1} = Z_{1} then … if x_{n} = Z_{n} then r⟨Y_{Z_{1}...Z_{n}}⟩ | ∏_{i,n}!get+_{XY_{i}}(r, x_{1}, …, x_{n}).

∏Y_{i}_{Z1...Zn}^{+} ∈I(X)∧{Z_{1},...,Z_{n}}\I(X)≠∅

if x_{1} = Z_{1} then … if x_{n} = Z_{n} then r⟨Y_{Z_{1}...Z_{n}}^{+}⟩ | C_{1}[… [C_{n}[After_{X}^{σ}]]])

if {Y_{1}, …, Y_{m}} = {Y | Y appears in I} ∪ {chan}, T_{X}(ρ_{0}, α_{1}) = (ρ_{1}, C_{1}), …, T_{X}(ρ_{n−1}, α_{n}) = (ρ_{n}, C_{n}) for ρ_{0} = {M ↦ M | M ∈ I(X)} and σ = ρ_{n} \ {M ↦ M | any M}

T_{X}(ρ, X → Y : M_{1}, …, M_{n}) = (ρ_{n}, νr. \overline{get_{Xchan}}⟨r, ρ(Y)⟩. r(c). C_{1}[… [C_{n}[\overline{c}⟨N_{1}, …, N_{n}⟩. [ ]]]])

if r, c fresh, Y ≠ X, Y ∉ I(X), and S_{X}(ρ, M_{1}) = (ρ_{1}, C_{1}, N_{1}), …, S_{X}(ρ_{n−1}, M_{n}) = (ρ_{n}, C_{n}, N_{n})

S_{X}(ρ, Y_{Z_{1}...Z_{n}})  = (ρ, νr. \overline{get_{XY}} ⟨r, ρ(Z_{1}), …, ρ(Z_{n})⟩. r(k). [ ], k)

if r, k fresh, Y_{Z_{1}...Z_{n}} ∈ I(X) and {Z_{1}, …, Z_{n}} \ I(X) ≠ ∅

S_{X}(ρ, Y_{Z_{1}...Z_{n}}^{+})  = (ρ, νr. \overline{get+_{XY}} ⟨r, ρ(Z_{1}), …, ρ(Z_{n})⟩. r(k). [ ], k)

if r, k fresh, Y_{Z_{1}...Z_{n}}^{+} ∈ I(X) and {Z_{1}, …, Z_{n}} \ I(X) ≠ ∅

map_{X}(ρ, Y_{Z_{1}...Z_{n}})  = (νr. \overline{get_{XY}} ⟨r, ρ(Z_{1}), …, ρ(Z_{n})⟩. r(k). [ ], k)

if r, k fresh, Y_{Z_{1}...Z_{n}} ∈ I(X) and {Z_{1}, …, Z_{n}} \ I(X) ≠ ∅

map_{X}(ρ, Y_{Z_{1}...Z_{n}}^{+})  = (νr. \overline{get+_{XY}} ⟨r, ρ(Z_{1}), …, ρ(Z_{n})⟩. r(k). [ ], k)

if r, k fresh, Y_{Z_{1}...Z_{n}}^{+} ∈ I(X) and {Z_{1}, …, Z_{n}} \ I(X) ≠ ∅

図 4 鍵データベースによる変換の拡張
Fig. 4 Extension of the Translation with Key Database

に相当するプロセスである。 ; 鍵ないし通信チャンネルの動的な検索がどのような ; 場合に必要かは、以下のように判定する。先の例で、 ; 知識 I(A) によく注意すると、参加者 B を知らない ; にもかかわらず、その公開鍵 K_{B}^{+} を知っていること ; になっている。これは、 B が静的にはわからず、 K_{B}^{+} ; を動的に検索する必要があることを暗示している。一 ; 般に、変数 X_{Y_{1}...Y_{n}} が初期知識にあるにもかかわら ; ず、 Y_{1}, …, Y_{n} のいずれかが初期知識にない場合は、 ; X_{Y_{1}...Y_{n}} を動的に検索しなければならない。 ; 以上の考察にもとづいて、図 3 の定義を図 4 のよう ; に拡張する。ただし、条件の重複する定義については ; 図 4 を優先するものとする。先の例は、この定義の特 ; 殊な場合となっている。 ; 図 4 の前半では、参加者 X を変換するときに、 X ; が動的に検索する（かもしれない）すべての鍵ないし ; 通信チャンネル Y_{i}_{x_{1}...x_{n}} および Y_{i}_{x_{1}...x_{n}}^{+} について、 ; それらのデータベースに相当するプロセスを並列に生 ; 成している。プロセス !get_{XY_{i}}(r, x_{1}, …, x_{n})…. は、 ; 参加者 X が共有鍵ないし通信チャンネル Y_{i}_{x_{1}...x_{n}} を ; 動的に検索するためのデータベースに相当する。先の例でいえば、 A が X に、 chan が Y_{i} に、 getc が get_{XY_{i}} に、 x が x_{1}, …, x_{n} に当たる。同様に、プロセス !get+_{XY_{i}}(r, x_{1}, …, x_{n})…. は、参加者 X が公開鍵 Y_{i}_{x_{1}...x_{n}}^{+} を動的に検索するためのデータベースに相当する。先の例でいえば、 A が X に、 K が Y_{i} に、 getk が get+_{XY_{i}} に、 x が x_{1}, …, x_{n} に当たる。図 4 の後半では、参加者 X の各行動を変換するときに、（必要ならば）データベースの動的な検索に相当するプロセスを生成している。動的な検索が必要かどうかは、前述のように「使用したい変数 Y_{Z_{1}...Z_{n}} ないし Y_{Z_{1}...Z_{n}}^{+} が初期知識にあるにもかかわらず、 Z_{1}, …, Z_{n} のいずれかが初期知識にない」ことにより判定する。

たとえば、 A は攻撃者 E の公開鍵 K_{E}^{+} を知っているものとして、前述の変換結果を P とする。

\overline{chan_{A}}⟨E⟩.
chan_{E}(x). case x of {x_{1}, x_{2}}_{K_{E}^{−}} in

     chan_{A}(y). if y = B then

\overline{chan_{B}}⟨\{x_{1}, x_{2}\}_{K_{B}^{+}}⟩.
chan_{E}(z). case z of {z_{1}}_{K_{E}^{−}} in
\overline{chan_{B}}⟨\{z_{1}\}_{K_{B}^{+}}⟩.
After_{E}^{N_{A}↦x_{1},N_{B}↦z_{1}}

なる攻撃プロセス Q について P | Q を実行すると、

νN_{A}. νN_{B}.
After_{A}^{N_{B}↦N_{B}} | After_{B}^{N_{A}↦N_{A}} |
After_{E}^{N_{A}↦N_{A},N_{B}↦N_{B}}

のように、 E が A, B のノンス N_{A}, N_{B} を共有するプロセスに簡約されてしまう。このように、 A が B だけでなく E からのリクエストも処理する場合は、いわゆる man-in-the-middle 攻撃が可能である^{15)} ことが、拡張された変換によって正確に反映されている。

なお、既存の文献^{2)} では同様の攻撃を表現するにあたり、本稿のように鍵や通信チャンネルを動的に検索するのではなく、 B と E のそれぞれについて別々の A が存在することを仮定している。この仮定は場合によっては非現実的だが、非依存型システムによりプロトコルを解析するために要求されている。依存型により解析を拡張すれば、本稿と同様の表現も使用できると予想される。

6. 関連研究と今後の課題

本稿ではセキュリティプロトコルの略式表現から spi 計算への変換を定義し、略式表現の意味を明確にした。我々は本稿のアイディアにもとづいて、略式表現のプレーンテキストから spi 計算のプロセス（および双方を整形した TEX ソース）を生成する Objective Caml^{14)} のプログラムを実装した。そもそも略式表現の意味が変換以外に定義されていないので、変換の妥当さを厳密に証明したり自動で検査することはできないが、我々は文献^{9)} にある 24 個のプロトコルについて、変換の結果が直観と合致していることを人手で確認した^{19)}。 24 個の中で主な 4 つを 4 節に挙げたが、他の 20 個のプロトコルも 4 つのいずれかと同じような形をしており、（5 節の拡張も含めて）同じように変換できる。

関連研究としては、すでに言及した spi 計算や spi 計算における検証以外に、 Casper^{16)} と CAPSL^{17)} がある。 Casper は略式記法に類似したスクリプトを、プロセス計算の一種である CSP^{13)} に変換するコンパイラである。 CAPSL はセキュリティプロトコルを記述・検証するための形式言語である。しかしどちらの言語も、参加者の予備知識だけでなく、参加者の役割（initiator か responder か）や変数の種類（メッセージかノンスか公開鍵か）の宣言が必要であり、プロトコルの動作を記述する目的では、我々の方法のほうが簡潔である。一方で、本稿の略式記法ではプロトコルの目的は記述できない。これを可能にするには、秘密にしたいメッセージに annotation をつけたり、認証を表現する対応表明^{11),20)} を挿入するといった拡張が必要だろう。

また、本稿の変換では算術演算の性質やタイムスタンプの概念に依存したセキュリティプロトコルを正確に定義することができない。図 3 の定義は、たとえば加算の結合法則を反映していないので、もし x + y と z の値を知っていても、 x + (y + z) の値は知らないことになってしまう。この問題を解決するためには、たとえば x + (y + z) を (x + y) + z と解釈させるような annotation を導入するか、あるいは応用 π 計算^{4)} と同様の等式理論で変換を拡張し、 M = N かつ map_{X}(ρ, N) が定義されている N が存在したら M の値を知っているとみなさなければならない。タイムスタンプについては、 fresh なノンスとして解釈するだけならば本稿の変換で可能だが、時間の概念を導入した解釈はそもそも spi 計算やほとんどの formal method でも手法が確立されておらず、今後の課題である。

参考文献

1) Abadi, M.: Secrecy by Typing in Security Protocols, Journal of the ACM , Vol. 46, No. 5, pp. 749–786 (1999). Preliminary version appeared in Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Springer-Verlag, vol. 1281, pp. 611–638, 1997.

2) Abadi, M. and Blanchet, B.: Secrecy Types for Asymmetric Communication, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Vol. 2030, Springer-Verlag, pp. 25–41 (2001).

3) Abadi, M. and Blanchet, B.: Secrecy Types for Asymmetric Communication, Theoretical Computer Science, Vol. 298, No. 3, pp. 387– 415 (2003). Preliminary version appeared in Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Springer-Verlag, vol. 2030, pp. 25–41, 2001.

4) Abadi, M. and Fournet, C.: Mobile Values, New Names, and Secure Communication, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 104–115 (2001).

5) Abadi, M. and Gordon, A. D.: A Bisimulation Method for Cryptographic Protocols, Nordic Journal of Computing, Vol. 5, pp. 267–303 (1998). Preliminary version appeared in Programming Languages and Systems – ESOP’98, 7th European Symposium on Programming, Lecture Notes in Computer Science, Springer-Verlag, vol. 1381, pages 12–26, 1998.

6) Abadi, M. and Gordon, A. D.: A Calculus for Cryptographic Protocols: The spi Calculus, Information and Computation, Vol. 148, No. 1, pp. 1–70 (1999). Preliminary version appeared in Proceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36–47, 1997.

7) Boreale, M., De Nicola, R. and Pugliese, R.: Proof Techniques for Cryptographic Processes, SIAM Journal on Computing, Vol.31, No.3, pp. 947–986 (2002). Preliminary version appeared in 14th Annual IEEE Symposium on Logic in Computer Science, pp. 157–166, 1999.

8) Borgström, J. and Nestmann, U.: On Bisimulations for the Spi Calculus, 9th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, Vol.2422, Springer-Verlag, pp.287–303 (2002).

9) Clark, J. and Jacob, J.: A Survey of Authentication Protocol Literature: Version

1.0, http://www-users.cs.york.ac.uk/~jac/
papers/drareview.ps.gz (1997).

10) Dolev, D. and Yao, A. C.: On the security of public key protocols, IEEE Transactions on Information Theory, Vol. 29, No. 2, pp. 198–208 (1983).

11) Gordon, A.D. and Jeffrey, A.: Authenticity by Typing for Security Protocols, Journal of Computer Security (2003). To appear. Extended abstract appeared in 14th IEEE Computer Security Foundations Workshop, pp. 145–159, 2001.

12) Gordon, A. D. and Jeffrey, A.: Types and Effects for Asymmetric Cryptographic Protocols, Journal of Computer Security (2004). To appear. Extended abstract appeared in 15th IEEE Computer Security Foundations Workshop, pp. 77–91, 2002.

13) Hoare, C. A. R.: Communicating Sequential Processes, Prentice Hall (1985). http://www.

usingcsp.com/.

14) Leroy, X.: Objective Caml, http://caml.

inria.fr/.

15) Lowe, G.: An Attack on the Needham-Schroeder Public-Key Authentication Protocol, Information Processing Letters, Vol. 56, No. 3, pp. 131–133 (1995).

16) Lowe, G.: Casper: A Compiler for the Analysis of Security Protocols, 10th IEEE Computer Security Foundations Workshop, pp. 18– 30 (1997).

17) Millen, J. K.: Common Authentication Protocol Specification Language, http://www.csl.

                                                sri.com/users/millen/capsl/.

18) Needham, R. and Schroeder, M.: Using encryption for authentication in large networks of computers, Communications of the ACM , Vol. 21, No. 12, pp. 993–999 (1978).

19) Tatsuzawa, H.: Translating Security Protocols from Informal Notation into Spi Calculus, Bachelor’s Thesis, Department of Information Science, Faculty of Science, University of Tokyo (2003).

20) Woo, T. Y. C. and Lam, S. S.: A Semantic Model for Authentication Protocols, IEEE Symposium on Security and Privacy, pp. 178– 194 (1993).

21) 住井英二郎: チュートリアル: 暗号化通信の spi 計算による形式的検証, コンピュータソフトウェア (2003). 掲載予定.

(平成 16 年2 月 23 日受付) (平成 16 年5 月 10 日採録)

住井英二郎

1975 年生。 1998 年 3 月東京大学理学部情報科学科卒業。 2000 年 3 月同大学院理学系研究科情報科学専攻修士課程修了。 2000 年 4 月より 2001 年 3 月まで同博士課程学生、日

本学術振興会特別研究員、およびペンシルバニア大学コンピュータ情報科学科 Visiting Scholar。 2001 年 4 月より 2003 年 3 月まで東京大学大学院情報理工学系研究科コンピュータ科学専攻助手。 2003 年 4 月よりペンシルバニア大学コンピュータ情報科学科 Research Associate。情報セキュリティ、プロセス計算、部分評価等の領域における、プログラミング言語および型システムの理論と応用について研究。 ACM 会員。

10  情報処理学会論文誌  2004

立沢秀晃 昭和 55 年生。平成 15 年東京大 学大学院情報理工学系研究科コン ピュータ科学専攻修士課程入学。現 在修士 2 年。米澤明憲（正会員） 1947 年 6 月に生まれ、 MIT 計算機科学科博士課程修了 (Ph.D. in Computer Science), MIT 計算機科学研究所および人工知能研究所において並列・分散計算モデルの研究に

従事し、「並列オブジェクト」概念のパイオニアの一人として知られている。帰国後、東工大を経て、 1988 年に東京大学理学部情報科学科教授に着任した。米国計算機学会終身フェロー (ACM Fellow) であり、 ACM TOPLAS 副編集長、日本ソフトウエア科学会理事長、ドイツ国立情報科学技術研究所 (GMD) 科学顧問、政府情報科学技術委員会委員などを歴任。