<4D F736F F F696E74202D204E FEE95F192CA904D835A834C A C F8FBC94F65F88F38DFC94C5>

Size: px

Start display at page:

Download "<4D F736F F F696E74202D204E FEE95F192CA904D835A834C A C F8FBC94F65F88F38DFC94C5>"

はなつつの
5 years ago
Views:

1 暗号プロトコルの安全性評価と国際標準化への寄与独立行政法人情報通信研究機構セキュリティアーキテクチャ研究室松尾真一郎 1

2 本発表の概要暗号プロトコル分野における国際標準化動向暗号プロトコルの安全性評価技術 ISO/IEC 29128(Verification of Cryptographic Protocols) 暗号プロトコルの評価事例 NICTにおける暗号プロトコル評価における取り組み 2

3 暗号技術に関連する国際標準化の概要 ISO/IEC ITU-T 暗号アルゴリズムおよびプロトコルを SC27/WG2 で標準化日本から多くの Contribution 標準規格日本から議長を 2 代連続して出している安全性に関する評価を主体的には実施していないが暗号に関するエキスパートが集まっており安全でない暗号が選ばれることはない IETF 暗号アルゴリズムの標準化は行っていない X.509 など一部暗号応用について標準化暗号アルゴリズムについては ISO/IEC を参照 IEEE 多くの暗号プロトコルを RFC としているその中で暗号スイートとして暗号アルゴリズムを掲載いくつかの日本の暗号も暗号スイートとして掲載ただし安全性に関するチェックは甘く RFC になった後に攻撃が見つかることが少なくない ID ベース暗号無線 LAN の暗号技術など個別の暗号技術を標準化特にハードウエア製品における影響力は大きい

4 ISO/IEC における国際標準化 ISO/IEC JTC1 SC27 においてセキュリティに関する標準化を実施 WG1 WG2 WG3 WG4 WGのタイトル情報セキュリティマネジメントシステム暗号とセキュリティメカニズムセキュリティ評価基準セキュリティコントロールとサービス標準の例 ISO/IEC (ISMS) ISO/IEC 18033(Encryption Algorithm) ISO/IEC (Common Criteria) WG5 アイデンティティ管理とプライバシ技術 4

5 ITU T における国際標準化標準化の項目図表 ITU-T SG17 WP の構成 WP 課題名 WP1: Network and information security WP2: Application security WP3: Identity management and languages Q.1 Telecommunications systems security project Q.2 Security architecture and framework Q.3 Telecommunications information security management Q.4 Cybersecurity Q.5 Countering spam by technical means Q.6 Security aspects of ubiquitous telecommunication services Q.7 Secure application services Q.8 Cloud computing security Q.9 Telebiometrics Q.10 Identity management architecture and mechanisms Q.11 Directory services, Directory systems, and public key/attribute certificates Q.12 Abstract Syntax Notation One (ASN.1), Object Identifiers (OIDs) and associated registration Q.13 Formal languages and telecommunication software Q.14 Testing languages, methodologies and framework Q.15 Open Systems Interconnection (OSI) 5

6 IETFにおける国際標準化標準化の項目 Application Bridging forfederated Access Beyond web (abfab) Common Authentication Technology Next Generation (kitten) DNS-based Authentication of Named Entities (dane) EAP Method Update (emu) Handover Keying (hokey)( に concluded WG となっている ) IP Security Maintenance and Extensions (ipsecme) Kerberos (krb-wg) Network Endpoint Assessment (nea) Public-Key Infrastructure (X.509) (pkix) Transport Layer Security (tls) Web Authorization Protocol (oauth) Javascript Object Signing and Encryption (jose) Managed Incident Lightweight Exchange (mile) 6

7 IETF における国際標準化 Authorization and Access Control (aac) Authenticated Firewall Traversal (aft) Better-Than-Nothing Security (btns) Profiling Use of PKI in IPSEC (pki4ipsec) Securely Available Credentials (sacred) Simple Authentication and Security Layer (sasl) Secure Shell (secsh) S/MIME Mail Security (smime) SNMP Authentication (snmpauth) SNMP Security (snmpsec) Simple Public Key Infrastructure (spki) Security Policy (spwg) Site Security Policy Handbook (ssphwg) stime Security Issues in Network Event Logging (syslog) Web Transaction Security (wts) xmldsig 7

