Cryptographic Protocol Verification Portal
About us
暗号プロトコル評価ポータルサイト CPVP（Cryptographic Protocol Verification Portal）では、暗号プロトコルの安全性評価の結果を、リストおよび技術文書として公開しています。公開情報は、国立研究開発法人 情報通信研究機構（以下「NICT」）による安全性評価の結果と、他の研究機関等による安全性評価をNICTで追試した結果とを幅広く含み、 ISO/IEC 29128（Verification of Cryptographic Protocol）で定められている安全性評価の基準に従ってまとめられています。なお、利用したツールはオープンソースであり、誰でも追試が可能です。
本ポータルサイトが想定する読者は、暗号プロトコルのネットワーク機器等への実装を目指す技術者、および暗号プロトコルの設計を目指す研究者です。本リストによって、実装対象の暗号プロトコルにすでに脆弱性が発見されているかどうかを確認してもらい、技術文書によって、より安全な暗号プロトコルの設計や自己評価に役立ててもらうことを目的としています。
なお、NICTは、ネットワークにおける情報通信の安全性を確立するため、暗号プロトコルを技術開発すると共に、中立的な立場で安全性を評価し、その評価結果を安全な情報通信システムの設計に役立てるための活動を実施しています。 まず、2011年に暗号プロトコルの安全性評価の基準を定める国際規格 ISO/IEC 29128 の標準化を達成し、2013年3月に改訂された電子政府推奨暗号リストの選定の際に安全性評価結果を提供、2013年7月に本ポータルサイトを開設しました。 さらに、2013年12月に設立された暗号プロトコルの安全性評価に関する唯一の国際組織「暗号プロトコル評価技術コンソーシアム（CELLOS）」設立の中心的な役割を果たすと共に事務局としても運営に貢献しています。 今後は、NICTで開発した安全性評価技術を国際標準候補の暗号プロトコルに適用し、情報通信システムの将来にわたる安全性確保に貢献します。
Further information
以下では、暗号プロトコルの安全性評価に関する解説を示します。
暗号プロトコルとは
暗号プロトコルは、暗号を用いた通信手順（プロトコル）であり、情報社会の安全性を支える基幹技術として、世界中の研究者・技術者により設計され、IETF、IEEE、ISO/IEC、ITU-Tなどの標準化団体で規格が策定（標準化）されています。代表的な例として、インターネットにおける通信相手の認証や、通信内容の秘匿と改ざん検知を目的としたSSL/TLS（Secure Sockets Layer/Transport Layer Security）が挙げられ、これは様々なネットワーク機器やPC、携帯電話、スマートフォンに実装され、広く普及しています。さらに、電子決済や時刻認証、電子投票など、社会活動の電子的な実現を目指した暗号プロトコルも活溌に研究されており、暗号プロトコルの用途は安全な通信インフラから多様なサービスまで実現しています。
暗号プロトコルの安全性評価の重要性
広く普及した暗号プロトコルに、設計の問題が発見されることが少なくありません。例えば2014年10月、約15年使われていたSSL3.0（Secure Sockets Layer version 3.0）にPOODLE と呼ばれる致命的な脆弱性が発見され、2015年6月にRFC 7568 によって使用が禁止されました。発見時、SSL3.0しかサポートしていないインターネット機器やフィーチャフォンが数多くあったため、本脆弱性の影響は大きいものでした。今後そのようなことが起きないためにも、現在普及している、あるいは将来開発される暗号プロトコルの安全性を多角的な観点から評価することが不可欠となっており、評価手法として人手による証明や形式手法に基づく検証が重要な役割を果たしています。
安全性評価の基準 ISO/IEC29128
ISO/IEC29128では、暗号プロトコルの安全性評価を、人手による証明あるいは形式手法に基づく検証で厳密化することを目指して、評価基準を定めています。具体的には安全性評価を、「プロトコル仕様、攻撃者モデル、セキュリティ要件」の記述と、「プロトコル仕様が攻撃者モデルに対してセキュリティ要件を満たしていること」の評価に分け、記述と評価の厳密性によってレベルを4つに分けています（PAL1〜4）。PAL1は厳密性が一番低く、記述と評価のいずれも形式化されていない場合を指します。PAL2〜4は記述が形式化されている点では共通ですが、PAL2は人手による証明、PAL3,4は形式手法に基づく検証ツールの適用を想定しており、評価の厳密性については必ずしも比較できません（後述の「人手による証明と形式手法による検証の特徴」を参照）。PAL3では暗号プロトコルの実行セッション数を制限していますが、PAL4では実行セッション数の制限無しで脆弱性を探索するため、同じ形式化の下であれば、PAL3よりPAL4の方が厳密な評価といえます。よって、PAL2とPAL4の両方のレベルで評価することが望ましいと考えられます。
| PAL1 | PAL2 | PAL3 | PAL4 | |
|---|---|---|---|---|
| プロトコル仕様 | PPS_SEMIFORMAL 準形式的 |
PPS_FORMAL 形式的 |
PPS_MECHANIZED 形式的（検証ツールの数学的な文法に従う） | |
| 攻撃者モデル | PAM_SEMIFORMAL 準形式的 |
PAM_FORMAL 形式的 |
PAM_MECHANIZED 形式的（検証ツールの数学的な文法に従う） | |
| セキュリティ要件 | PSP_SEMIFORMAL 準形式的 |
PSP_FORMAL 形式的 |
PSP_MECHANIZED 形式的（検証ツールの数学的な文法に従う） | |
| 評価 | PEV_ARGUMENT 非形式的な議論 |
PEV_HANDPROVEN 人手による証明 |
PEV_BOUNDED 検証ツールによる解析 実行セッション数有限 |
PEV_BOUNDED 検証ツールによる解析 実行セッション数無限 |
人手による証明と形式手法による検証の特徴
人手による証明では、プロトコル仕様と攻撃者モデル、およびセキュリティ要件を暗号理論に基づき定式化し、プロトコル仕様が攻撃者モデルに対してセキュリティ要件を満たすこと、あるいは満たさず攻撃が存在することを数学的に証明します。その際、素因数分解問題や離散対数問題など、ある種の数学問題の求解困難性を仮定し、安全性を問題の求解困難性に帰着させます。証明は自然言語で記述されます。人手による証明の長所は、攻撃成功の確率や複雑度などを厳密に評価できる点です。一方、短所は手間がかかることと、単純な誤解による誤りが混入しやすい点です。実際、著名で権威ある国際会議で採録された論文で人手による証明が示された後に、証明に誤りが指摘され、攻撃が発見された暗号プロトコルがあります。
形式手法に基づく検証では、評価を計算機で自動化できるように、プロトコル仕様と攻撃者モデル、およびセキュリティ要件を抽象化して記述し、プロトコル仕様が攻撃者モデルに対してセキュリティ要件を満たす、あるいは満たさず攻撃が存在することを、検証ツールを利用して数学的に解析します。解析でプロトコルの実行セッション数を制限する場合（bounded）と制限が無く任意のセッション数を許す場合（unbounded）があります。Boundedで攻撃が発見されなくとも、unboundedで攻撃が発見される場合があり、後者での評価が望ましいと考えられています。形式手法に基づく検証の長所は、評価の自動化による手間の削減と自然言語による曖昧さによる誤り見逃しが無い点です。一方、短所は状態爆発による検証不能性や、抽象化による攻撃見逃しです。実際、人手による証明で発見できる攻撃であっても暗号理論に強く依存していた場合、形式手法では記述できず、検証ツールでは検知できません。それを解決するため、計算論的に健全な形式化として、暗号理論的に見逃しても問題ない攻撃のみ見逃す形式化が研究されています。