二者間データ通信を安全に行うプロトコルの自動生成法

日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
1
二者間データ通信を安全に行うプロトコルの自動生成法
Construction method of Security Protocols for Data Exchange
between Two Participants
†
‡
佐藤 直人
‡
萩原 茂樹
Shigeki Hagihara
Naoto Sato
†
米崎 直樹
Naoki Yonezaki
日立製作所システム開発研究所
Hitachi, Ltd., Systems Developemnt Laboratory
[email protected]
‡
東京工業大学大学院情報理工学研究科計算工学専攻
Department of Computer Science, Graduate School of Information Science and Engineering,
Tokyo Institute of Technology
{hagihara,[email protected]
[email protected][email protected]る。本稿
では二者間データ通信のためのセキュリティプロトコル自動生成法を提案する。これは、プロトコルの構造
から安全性を導出する推論規則を利用し、安全なプロトコルのみを生成する手法である。また、プロトコル
に対するコスト評価を行うことで、使用環境に適したより良いプロトコルを生成する。さらに、他の自動生
成方式と比較することで、本稿で提案する自動生成法の利点についても議論する。
1
はじめに
個人情報や商取引に関する重要データがネットワー
ける意味に基づいて証明する。最後に、他の自動生
成法との比較も行う。
クを通じて伝達されるようになった現在、これらの
通信上のセキュリティを守るためには、暗号化技術
準備
2
が必須であるが、それだけでは十分ではない。たと
本稿で自動生成の対象としているプロトコルの性
え、暗号化技術が完全であっても、伝送手順である
質や、想定する攻撃者の振る舞い、プロトコルが満
プロトコルに欠陥があればメッセージのすり替えや
たすべき安全性等を定義する。
成り済まし攻撃を受ける可能性がある。よって、プ
ロトコルの安全性を形式的に検証する技術が必要で
ある。しかし、検証のコストを考えると、これまで
は非形式的に行われてきたプロトコルの設計を形式
的に行うアプローチの方が現実的である。
そこで本稿では、二者間でデータ通信を行うため
のセキュリティプロトコルの自動生成法を提案する。
2.1
生成対象プロトコル
• 2 者間でデータをやり取りするためのプロトコ
ルを生成する。データとは、ナンスや参加者の
名前とは異なるメッセージで、これをお互いに
通達することをプロトコルの目的とする。
この生成法では安全性が保証されているメッセージ
• 参加者は受信したデータを返送することはない。
構造を元に、安全なプロトコルのみを生成する。ま
• データは必ず交互にやり取りする。
た、プロトコルに対する静的なコスト評価を行うこ
とで、使用環境に適したセキュリティプロトコルを
選別する。
以下ではまず前提条件を示した後、プロトコルの
構造から安全性を推論するための推論規則を導入す
る。そしてこれを利用した自動生成手続きを示す。さ
らにこの推論規則の健全性をストランド空間 [3] にお
• 1つの送受信メッセージに対して、同じ鍵で二
度以上の暗号化、署名操作は行わない。
• ナンスは必ずセッションに対応付けて使用する。
(自分の作成したナンスとセッションとの対応を、
相手に認識させる)
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
2
• レスポンダは、ステップ 1 のメッセージからイ
ニシエータの名前を知ることが出来る。
• 秘密にしたいデータ(何番目のデータを秘密に
するか)。
• 正当な参加者がセッションごとに作成するナン
スは新規なものであり、以前に使用されたもの
を使用することはない。(ナンスの新規性)
• イニシエータとレスポンダのどちらからデータ
• 参加者は一度に複数のセッションで通信を行う
ことが出来る。
を送信し始めるか。
自動生成法
3
本節では、プロトコルの自動生成法について述べ
る。初めに自動生成に利用する論理を与え、その後こ
2.2
攻撃者のモデル
本稿では、攻撃者の振る舞いや、その知識を以下
れを利用した自動生成手続きについて述べる。また、
プロトコルに対するコスト評価についても述べる。
のように想定する。
3.1
• 攻撃者は、通信される全てのメッセージを盗聴
することが出来る。
• 攻撃者は、通信される全てのメッセージを他の
メッセージとすり替えることが出来る。
• 攻撃者は対象とするネットワークにおいて、参
加者として通信を行うことが出来る。
• 攻撃者は全ての参加者の公開鍵を知っている。
• セッション開始前に、攻撃者がそのセッション
参加者の秘密鍵を知っていることはない。
論理
本節では、プロトコルの自動生成に用いる論理を
与える。この論理を用いることで、前節であげた安
全性の検証を行うことができる。
3.1.1
用語
A, B: それぞれ、イニシエータ、レスポンダを表す
定数。
Si , Ri : ステップ i での送信者、受信者を表すメタ
変数。
(ステップ i でイニシエータが送信者、レスポ
ンダが受信者であるとき、Si = A, Ri = B となる。
レスポンダが送信者、イニシエータが受信者である
• 攻撃者は、元々知っている知識や攻撃によって とき、Si = B, Ri = A となる。)i が明らかの場合
得た知識を元にメッセージを偽造し、正しいメッ は、i を省略する。
セージとすり替えることが出来る。
X: 参加者を表すメタ変数
NX : X が作成したナンスを表す定数。
2.3
安全性
以下の3つの安全性を満たすプロトコルを生成す
る。
データの秘密性 秘密にすべきデータについて、デー
タ作成者の意図した相手以外にそのデータは知られ
ることのない性質。
KX : X の公開鍵を表す定数。
−1
KX
: X の秘密鍵を表す定数。
Mi : ステップ i で送受信されるメッセージを表す
定数。
Di : ステップ i で送受信されるデータを表す定数。
M : メッセージを表すメタ変数。
ものであることを受信者が確認できる性質。
N : ナンスを表すメタ変数。
K: 鍵を表すメタ変数。
受信確認 セッションで送信した全てのデータが、意
ナンス、データ、参加者の名前をアトミックメッ
データ認証
受信したデータが意図した相手からの
図した相手に正しく受信されたことを送信者が確認
セージと呼ぶ。
できる性質。
3.1.2
2.4
プロトコルの仕様
式
式は、プロトコルの構造を表す式と、性質を表す
生成するプロトコルの仕様は以下の項目からなる。 式に分けることができる。プロトコルの構造を表す
仕様は自動生成器に対する入力として与えられる。 式は、[5] から引用した。
• やり取りするデータの数。
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
3
プロトコルの構造を表す式
Di is warranted: ステップ i の受信者は、Di は意
M1
M2 : M1 が M2
の部分メッセージであることを表す。ここで、メッ 図した通信相手が意図したステップで送信したもの
セージ中で暗号化や署名に用いられる鍵は部分メッ であることを確認できる。(データ認証)
セージではない。以下のように帰納的に定義される。 Di is secret: データ Di はその作成者の意図する
相手以外に知られることはない。(データの秘密性)
• M M
• M
M ならば、M
{M }K
• M
M1 ならば、M
M1 M2 (M
推論規則
3.1.3
M2 M1 )
プロトコルの構造を表す式を導出する推論規則
プ
ロトコルの構造を表す式は以下の規則により導出さ
M1 N M2 : M1 は M2 の部分メッセージで、かつ、 れる。これらの規則は、[5] で導入された。
N が M2 の部分メッセージであるとき、N は M1 の (DA1)M から M を取り出すことが出来る。
みに出現することを表し、以下のように定義される。
i
• M
N
M
• M
N
M ならば、M
• M
N
M1 かつ N
(M
i
N
N
(DA2)M1 から M2 を取り出すことができ、M2 か
ら M3 を取り出すことが出来るならば、M1 から M3
{M }K
M2 ならば、M
M ↓R M
N
M1 M2
を取り出すことが出来る。
i
M2 M1 )
M1 ↓R M2 : ステップ i で R が M1 を受け取っ
た際、M1 から M2 という情報を取り出せる。
i R knows N : ステップ i 以前のメッセージか
ら、R は N を知ることができる。
M1 ↓R M2 i M2 ↓R M3
i M1 ↓R M3
(DA3)M から M1 と M2 の連接メッセージが取り出
すことが出来るならば、M から M1 を取り出すこと
が出来、かつ M から M2 を取り出すことが出来る。
i
i NS ↔ S: ステップ i で S は、自分の名前 S と
自分が作成したナンス NS を一緒に暗号化するか、S
を NS で暗号化して、相手に送信する。
i
−1
(DA4)R は KR
を知っているため、{M }KR から
M と(情報として)R を取り出すことが出来る。
プロトコルの性質を表す式
i N is not extracted:
イントルーダはステップ i までに送受信されたメッ
セージから N を得られない。
M ↓R M1 M2
M ↓R M j
{M }KR ↓R R ∧ i
i
{M }KR ↓R M
(DA5)R は KS を知っているため、{M }K −1 から
S
i
N is not known: N の作成者がステップ i ま
で実行した時点で、N はイントルーダに知られてお
らず、N の作成者とその意図した相手のみが知って
M と(情報として)S を取り出すことが出来る。
{M }K −1 ↓R S ∧ i
i
S
{M }K −1 ↓R M
S
(DA6)R が N を知っていれば、{M }N から M と
i M is addressed to NR : Mi のサブメッセージ (情報として)N を取り出すことが出来る。
M は、NR の作成者 R への宛先情報を含んでおり、
i R knows N
いる。
かつイントルーダによって偽造されることはない。
i R recognize (NS , NR ): NR を作成した受信者
R は、ナンス NS が意図した通信相手の作成したも
ので、セッションに対応したナンスであることをス
i
{M }N ↓R N ∧ i
{M }N ↓R M
(Knows1) イニシエータ A は NA を初めから知っ
ている。同様にレスポンダ B は NB を初めから知っ
ている。
テップ i で認識する。(R は S を認証する)
i A knows NA ∧ i B knows NB
i M is guaranteed: Mi のサブメッセージ M は、
イントルーダによる攻撃に対して耐性がある。つま (Knows2)i 以前のステップ j のメッセージから、R
i
りステップ i の受信者は、M は意図した通信相手が は N を取り出すことが出来る。
意図したステップで作成したものであることを確認
∃j < i j Mj ↓Ri N
出来る。
i Ri knows N
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
4
(B1) 送信者 Si は、ナンス NSi と名前 Si をメッセー 含む構造であれば、ステップ i + 1 のメッセージがイ
ジ {M }KRi に含めて相手に送信する。ここで、tagi ントルーダによって偽造されることはない。よって
はタグを表しており、メッセージがステップ i 用であ Ri がステップ i までしか実行しなければ、相手 Si も
るという情報を持つ。仮にプロトコルの中で {M }KRi
ステップ i までしか実行することが出来ない。i まで
という形のメッセージが一意的であるならば、tagi
のメッセージから NRi は漏れないため、Ri がステッ
は必要ない。他の規則でも同様である。
プ i まで実行した時点では NRi は秘密となる。
i
Mi ↓Ri {M }KRi i M ↓Ri NSi
i M ↓Ri Si i M ↓Ri tagi
i
i
NSi ↔ Si
i
(B2) 送信者 Si は、名前 Si を含むメッセージをナ
ンス NSi で暗号化して相手に送信する。
i
Mi ↓Ri {M }NSi i
i M ↓Ri Si i
i
NRi is not extracted i + 1 Mi+1 ↓Ri+1 {M }KRi+1
i + 1 M ↓Ri+1 NRi i + 1 M ↓Ri+1 tagi
NRi is not known
(K2)(K1) と同様
i
{M }NSi ↓Ri NSi
M ↓Ri tagi
Mi+1 ↓Ri+1 {M }K −1
NRi is not extracted i + 1
M ↓Ri+1 NRi i + 1
i+1
i
NSi ↔ Si
M ↓Ri+1 tagi
Si+1
NRi is not known
(K3)(K1) と同様
i
プロトコルの性質を表す式を導出する推論規則
プ
NRi is not extracted i + 1 Mi+1 ↓Ri+1 {M }NRi
i + 1 M ↓Ri+1 NRi i + 1 M ↓Ri+1 tagi
i
ロトコルの性質を表す式は、以下の規則により導出
NRi is not known
される。
(KK) ナンス N が、ステップ i + 1 まで実行した時
(NN) ナンス N がサブメッセージとして含まれなけ 点で秘密ならば、ステップ i の時点でも秘密である。
れば、イントルーダに漏れることはない。
i−1
N is not extracted N
i N is not extracted
i + 1 N is not known
i N is not known
Mi
(NS) ナンス NSi を相手の公開鍵 KRi で暗号化す
れば、相手 Ri 以外に漏れることはない。
i−1
NSi is not extracted {M }KRi
i M ↓Ri tagi
i
NS i
Mi
NRi is not extracted ∃j < i j NRi ↔ Ri
{M }KRi NRi Mi i M ↓Ri tagi
NRi is not extracted
i
i
NRi is not known i Mi ↓Ri {M }KRi
i M ↓Ri NRi i M ↓Ri tagi
NSi is not extracted
(NR) ナンス NRi をその作成者の公開鍵 KRi で暗
号化すれば、Ri 以外に漏れることはない。
i−1
(AD1) 秘密の NRi を含み Ri の公開鍵で暗号化さ
れた M を作成できるのは、通信相手は NRi を作成
した Ri であると信じている Si のみ。
{M }KRi is addressed to NRi
i
(AD2)NRi と Ri を含み Si の署名がなされた M を
作成できるのは、通信相手は NRi を作成した Ri で
あると信じている Si のみ。
Mi ↓Ri {M }K −1 i
i
Si
i
(K0) メッセージを送受信していなければ、ナンス
は漏れない。
0
N is not extracted
M ↓Ri Ri i
N is not extracted k は最終ステップ
k N is not known
M ↓Ri tagi
{M }K −1 is addressed to NRi
i
Si
(AD3)Ri を含み秘密の NRi で暗号化された M を
作成できるのは、通信相手は NRi を作成した Ri で
(KL) 全てのメッセージから N が漏れることがなけ あると信じている Si のみ。
れば、セッションを通して N は秘密である。
i NRi is not known i
k
M ↓Ri NRi
i
i
M ↓Ri Ri i
Mi ↓Ri {M }NRi
M ↓Ri tagi
{M }NRi is addressed to NRi
(K1) ステップ i まで実行した時点で NRi が秘密で
(AD4) 既に Si が NRi とその持ち主の名前 Ri の対
あり、ステップ i + 1 のメッセージが NRi とタグを
応を認識しているのであれば、秘密の NRi で暗号化
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
された M を作成できるのは、通信相手は NRi を作
成した Ri であると信じている Si のみ。
NRi is not known ∃j < i j NRi ↔ Ri
i Mi ↓Ri {M }NRi i M ↓Ri tagi
i
i
{M }NRi is addressed to NRi
(AD5)M を作成したのは、通信相手は NR1 i を作成
2
した Ri であると信じている Si であり、M に NR
i
が含まれるならば、M を作成できるのは通信相手は
NR2 i を作成した Ri であると信じている Si のみで
ある。
i
1
M is addressed to NR
i
i
i
2
M ↓Ri NR
i
2
M is addressed to NR
i
(REC1)M を作成できるのは、通信相手を NRi を
(GS3) タグを含み、受信者がセッションとの対応
を認識する送信者のナンス NSi で暗号化されたメッ
セージは、意図した通信相手が意図したステップで
送信したものであることを確認できる。i が最終ス
テップの場合は i + 1
NSi is not known i Mi ↓Ri {M }NSi
i M ↓Ri tagi i {M }NSi ↓Ri NSi
Ri recognize (NSi , NRi ) i + 1 M is guaranteed
i
∃j j
i
送信したものであることを確認できる。
i
スであることを認識する。
Ri recognize (NSi , NRi ) ∧ i
M is guaranteed
(REC2)(REC1) によって Si が NRi が意図した相
手のナンスであることを確認した後、NRi を返送す
ることによって、Ri は NSi が Si の作成したナンス
{M }KRi is guaranteed
(GR2) 送信者がセッションとの対応を認識した、受
信者のナンス NRi 、受信者の名前 Ri 、タグを含む署
名メッセージは、意図した通信相手が意図したステッ
プで送信したものであることを確認できる。
i
Mi ↓Ri {M }K −1 i
Si
M ↓Ri NRi
i M ↓Ri tagi i M ↓Ri Ri
∃j < i j Si recognize (NRi , NSi )
i M is addressed to NRi
∃j < i j Si recognize (NRi , NSi )
Ri recognize (NSi , NRi ) ∧ i
NRi is not known i Mi ↓Ri {M }KRi
i M ↓Ri NRi i M ↓Ri tagi
∃j < i j Si recognize (NRi , NSi )
i
であることを確認できる。
i
{M }NSi is guaranteed
(GR1) 送信者がセッションとの対応を認識した、
受信者の秘密のナンス NRi と、タグを含む暗号メッ
セージは、意図した通信相手が意図したステップで
受信者 Ri は、NSi はそのような Si の作成したナン
i
M is guaranteed の条件は必
要ない。
作成した Ri であると信じている Si のみであるため、
(ステップ i 以前に Ri が送信した全ての NRi について)
i M is addressed to NRi i M ↓Ri NSi
5
i
{M }K −1 is guaranteed
Si
M is guaranteed
(GR3) タグを含み、送信者がセッションとの対応
(GS1) 受信者がセッションとの対応を認識する送
を認識した受信者のナンス NRi で暗号化されたメッ
信者の秘密のナンス NSi と、タグを含む暗号化メッ
セージは、意図した通信相手が意図したステップで
セージは、意図した通信相手が意図したステップで
送信したものであることを確認できる。
送信したものであることを確認できる。i が最終ス
i NRi is not known i Mi ↓Ri {M }NRi
テップの場合は i + 1 M is guaranteed の条件は必
i
要ない。
i
M ↓Ri tagi ∃j < i j
i
Si recognize (NRi , NSi )
{M }NRi is guaranteed
NSi is not known ∃j j Ri recognize (NSi , NRi )
i Mi ↓Ri {M }KRi i M ↓Ri NSi
i M ↓Ri tagi i + 1 M is guaranteed
た通信相手が意図したステップで作成したものであ
{M }KRi is guaranteed
ることを確認できるため、Mi に含まれる Di も意図
i
(WAR)Mi のサブメッセージである M は、意図し
(GS2) 受信者がセッションとの対応を認識する送信 した通信相手が意図したステップで作成したデータ
者のナンス N と、タグを含む署名メッセージは、 であることを受信者は確認できる。
Si
i
意図した通信相手が意図したステップで送信したも
のであることを確認できる。
i
i
Mi ↓Ri {M }K −1 i
M ↓Ri tagi ∃j j
i
M ↓Ri NSi
(SEC1)Di は一度しか送受信されないため、相手の
Ri recognize (NSi , NRi )
公開鍵で暗号化すればイントルーダに漏れることは
Si
{M }K −1 is guaranteed
Si
M is guaranteed i M ↓Ri Di
Di is warranted
ない。
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
6
やり取りされるメッセージの暗号化コストや量的
{M }KRi
Di
コストはプロトコルの評価基準として一般的である
Mi
が、本稿ではこれに加え、攻撃が検出される時期に
Di is secret
対してコスト基準を導入する。
(SEC2)Di が送信者の作成した秘密のナンス NSi
で暗号化されていれば、イントルーダに漏れること
はない。(k は最終ステップ)
NSi is not known
k
本稿で生成するプロトコルは 2.3 節の安全性を満
たしているため、攻撃者によってメッセージすり替
え等の攻撃が行われたとしても、セッション参加者
{M }NSi
Di
Mi
Di is secret
は必ずこれを検出することが出来る。しかし、その
検出時期はプロトコルごとに異なり、全ての攻撃を
即座に検出できるプロトコルもあれば、ある特定の
(SEC3)Di が認証した相手の秘密のナンス NRi で
攻撃に関しては後のステップでしか検出できないプ
暗号化されていれば、イントルーダに漏れることは
ロトコルもある。このような違いをコスト基準とし
ない。(k は最終ステップ)
て導入した。本稿では、より早く攻撃を検出できる
k
NRi is not known {M }NRi Di Mi
∃j < i j Si recognize (NRi , NSi )
Di is secret
プロトコルの方が良いプロトコルであるという立場
をとる。
3.3
自動生成法
本節では 3.1 節で示した論理を利用した、プロト
安全性を表す式
3.1.4
本節では、本論理においてどのように 2.3 節の安
全性を表現しているかを述べる。
コルの自動生成法を示す。まず初めに生成に必要な
入力について述べ、その後プロトコルの生成手続き
を示す。
データの秘密性 Di is secret が導出されればステッ
プ i で送受信されるデータ Di の秘密性が保証され
る。
3.3.1
入力
まず、2.4 節で挙げたプロトコルの仕様を以下のよ
データ認証 やり取りされる全てのデータ Di につい
うに形式化し、入力として与える。やり取りするデー
て Di is warranted が導出されれば、データ認証が満
タの数とデータを送信し始める側が決定されれば、そ
たされる。
のために必要なプロトコルの最小ステップ数が決定
受信確認 受信確認を満たすためには、データのやり
されるため、これをプロトコルのステップ数とする。
取りが終わった後(データを含まない)確認メッセー
これによりデータが送受信されるステップも決定さ
ジを送受信すればよい [4]。よってやり取りしたいデー
れる。
M is guaranteed step, Data, Secret :プロトコルの仕様
が導出されれば受信確認が満たされる。
step: プロトコルのステップ数
タが Dk まで存在する場合、k + 1
Data:
3.2
プロトコルに対するコスト評価
本稿では、以下のコスト評価基準に基づきプロト
コルを評価し、使用環境に適したプロトコルを選別
する。
• メッセージの暗号化コスト
• メッセージの署名操作コスト
• メッセージの量的コスト
• 攻撃の検出時期コスト
Secret:
データを送受信するステップ番号の集合
秘密にしたいデータが送受信されるステップ番
号の集合。Data の部分集合
さらに 3.2 節のコスト基準に対するコスト重みを
入力として与えることで、3.2 の基準のうちどの基準
を重視するかを指定することが出来る。つまり、コ
スト重みによってプロトコルが使用される環境が表
現される。
3.3.2
生成手続き
プロトコルの生成手続きについて述べる。この生
成法では、仕様と安全性を両方とも満たす構造を持
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
つメッセージを元に、安全なプロトコルのみを生成
する。
7
呼ぶ。
イントルーダストランドは、攻撃者が行える全て
(1) メッセージ生成器によりステップ i のメッセージ の振る舞いを考慮する必要があるため、攻撃者の行
候補をコスト昇順に自動生成する。このメッセージ える基本動作の組み合わせで定義する。基本動作はア
トミックメッセージの生成、メッセージの消失、メッ
候補はプロトコルの仕様を満たしている。
(2) 生成されたメッセージ候補から、ステップ i に関 セージの二重化、連結、分解、鍵使用、暗号化、復
する安全性の式が導出されるかを、推論規則を用い 号化(署名)であり、これらを組み合わせることに
て調べる。候補メッセージをコスト昇順に調べるこ より、2.2 節で定義した攻撃者の可能な行為を全て表
とで、安全性の式が導出される最小コストメッセー 現できる。
生成されるプロトコルのストランド空間について、
ジをステップ i の送受信メッセージとして採用する。
(3) 全てのステップの送受信メッセージを決定し、プ 以下の変数を定義する。
a, b, · · · : 参加者の名前を表す変数
ロトコルが生成される
na , nb , · · · : a, b, · · · の作成したナンスを表す変数
以上の手続きにより、一つの安全なプロトコルが
生成されるが、相手を認証するステップ等、仕様とし
て与えられていない条件を変更することで、一つの
入力から複数の安全なプロトコルが生成される。本
生成法では、得られる可能性のあるプロトコルを全
て生成する。その後プロトコル全体に対するコスト
評価を行い、最小コストプロトコルを出力する。
d1 , d2 , · · · : やり取りされるデータを表す変数
パラメータを利用してストランドを表記すること
も出来る。例えば、イニシエータの名前 a、レスポン
ダの名前 b、イニシエータのナンス na 、レスポンダ
のナンス nb 、やり取りするデータ d1 , d2 であるセッ
ションにおける、高さ i のイニシエータストランド
を INI(a, b, na , nb , d1 , d2 )i 、レスポンダストランドを
RES(a, b, na , nb , d1 , d2 )i と表記する。さらに ∗ を利
用した省略形を定義する。
∪
本節では、本生成法により生成されたプロトコル
INI(a, b, na , ∗) = nb INI(a, b, na , nb )
は、安全性を満たすことを示す。つまり、3.1 節で示 ∗ は任意の値を表しており、どのような値が入っても
した推論規則の健全性をストランド空間 [3] における 構わない。本稿ではしばしば、やり取りするデータ
本生成法の正当性
4
意味に基づき証明する。
を省略したストランド表記を用いるが、その場合も
データの値は任意である。
4.1
ストランド空間
本稿で扱うストランド空間の定義は [3] に従う。ス
トランドとは符号付メッセージの列である。ストラン
4.2
ストランド空間における式の意味
式に対して、ストランド空間における意味を与え
ドはスレッドのようなもので、参加者によって順番に る。プロトコルの構造を表す論理式の持つ意味は、そ
送受信されるメッセージの列を表す。符号付メッセー のような構造を持つプロトコルのストランド空間を
ジは +M と −M のどちらかであり、+M によって
考慮しているという意味でしかないため、ここではプ
メッセージ M の送信を表し、−M によってメッセー
ロトコルの性質を表す式に対してのみ意味を与える。
ジ M の受信を表す。ストランドに現れるこれらの符
号付メッセージをノードと呼ぶ。例えば +M1 , −M2
i
N is not extracted: N がイニシエータのナン
スの場合を考える。高さ i + 1 以上の INI(a, b, na , ∗)
はストランドであり、初めのノードで M1 を送信し、 が存在せず、かつ高さ i + 1 以上の RES(∗, b, na , ∗) も
二番目のノードで M2 を受信する。また、ストランド 存在しなければ、na を知っている可能性のあるレギュ
の持つノードの総数をそのストランドの高さと呼ぶ。 ラーストランドは INI(a, b, na , ∗) と RES(∗, b, na , ∗)
また、攻撃者でない正当な参加者の振る舞いを表
のみであり、かつ +na をノードとして持つイント
すストランドをレギュラーストランド、攻撃者の振
ルーダストランドは存在しない。N がレスポンダの
る舞いを表すストランドをイントルーダストランド
ナンスの場合も同様。
と呼ぶ。また、イニシエータの振る舞いを表すスト
i N is not known: N がイニシエータのナンスの
ランドをイニシエータストランド、レスポンダの振 場合を考える。高さ i + 1 以上の INI(a, b, na , ∗) が存
る舞いを表すストランドをレスポンダストランドと 在しないならば、na を知っている可能性のあるレギュ
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
ラーストランドは INI(a, b, na , ∗) と RES(∗, b, na , ∗) 4.3
8
推論規則の健全性
のみであり、かつ +na をノードとして持つイント
3.1 節の推論規則が、式に与えられたストランド空
ルーダストランドは存在しない。N がレスポンダの 間における意味を保存することを証明する。これに
ナンスの場合も同様。
より、定理 1 が示され推論規則の健全性が示される。
i
M is addressed to NR : ステップ i ではイニシ
対象プロトコルの条件より、考慮するストランド
エータが受信側とする。i 番目のノードに、M を含む 空間では以下の性質が成立すると仮定する。これは、
メッセージの受信ノードを持つ INI(a, b, na , ∗)i が存 正当な参加者がセッションで作成するナンスは新規
在するならば、i 番目のノードに M を含むメッセージ なもので、以前に使用されたものを使用することは
の送信ノードを持つ、高さ i 以上の RES(a, b, na , ∗) ないという意味である。
が存在する。レスポンダが受信側の場合も同様。
仮定 1 (ナンスの新規性) あるストランド空間にレ
i R recognize (NS , NR ): ステップ i ではイニシ
ギュラーイニシエータストランド INI(a, b, na , nb ,
エータが受信側とする。INI(a, b, na , nb )i が存在する
d1 , · · ·) と、レギュラーイニシエータストランド INI
ならば、高さ i 以上の RES(a, b, na , nb ) が存在する。
(a , b , na , nb , d1 , · · ·) が存在するならば、a = a , b =
レスポンダが受信側の場合も同様。
b , nb = nb , d1 = d1 , · · · が成立する。同様に、ある
i M is guaranteed: ステップ i ではイニシエータ
ストランド空間にレギュラーレスポンダストランド
が受信側とする。i 番目のノードに、M を含むメッ
RES(a, b, na , nb , d1 , · · ·) と、レギュラーレスポンダ
セージの受信ノードを持つ INI(a, b, na , nb )i が存在
ストランド RES(a , b , na , nb , d1 , · · ·) が存在するな
するならば、i 番目のノードに M を含むメッセージ
らば、a = a , b = b , na = na , d1 = d1 , · · · が成立
の送信ノードを持つ、高さ i 以上の RES(a, b, na , nb )
する。
が存在する。
※ただし、a による b の認証が i より後のステップ j (K1) の証明:NRi はイニシエータが作成したナンス
で行われる場合、この式の意味は以下のようになる であるとすると、ステップ i ではイニシエータが受信
ステップ i ではイニシエータが受信側とする。i 番目 側となる。今、INI(a, b, na , ∗)i が存在するとする。仮
のノードに、M を含むメッセージの受信ノードを持 にまだ RES(∗, b, na , ∗) の高さが i 以下であるとする
つ INI(a, b, na , nb )j が存在するならば、i 番目のノー と、i NRi is not extracted より、na を知っている
ドに M を含むメッセージの送信ノードを持つ、高さ 可能性のあるレギュラーストランドは INI(a, b, na , ∗)i
j 以上の RES(a, b, na , nb ) が存在する。レスポンダが と RES(∗, b, na , ∗) のみであり、かつ +na をノードと
受信側の場合も同様。
して持つイントルーダストランドは存在しない。こ
Di is warranted: ステップ i ではイニシエータが受 こで、ステップ i + 1 ではイニシエータが送信側であ
信側とする。i 番目のノードに、di を含むメッセージ り、ステップ i + 1 で送受信されるメッセージにはタ
の受信ノードを持つ INI(a, b, na , nb , di )i が存在する グと秘密の na が含まれるため、イントルーダがこの
ならば、i 番目のノードに di を含むメッセージの送 メッセージの送信ノードを持つことはない。よって
信ノードを持つ、高さ i 以上の RES(a, b, na , nb , di ) RES(∗, b, na , ∗) の高さが i + 1 以上になるためには、
が存在する。加えて、受信者はステップ i の送受信 高さ i + 1 以上の INI(a, b, na , ∗) が存在しなければな
メッセージから di を取り出すことが出来る。レスポ らない。つまり、高さが i+1 以上の INI(a, b, na , ∗) が
ンダが受信側の場合も同様。
存在しないならば、高さ i + 1 以上の RES(∗, b, na , ∗)
Di is secret: ステップ i ではイニシエータが送信 は存在しないことになる。今、INI(a, b, na , ∗) の高さ
側とする。i 番目のノードに di を含むメッセージの は i であることと i NRi is not extracted より、na
送信ノードを持つ INI(a, b, na , nb , di ) が存在するな を知っている可能性のあるレギュラーストランドは
らば、di を知る可能性のあるレギュラーストランド INI(a, b, na , ∗) と RES(∗, b, na , ∗) のみであり、かつ
は RES(∗, b, ∗, ∗, di ) のみで、かつ +di をノードとし +na をノードとして持つイントルーダストランドは
て持つイントルーダストランドは存在しない。レス 存在しない。
ポンダが受信側の場合も同様。
(GR1) の証明:ステップ i ではイニシエータが受
信側とする。i 番目のノードに、{M }Ka を含むメッ
セージの受信ノードを持つ INI(a, b, na , nb )i が存在
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
9
NRi is not known より 使用する。そして、安全性を満たしたプロトコルの
INI(a, b, na , nb )i 以外に na を知っている可能性があ みを出力する。この生成法では、大量のプロトコル
るのは RES(∗, b, na , ∗) のみであり、i M ↓Ri NRi に対して検証を行う。これに対し本稿で提案した自
より RES(∗, b, na , ∗) が存在する。さらに M が a の 動生成法では、安全性が保証されているメッセージ
公開鍵で暗号化されていることから RES(a, b, na , ∗) 構造を元に設計を行うため、安全なプロトコルのみ
するとする。この時、i
M ↓Ri tagi より高さ i 以上の を効率的に生成することが出来る。
RES(a, b, na , ∗) が存在することになる。ここで j <
i. j Si recognize (NRi , NSi ) より、高さ j 以上の 5.2 束縛関係に基く検証法
INI(a, b, na , ∗) が存在することになるが、ナンスの新
これは [5] にて提案された。推論規則によって、プ
規性より INI(a, b, na , ∗) は INI(a, b, na , nb ) であるた ロトコルの構造から直接的にプロトコルの秘密性や
が存在し、i
め、RES(a, b, na , nb ) が存在しなければならない。以 認証を検証する。束縛関係とは、ナンス等のメッセー
上より i 番目のノードに {M }Ka を含むメッセージ ジ間の対応関係のことである。ある参加者が相手を
の送信ノードを持つ、高さ i 以上の RES(a, b, na , nb ) 認証するということは、相手の名前やナンスを自分
が存在する。これ以外の規則に対する証明は、本稿 の名前やナンスと対応づけることと見なせるため、こ
では省略する。
定理 1 全ての Di について Di is warranted が導出
されるとする。また、やり取りするデータが Dk まで
存在し、ステップ k ではイニシエータが受信側であ
るとする。この時 INI(a, b, na , nb , d1 , d2 , · · · , dk )k が
存在するならば、高さ k 以上の RES(a, b, na , nb , d1 ,
の対応関係に基づいて認証を検証する。束縛関係に
関する推論規則では、本稿で提案した推論規則と同
様、プロトコルの静的な構造から安全性を検証する
ことができる。よって、これを利用してプロトコル
の自動生成を行うことも可能である。しかし束縛関
係に基く推論規則を用いた場合では、生成されない
ようなプロトコルが存在する。束縛関係に基く推論
d2 , · · · , dk ) が 存 在 す る 。逆 に ス テップ k で は レ
規則では、ナンスの秘密性に関する導出を行った後
スポンダが受信側であるとすると、RES(a, b, na ,
にこれを利用して認証を導くことや、ナンスの秘密
nb , d1 , d2 , · · · , dk )k が存在するならば、高さ k 以上
性に対する要件が厳しすぎるという理由から、ナン
の INI(a, b, na , nb , d1 , d2 , · · · , dk ) が存在する。
スを秘密共有しないプロトコルやセッション途中ま
これはストランド空間における agreement プロパ
でしかナンスを秘密保持しないようなプロトコルは
ティである [3]。agreement プロパティは、あるスト
生成されない。本稿の手法でも、生成されないプロ
ランドに対してそのパラメータと高さが一致した相
トコルが存在するが、本手法ではより厳密にナンス
手ストランドの存在を保証するものであり、認証の
の秘密性について調べており、そのようなプロトコ
形式化のひとつである。
ルでも生成出来るものがある。
関連研究との比較
5
6
まとめ
本節では関連研究との比較を行う。関連研究の特
本稿では、二者間データ通信のための安全なプロ
徴に触れながら、本稿で提案した自動生成法の利点
トコルの自動生成法を提案した。これにより、使用環
について言及する。
境に適した安全なプロトコルを効率的に自動生成出
来るようになった。また、関連研究との比較を行い、
5.1
Automatic Protocol Generator
[1] にて提案された自動生成法で、2 者間で認証を
行いセッション鍵を秘密共有するためのプロトコル
を自動生成する。まず、プロトコル生成器により、入
力として与えられた仕様を満たすプロトコルを大量
に生成し出力する。次に、得られたプロトコル群をプ
ロトコル自動検証器にて検証し、安全性を満たすプ
ロトコルを選別する。自動検証器には Athena[2] を
本生成法の特徴について述べた。近年ではインター
ネット上において様々なサービスが行われており、求
められる安全性も様々である。例えば、web サーバに
対して過剰に接続し、サーバを動作不能にするサー
ビス拒否攻撃と呼ばれる攻撃も多く報告されており、
このような攻撃に対する耐性も求められている。こ
のような、秘密性、認証以外の安全性も取り入れる
ことが今後の課題である。
日本ソフトウェア科学会第 22 回大会(2005 年度)論文集
参考文献
[1] Adrian Perrig Dawn Song. Looking for diamonds in
the dessert — extending automatic protocol generation to three-party authentication and key distribution. In Proc. of IEEE Computer Security Foundation Workshop, 2000.
[2] S.Berezin D.Song and A.Perrig. Athena: a novel approach to efficient automatic security protocol analysis. Journal of Computer Security, Vol. 9, No. 1,
pp. 47–74, 2001.
[3] F. Javier Thayer F´
abrega, Jonathan C. Herzog, and
Joshua D. Guttman. Strand spaces: Proving security protocols correct. Journal of Computer Security, Vol. 7, pp. 191–230, 1999.
[4] 根岸和義, 米崎直樹. セキュリティプロトコルの一貫性
および正常終了一致の同一参加者による複数セッショ
ンを考慮した検証法. 情報処理学会論文誌, Vol. 41,
No. 8, pp. 2281–2290, 2000.
[5] 萩谷昌己, 竹村亮, 高橋孝一, 斉藤孝道. 束縛関係に基
づく認証プロトコルの検証. コンピュータソフトウェ
ア, Vol. 20, No. 3, pp. 17–29, 2003.
10