8 IETF における国際標準化 Common Authentication Technology (cat) Commercial Internet Protocol Security Option (cipso) Domain Keys Identified Mail (dkim) Credential and Provisioning (enroll) Handover Keying (hokey) TCP Client Identity Protocol (ident) Intrusion Detection Exchange Format (idwg) Extended Incident Handling (inch) IP Authentication (ipauth) IP Security Protocol (ipsec) IPSEC KEYing information resource record (ipseckey) IP Security Policy (ipsp) IP Security Remote Access (ipsra) Integrated Security Model for SNMP (isms) ispp ( 詳細情報活動記録なし ) Provisioning of Symmetric Keys (keyprov) Kerberized Internet Negotiation of Keys (kink) Long-Term Archive and Notary Services (ltrans) IKEv2 Mobility and Multihoming (mobike) Multicast Security (msec) An Open Specification for Pretty Good Privacy (openpgp) One Time Password Authentication (otp) Privacy-Enhanced Electronic Mail (pem) Profiling Use of PKI in IPSEC (pki4ipse) 8

9 IEEE における国際標準化標準化の項目無線 LAN セキュリティ (IEEE x) WEP, WPA, WPA2 など暗号アルゴリズム (IEEE P.1363) 公開鍵暗号認証など ( パスワード認証付き鍵交換 ) 9

10 その他のセキュリティ関連の標準化団体 Web 技術の標準 W3C OASIS ヨーロッパの標準化団体 ETSI 10

攻撃ポイント A, r B 乱数生成電子署名生成乱数生成電子署名検証 Sig<SK A >{r B }, B, r

11 暗号プロトコルとは暗号アルゴリズム ( 暗号化電子署名など ) と通信を組み合わせてより高度なセキュリティ機能 ( 認証やプライバシ保護 ) を達成する技術 SSL/TLS をはじめとして様々な場面で利用されている A B 攻撃ポイント A, r B 乱数生成電子署名生成乱数生成電子署名検証 Sig<SK A >{r B }, B, r A Sig<SK B >{r A }, r B 電子署名検証乱数生成電子署名生成電子署名を利用した相互認証プロトコルの例 11

12 暗号プロトコルの安全性評価暗号プロトコルが任意の攻撃者による行動の組み合わせに対して防ぎたい状況が発生しないかどうかをチェック起きてはいけない状況情報の漏洩なりすましの成功 ( 例 ) プロトコル仕様認証方式通信路サーバ内の暗号化方式攻撃者の能力盗聴改ざん安全性評価 ( ツール利用手による証明, ) 起きてはいけない状況が発生しないかどうか発生する場合は発生に至る手順を出力任意の通信データの送信

13 暗号プロトコル評価の現状多数の技術ツールが研究開発されている 1. 様相論理を用いるもの限定された認証性質についてしか推論できないため現在ではあまり利用されていない ( 例 : BAN ロジック ) 2. モデルチェッキング手法を用いるもの自動検証可能安全性評価に大きな効果を上げている ( 例 :NRL FDR AVISPA ProVerif SCYTHER CryptoVerif など多数 ) 3. 定理証明を用いるもの通常人手による証明戦略の指示などが必要であるため完全な自動証明は困難だがセッション数の制限などはないためより強い検証結果を得られる ( 例 : Isabelle, Coq, CertiCrypt, EasyCrypt)

14 暗号プロトコル評価の現状 ( 続き ) 抽象化レベルもさまざま Dolev Yaoモデル : 暗号プリミティブを完全なものと仮定するモデル計算量理論的なモデル : 暗号プリミティブを確率的な振る舞いをするより現実的なものと仮定するモデル検証範囲もさまざま Unbounded: セッション数に制限を設けず検証 Bounded: セッション数に制限を設けた範囲のみの探索により検証

15 主な暗号プロトコル検証ツール

16 実用上の課題各ツールが扱えるプロトコル / セキュリティ要件はそれぞれ異なりまた検証結果の保証の程度も異なる異なる手法間の関係性も必ずしも明らかではないその結果暗号プロトコルを実務的に開発あるいは利用する立場からはプロトコルをどのツールを使って評価すればよいのかまたどういう結果が得られれば安心できるのかが分からない状況にある暗号プロトコル評価に一定の基準を与えたい!

17 暗号プロトコル評価の物差し :ISO/IEC Verification of Cryptographic Protocols 日本からの提案により ISO/IEC JTC1 SC27/WG3において標準化を開始 2011 年 11 月に標準化を完了

18 ISO/IEC の概要プロトコル評価を行う上で共通的に必要となると考えられる記述事項 ( プロトコル仕様攻撃者モデルセキュリティ要件自己評価資料 ) を規定しさらに検証の度合いに応じて以下の 4 つのプロトコル保証レベルを定義プロトコル保証レベル1 プロトコル仕様は準形式的に記述され攻撃者モデルセキュリティ要件は非形式的に記述されていてよいまた検証は非形式的な議論によるものでよいプロトコル保証レベル2 プロトコル仕様攻撃者モデルセキュリティ要件は数学的に厳密な形で記述されなければならない検証には安全性証明の正しさを専門家が確認できることが求められるプロトコル保証レベル3 プロトコル仕様攻撃者モデルセキュリティ要件は機械的に処理可能な形で形式的に記述されなければならないまた検証はツールを用いた形式的な証明でなければならないただし検証に当たっては並行動作するセッション数には上限を設けてよいプロトコル保証レベル4 プロトコル保証レベル2に加えてさらにセッション数に関する制限なしに検証されなければならない

