セキュリティプロトコルの形式検証のパターン化について

セキュリティプロト コルの形式検証のパターン化について
塚
田
章†
恭
形式検証のパターン化は，検証の再利用性の向上や効率化に資すると期待される．本稿では，対象
をセキュリティプロトコルの形式検証に限定し，形式検証のパターン化について考察する．特に，電
子投票を例題として，セキュリティ要件記述のパターン化に向けたアプローチについて論じる．
1. は じ め に
間の観測等価性（ observational equivalence ）によっ
電子商取引や電子投票で用いられる暗号通信プロト
て要件が記述される．第 3 に，これら形式的に記述さ
コル（セキュリティプロトコル）には高い信頼性が求
れたプロトコル本体が，形式的に記述されたセキュリ
められる．1980 年代以降，セキュリティプロトコル
ティ要件を満たすことを，実際に検証する枠組みが必
の安全性を形式手法によって証明するための様々な理
要である．ここでは定理証明器やモデル検査器などが
論的枠組み（ Dolev-Yao モデル 4) ，BAN 論理2) ，スト
しばしば利用される．
ランド 空間5) ，帰納的手法12) ，spi 計算1) など ）が提
第 1 のプロトコル本体記述においても，セキュリ
案され，有用なツールが多数開発された．これらの古
ティプロトコルというド メインの特徴を記述言語に反
典的なアプローチを発展させ，暗号の脆弱性も考慮に
映させることにより，一定のパターン化が期待できそ
入れた新しい形式手法を確立しようとする動きも，近
うである☆☆ ．第 3 の検証においても，例えば定理証
6)
年盛んである ．本稿では，セキュリティプロトコル
明系では証明戦略や証明上の定石などにパターンを導
にド メインを限定し，形式検証のパターン化の可能性
入することが考えられる．本稿では，第 2 のセキュリ
について論じる☆ ．
ティ要件の記述に焦点をあてる．セキュリティプロト
2. 形式検証の 3 段階とそのパターン化
一般の計算機ソフトウェアの場合と同様，セキュリ
ティプロトコルの形式検証も概して 3 つの段階から構
成される．第 1 に，各プロトコル本体を形式的に記述
する必要がある．この際，用いられる形式手法に応じ
コルには一般に多種多様な安全性が求められるため，
これらをパターン化し再利用可能な形で整理しておく
ことは，プロトコルの設計者・開発者にとって有意義
であると考えるからである．
3. セキュリティ要件記述のパターン化
て，様々なプロトコル記述体系が利用される．BAN
具体例として電子投票プロトコルを取り上げる．用
論理ではいわゆるアリス・ボブ記法であり，spi 計算
途や実現方式の違いにより求められる安全性に多少
では spi 計算のプロセス式といった具合である．第 2
のバリエーションもあるが，以下の性質が基本的であ
に，検証すべき性質（セキュリティ要件）が形式的に
る11) :
記述されている必要がある．ここでも様々な要件記述
(1)
体系が用いられる．BAN 論理では信念論理により認
証についての要件が記述され，spi 計算ではプロセス
公平性（ fairness ）: 選挙が終了するまで，誰も
投票の途中経過を知ることができない．
(2)
適格性（ eligibility ）: 選挙管理簿に登録され
ている有権者のみが投票権を持ち，1 回のみ投票で
† 日本電信電話（株），NTT コミュニケーション科学基礎研究所
当然のことながら，ここでの議論を計算機ソフトウェア全般の
形式検証に一般化する場合には注意が必要である．セキュリティ
プロトコルは，分散ソフトウェアの一種であり，プロトコル本体
の記述が比較的簡易であっても，通信参加者数の非有界性・攻撃
者の振舞いの多様性・セッションの並行実行などにより，検証対
象となる状態遷移モデルのサイズは莫大なものになりやすいと
いう特徴を持つ．
☆
きる．
(3)
☆☆
匿名性／プライバシ（ anonymity/privacy ）: 誰
た だし ，セ キュリ ティプ ロト コ ル に お い て は ，NeedhamSchroeder プロトコル 8) の例にも見られるように，本体記述の
微妙な差異がしばしば安全性の決定的差異につながることを把
握しておく必要がある．
が誰に投票したかが秘匿される．
成する際，部品プロトコルのセキュリティが合成後も
個別検証可能性（ individual verifiability ）: 投
保証される枠組みについての研究が盛んである10) ．こ
票者は自分の投票がカウントされていることを検証
れらの研究成果が提供する検証のモジュラー性を，形
(4)
可能である．
(5)
総合検証可能性（ universal verifiability ）: 最
終的に公開された結果が全ての投票を正しくカウン
トしていることを検証可能である．
(6)
無証拠性（ receipt-freeness ）: 誰に投票したか
の証拠を投票者は示すことができない．投票の買収
を防ぐのに有効とされる．
(7)
耐強制性（ coercion-resistance ）: 強制的に介
入する攻撃者に対しても，投票者は誰に投票したか
の証拠を示すことができない．
これらは，適切な検証モデル上でフォーマルに記述す
ることが現在では可能となっており，実際にさまざま
な電子投票プロトコルの形式検証が行われている3),7) ．
検証性質のパターン化を可能にするためには，次の
2 つが重要な視点であると考える．第 1 に，これら検
証すべき性質の間の関係を論理的に明らかにすること
が必要である．例えば，匿名性／プライバシ，無証拠
性，耐強制性は，この順に徐々に強くなっていくとい
う論理的関係にあると報告されている3) ．すなわち，
これらは別個の 3 種の要件ではなく，あるひとつのパ
ターンから生成された（セキュリティの度合いの異な
る）3 つのインスタンスと考えることができる．第 2
に，これらの性質を，ある具体的な電子投票プロトコ
ルに特化して記述するのではなく，抽象度が高く汎用
性の高い記法によって記述しておくことが望ましい．
これにより，電子投票プロトコルと，例えば（機能は
異なるが類似点も多い）内部告発用社内掲示板システ
ムとが，パターンを共有して形式検証可能となる可能
性が開ける．
我々は，匿名性／プライバシに関連する性質の周辺
で，上記 2 点についていくばくかの検討を行っている．
第 1 の視点については，匿名性／プライバシを，匿名
性（「誰が投票したか」が秘匿される性質）とプライ
バシ（「誰に投票したか」が秘匿される性質）という
2 つの性質に精製・分解し，これらが役割交換可能性
と呼ばれる別の基本的性質から対称性を伴って導出さ
れることを示している9) ．第 2 の視点については，匿
名性とプライバシを知識論理（ epistemic logic ）と呼
ばれる論理体系を用いて高い抽象度で記述・表現し ，
その汎用性について議論している9),13) ．
4. お わ り に
全体プロトコルをいくつかの部品プロトコルから合
式検証のパターン化と併用することは，複雑なシステ
ムをセキュアかつ効率的に開発するための有望なアプ
ローチのように思える．
謝辞 河辺義信，櫻田英樹，真鍋義文，真野健，藤
田邦彦の各氏に謹んで感謝の意を表する．
参 考 文 献
1) Abadi, M. and Gordon, A. D.: A Calculus for
Cryptographic Protocols: The Spi Calculus, Inform. Comput., Vol. 148, No. 1, pp. 1–70 (1999).
2) Burrows, M., Abadi, M., and Needham, R.M.:
A Logic of Authentication, ACM Trans. Comput. Syst., Vol. 8, No. 1, pp. 18–36 (1990).
3) Delaune, S., Kremer, S., and Ryan, M.: Verifying Privacy-Type Properties of Electronic Voting Protocols, J. Computer Security (to appear).
4) Dolev, D. and Yao, A.: On the Security of
Public Key Protocols, IEEE Trans. Inform.
Theory, Vol. 29, No. 2, pp.198–207 (1983).
5) Thayer Fábrega, F. J., Herzog, J. C., and
Guttman, J. D.: Strand Spaces: Proving Security Protocols Correct, J. Comput. Security,
Vol. 7, Nos. 2–3, pp.191–230 (1999).
6) 萩谷昌己: 数理的技法による情報セキュリティの
検証, 応用数理, Vol. 17, No. 4, pp. 8–15 (2007).
7) Kawabe, Y., Mano, K., Sakurada, H., and
Tsukada, Y.: On Backward-Style Anonymity
Verification, IEICE Trans. Fundam. Electron.
Commun. Comput. Sci., Vol. E91-A, No. 9,
pp. 2597–2606 (2008).
8) Lowe, G.: Breaking and Fixing the NeedhamSchroeder Public-Key Protocol Using FDR,
Software—Concepts and Tools, Vol. 17, No. 3,
pp.93–102 (1996).
9) Mano, K., Kawabe, Y., Sakurada, H., and
Tsukada, Y.: Role Interchangeability and Verification of Electronic Voting, Proc. SCIS’06,
4D2-1 (2006).
10) 岡本龍明: はん用的結合可能性と数理的技法, 信
学誌, Vol. 90, No. 6, pp. 451–456 (2007).
11) 岡本龍明, 山本博資: 現代暗号, 産業図書 (1997).
12) Paulson, L. C.: The Inductive Approach to
Verifying Cryptographic Protocols, J. Comput.
Security, Vol. 6, Nos. 1–2, pp. 85–128 (1998).
13) Tsukada, Y., Mano, K., Sakurada, H., and
Kawabe, Y.: Anonymity, Privacy, Onymity,
and Identity: A Modal Logic Approach, Proc.
PASSAT-09 (to appear).