SET支払いプロトコルの秘匿性検証(セキュリティプロトコル・電子公証)(<特集>新たな脅威に立ち向かうコンピュータセキュリティ技術)  [in Japanese] Verification of Secrecy of the SET Payment Protocol(Security Protocols and Electronic Notary Public)(<Special Issue on Computer Security>Combating Emerging Threats)  [in Japanese]

セキュリティ・プロトコルの安全性を証明によって検証する論理的検証は,プロトコル仕様記述の柔軟性と検証の完全性の点で優れている.特にPaulsonによる帰納的方法は,実際に使用されているプロトコルの検証の実績があり,証明スクリプトも公開されている.しかしこの方法では大きなプロトコル仕様記述が繁雑になりやすいという欠点があった.本論文ではプロトコル仕様を簡潔に記述する言語と,この言語で記述したプロトコル仕様を帰納的方法の論理式に変換する方法を提案する.これにより大きなプロトコルを検証する際にも帰納的方法の証明スクリプトの多くをそのまま利用でき,検証を効率的に行うことができる.本論文ではさらに,これをSET(Secure Electronic Transaction)の支払いプロトコルの検証に適用し,カード番号の秘匿性を検証することができた.その際,検証を現実的な時間内で可能にするために,検証を目指すセキュリティから参照されない部分を省略して簡略化されたプロトコル仕様を得た.

To verify security protocols by giving the proofs of security properties has advantages in flexibility of protocol specification and completeness of verification. In particular, Paulson's Inductive Method is used to verify several practical protocols and the proof modules are freely available. However, protocol specifications in this method tend to be complicated. This paper proposes a language in which one can express protocols concisely and also proposes a method to convert the protocol specification to logical formulae for Inductive Method. They make it possible to reuse the proof modules of Inductive Method in verification of large security protocols. This paper also applies them to the SET payment protocol and verifies the secrecy of payment card numbers in the protocol. To achieve this, this paper simplifies the protocol by omitting parameters that are not referred in security requirements we aim to verify.