19 プロコトル保証レベル客観的な信頼性の高さプロトコル保証レベルプロトコル仕様 PAL1 PAL2 PAL3 PAL4 PPS_SEMIFORMAL PPS_FORMAL PPS_MECHANIZED プロトコル仕様を準形式的に記述プロトコル仕様を形式的に記述プロトコル仕様を形式的に記述その記述はツールに対応した言語で記述されその言語の文法は数学的に定義されている攻撃者モデル PAM_INFORMAL PAM_FORMAL PAM_MECHANIZED 攻撃者モデルを非形式的に記述攻撃者モデルを形式的に記述攻撃者モデルを形式的に記述その記述はツールに対応した言語で記述されその言語の文法は数学的に定義されているセキュリティ要件 PSP_INFORMAL セキュリティ要件を非形式的に記述 PSP_FORMAL セキュリティ要件を形式的に記述 PSP_MECHANIZED 攻撃者モデルを形式的に記述その記述はツールに対応した言語で記述されその言語の文法は数学的に定義されている自己評価エビデンス PEV_ARGUMENT 攻撃者モデルにおいて対象となるプロトコルがセキュリティ要件を満たしている事を非形式的に評価 PEV_HANDPROVEN 攻撃者モデルにおいて対象となるプロトコルがセキュリティ要件を満たしている事を数学的形式が整った人間による証明で評価 PEV_BOUNDED 攻撃者モデルにおいて対象となるプロトコルがセキュリティ要件を満たしている事をツールを利用した有限チェックで評価 PEV_UNBOUNDED 攻撃者モデルにおいて対象となるプロトコルがセキュリティ要件を満たしている事をツールを利用した無限チェックで評価 19

ISO/IEC で規定されたエンティティ認証の評価 ISO/IEC 9798-2( 共通鍵暗号を用いたプロトコル ) ISO/IEC 9798-3( 電子署名を用いたプロトコル ) ISO/IEC 9798-4(

20 ISO/IEC で規定されたエンティティ認証の評価 ISO/IEC ( 共通鍵暗号を用いたプロトコル ) ISO/IEC ( 電子署名を用いたプロトコル ) ISO/IEC ( 検査関数 (MAC) を用いたプロトコル ) 例 ) Mechanism 4 - Three-pass authentication 形式化手法を用いることで 3 種類の攻撃を発見 ISO/IEC で修正を実施

21 安全性評価結果 (1) Role Mix-up Attack エンティティの役割に関する確認ができなくなる攻撃 Matching conversation やプロトコルにおける同期の問題が発生

22 安全性評価結果 (2) Type Flow Attack エンティティの名前が n ビットのビット列にエンコードされていてプロトコル中の nonce も n ビットで表現されるときに発生エンティティの名前を誤って fresh な乱数として受け取ってしまう

23 安全性評価結果 (3) Reflection Attack プロトコルの Initiator と Responder が同一の場合に起こる攻撃オプションフィールドの利用目的が規定されていないため暗号化されたデータをそのまま再利用することで攻撃が発生

24 暗号プロトコル評価ポータル NICTで実施した暗号プロトコルに対する安全性評価結果を公開 SCYTHERとProVerifの2つのツールによる安全性評価結果技術標準になっているプロトコルなどを評価 IETF ISO/IEC IEEE その他

25 暗号プロトコル評価システム Web 画面を通じて形式的検証ツールを用いたプロトコル評価が可能 GUI による簡単な入力複数のツール (Scyther, ProVerif) による結果を蓄積表示過去の評価結果も参照可能

26 まとめ暗号プロトコル分野における国際標準化動向暗号プロトコルの安全性評価技術 ISO/IEC 29128(Verification of Cryptographic Protocols) 暗号プロトコルの評価事例 NICTにおける暗号プロトコル評価における取り組み 26

JSIAM年会2011プレゼンファイルISO_CRYPTREC

JSIAM年会2011プレゼンファイルISO_CRYPTREC (1) BAN (2) NRL FDR AVISPA ProVerif SCYTHER CryptoVerif (3) Isabelle Dolev-Yao Unbounded Bounded !"#$%&'($')*+, -($".$/&0."1*+, 23/4"%*' H=C 25:-;K >."8$.*9 K8?2>K& F-KL2>G 5.306",.70(*'