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

日本ソフトウェア科学会第 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,yonezaki}@fmx.cs.titech.ac.jp
近年のインターネット上での重要な取引の増加に伴い、安全なプロトコルが必要不可欠となっている。本稿
では二者間データ通信のためのセキュリティプロトコル自動生成法を提案する。これは、プロトコルの構造
から安全性を導出する推論規則を利用し、安全なプロトコルのみを生成する手法である。また、プロトコル
に対するコスト評価を行うことで、使用環境に適したより良いプロトコルを生成する。さらに、他の自動生
成方式と比較することで、本稿で提案する自動生成法の利点についても議論する。
1
はじめに
個人情報や商取引に関する重要データがネットワー
ける意味に基づいて証明する。最後に、他の自動生
成法との比較も行う。
クを通じて伝達されるようになった現在、これらの
通信上のセキュリティを守るためには、暗号化技術
準備
2
が必須であるが、それだけでは十分ではない。たと
本稿で自動生成の対象としているプロトコルの性
え、暗号化技術が完全であっても、伝送手順である
質や、想定する攻撃者の振る舞い、プロトコルが満
プロトコルに欠陥があればメッセージのすり替えや
たすべき安全性等を定義する。
成り済まし攻撃を受ける可能性がある。よって、プ
ロトコルの安全性を形式的に検証する技術が必要で
ある。しかし、検証のコストを考えると、これまで
は非形式的に行われてきたプロトコルの設計を形式
的に行うアプローチの方が現実的である。
そこで本稿では、二者間でデータ通信を行うため
のセキュリティプロトコルの自動生成法を提案する。
2.1
生成対象プロトコル
• 2 者間でデータをやり取りするためのプロトコ
ルを生成する。データとは、ナンスや参加者の
名前とは異なるメッセージで、これをお互いに
通達することをプロトコルの目的とする。
この生成法では安全性が保証されているメッセージ
• 参加者は受信したデータを返送することはない。
構造を元に、安全なプロトコルのみを生成する。ま
• データは必ず交互にやり取りする。
た、プロトコルに対する静的なコスト評価を行うこ
とで、使用環境に適したセキュリティプロトコルを
選別する。
以下ではまず前提条件を示した後、プロトコルの
構造から安全性を推論するための推論規則を導入す
る。そしてこれを利用した自動生成手続きを示す。さ
らにこの推論規則の健全性をストランド空間 [3] にお
• １つの送受信メッセージに対して、同じ鍵で二
度以上の暗号化、署名操作は行わない。
• ナンスは必ずセッションに対応付けて使用する。
（自分の作成したナンスとセッションとの対応を、
相手に認識させる）
日本ソフトウェア科学会第 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
安全性
以下の３つの安全性を満たすプロトコルを生成す
る。
データの秘密性秘密にすべきデータについて、デー
タ作成者の意図した相手以外にそのデータは知られ
ることのない性質。
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 eﬃcient 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

Download Report