ProVerifによる暗号プロトコルの形式的検証

Size: px

Start display at page:

Download "ProVerifによる暗号プロトコルの形式的検証"

ときおなか
5 years ago
Views:

1 東京理科大学大学院電気工学専攻井上博之, 荒井研一, 金子敏信

2 序論 ProVerif の概要検証方法セキュアシンプルペアリングの概要 Passkey Entry モード形式的な検証検証結果新たな Numeric Comparison モード形式的な検証検証結果結論

3 Bluetooth の SSP において中間者攻撃に対する安全性が謳われている [1] 様々な研究本研究 ProVerif による Numeric Comparison モードに対する安全性評価 Passkey Entry モードに対する安全性評価 ProVerif による Passkey Entry モードに対する安全性評価 ProVerif による新たな Numeric Comparison モード [2] に対する安全性評価

4 ProVerif は Blanchet らが開発形式モデル (Dolve-Yao モデル ) での暗号プロトコルの安全性検証ツール Horn 節の原理を用い攻撃ルールを作成 ProVerif のコード宣言部暗号プロトコルに用いられる暗号プリミティブや検証対象の設定プロセス部プロトコル全体の流れを参加者ごとに逐次的に記述 ( 秘匿, 認証 ) 共通鍵暗号, 公開鍵暗号

5 完全な暗号 (perfect encryption) を仮定 ( 例 ) 共通鍵暗号方式 E( M, K) D( C, K ) 鍵 Kにおける M の暗号化鍵 Kにおける C の復号 M D( E( M, K), K) 鍵 K を知らなければ平文 M に関する情報はまったく得られない

6 秘匿 (Standard Secrecy) 攻撃者が秘匿対象の情報を入手可能か否かを検証強秘匿 (Strong Secrecy) 攻撃者が秘匿対象の情報を暗号化した暗号文とその暗号文とはなんら関係のない乱数との違いを識別可能か否かを検証

7 通信のプロセス中で情報が生成された時を事前 event, 確認した時を事後 event 事後 event が出現した際にそれに対応する事前 event が出現しているか否かを検証存在していない場合なりすましが可能 M 存在している場合 Non-Injective 経路が唯一なのか複数あるかについては関知しない認証用情報を再送 ( 再生攻撃 ) 攻撃者 N 認証してしまう Injective このとき経路は唯一なのか否かについても検証を行う M N M から N へ到着可能なパスが 1 つだけ存在

8 端末間で相互認証し関連付けを行うこと 2007 年に bluetooth2.1+edr が策定セキュアシンプルペアリング (SSP) が追加 SSP 1Numeric Comparison 2Out of Band 3Just Works 4Passkey Entry 5Tzu-Chang らにより [5] 提案された新たな NumericComparison SSP のフェーズ 1 公開鍵交換 2 認証ステージ 1 3 認証ステージ 2 4 リンクキー計算 5 認証暗号化

9 DeviceA 1(SKa,PKa) フェーズ 1 2A,IOcapA,PKa 3B,IOcapB,PKb DeviceB 1(SKb,PKb) 4DHKey=P192(SKa,PKb) 4DHKey=P192(SKb,PKa) フェーズ2 r a =r b 事前共有パスキ-r a =r b (20bit) r a =r b 5N ai の生成 6C ai の生成 C ai =f1(pka,pkb,n ai,r ai ) 12C bi の生成 ( ハッシュ値 ) C v bi =f1(pkb,pka,nbi,rai) C bi =C bi の時 1ECDHの秘密鍵公開鍵のペアを生成 5N bi の生成 2A(MAC 値 ),IOcapA(I/O 情報 ),Pka( 公開鍵 ) を送信 3B(MAC 値 ),IOcapB(I/O 7C 情報 ),Pkb( 公開鍵 ) を送信 ai 4DH 鍵の生成 5 乱数 N 8C bi A,B:BluetoothMac ai,n bi の生成値 6ハッシュ値 IOcapA,IOcapB:I/O C ai,c bi の生成 9N ai 情報 r ai,r bi はパスキーの1bitを表わしている 11N bi 20 回繰り返す 6Cbiの生成 C bi =f1(pkb,pka,n bi,r bi ) 10C ai の生成 ( ハッシュ値 ) C ( 1 ai =f1(pka,pkb,nai,rbi) i v 20 ) C ai =C ai の時

10 13Ea の生成 ( ハッシュ値 ) Ea=f3(DHKey,Na,Nb,ra,IOcapA, A,B) フェーズ 3 14 Ea 13Ebの生成 ( ハッシュ値 ) Eb=f3(DHKey,Nb,Na,rb,IOcapB, B,A) Ea の生成 ( ハッシュ値 ) 17Eb の生成 ( ハッシュ値 ) Eb =f3(dhkey,nb,na,rb,iocapb, B,A) E b =E b の時 16Eb 13 ハッシュ値 Ea,Eb の生成 14Ea の送信フェーズ 4 18 両デバイスでリンクキー c (LK) を計算 15Ea の生成 ( ハッシュ値 ) Ea =f3(dhkey,na,nb,ra,iocapa, A,B) E a =E a の時共有したKcが秘匿性を満たしているか 15ハッシュ値 Ea の生成 LK=f2(DHKey,Na,Nb, btlk,a,b) Ea=Ea の時次に進む,Ea Ea の時アボートする 16Ebの送信フェーズ5 17ハッシュ値 Eb の生成 Eb=Eb 19Kc=E3(LK,EN_RAND,COF) の時次に進む,Eb Eb の時アボートする

11 秘匿 free secreta,secretb:bitstring[private]. query attacker(secreta); attacker(secretb); secreta,secretb の秘匿性認証 event endaparam(g1). event beginaparam(g1). event endbparam(g1). event beginbparam(g1). event endakey(g1,g1,g1). event beginakey(g1,g1,g1). event endbkey(g1,g1,g1). event beginbkey(g1,g1,g1). 型宣言 Weak authenticcation 参加者が誰であるかの認証 query x:g1 ; inj-event(endaparam(x)) ==> inj-event(beginaparam(x)). query x:g1 ; inj-event(endbparam(x)) ==> inj-event(beginbparam(x)). query x1:g1,x2:g1,x3:g1 ; inj-event(endakey(x1,x2,x3)) ==> inj-event(beginakey(x1,x2,x3,x4)). query x1:g1,x2:g1,x3:g1 ; inj-event(endbkey(x1,x2,x3)) strong authenticcation ==> inj-event(beginbkey(x1,x2,x3)). 鍵を誰が作成したかと参加者が誰であるかの認証

12 離散対数問題 (DLP) 既知の (g,g a ) に対して a を求めること計算 DH 問題 (CDH) 有限体上で与えられた入力組 (g,g a,g b ) に対して g ab を求めること 1. fun exp(g2,scalar):g2. 2. equation forall a:scalar, b:scalar; exp(exp(g,a),b)=exp(exp(g,b),a) 楕円曲線上の離散対数問題 (ECDLP) 既知の (P,aP) に対して a を求めること楕円曲線上の計算 DH 問題 (ECDHP) 既知の (P,aP,bP) に対して abp を求めること 1. fun P192(scalar,G1):G1. 2. equation forall a:scalar, b: scalar; g ab =g ba abp=bap P192(a,P192(b,P)) =P192(b,P192(a,P)).

13 秘匿の検証結果 AB 間で共有した Kc についての秘匿性を調査 Property Result SecretA False SecretB False 認証の検証結果 1Weak Authentication 2Strong Authentication Kcは秘匿性を満たしていない中間者攻撃 Property Result A-to-B Non-Injective Weak Authentication False B-to-A non-injective Weak Authentication False A-to-B Non-Injective Strong Authentication False B-to-A Non-Injective Strong Authentication False 認証を満たしていないなりすましが可能

14 DeviceA フェーズ1,2,3 DeviceB 2(SKa,PKa) 1 事前にPINを共有 2(SKb,PKb) 3A,IOcapA,PKa PIN 4DHKey=P192(Skb,PKa) 5B,IOcapB,PKb PIN,Cb Cb の生成 ( ハッシュ値 ) Cb=f1(DHKey,IOcapB, IOcapA,B,A) 6DHKey=P192(Ska,Pkb) 排他的論理和 Cb の生成 ( ハッシュ値 ) Cb =f1(dhkey,iocapb, IOcapA,B,A) Cb=Cb の時 7Caの生成 ( ハッシュ値 ) Ca=f1(DHKey,IOcapA, IOcapB,A,B) 1 事前にPINを共有 2ECDHの秘密鍵公開鍵のペアを生成 ( 公開鍵は公開しない ) 3A(MAC 値 ),IOcapA(I/O 情報 ),PKa 4DH 鍵の生成, ハッシュ値 Cbの生成 5B(MAC 値 ),IOcapB(I/O 情報 ),Pkb 8Ca PIN を送信 PINを送信

15 フェーズ 4 両デバイスでリンクキー c (LK) を計算 10LK=f2(DHKey, btlk,a,b) フェーズ 5 11Kc=E3(LK,EN_RAND,COF) 9Ca の生成 ( ハッシュ値 ) Ca =f1(dhkey,iocapa, IOcapB,A,B) Ca=Ca の時共有したKcが秘匿性を満たしているか

16 ProVerif での形式化 (( x y) y) y ( x x) 1. fun xor(g1,g1):g1. 2. equation forall x:g1, y: G1; xor(xor(x,y),y)=x. 3. equation forall x:g1, y: G1; xor(y,xor(x,x))=y. 4. equation forall x:g1; xor(x,xor(x,x))=x. 5. equation forall x:g1; xor(xor(x,x),x)=x. x x ( x x) y x ( x x) x x

秘匿の検証結果認証の検証結果 AB 間で共有した Kc についての秘匿性を調査 1 参加者が誰であるかの認証 2 鍵を誰が作成したかと参加者が誰であるか Property Property SecretA SecretB Result True A-to-B Injective Weak Authentication True B-to-A Injective Weak

17 秘匿の検証結果認証の検証結果 AB 間で共有した Kc についての秘匿性を調査 1 参加者が誰であるかの認証 2 鍵を誰が作成したかと参加者が誰であるか Property Property SecretA SecretB Result True A-to-B Injective Weak Authentication True B-to-A Injective Weak Authentication A-to-B Non-Injective Weak Authentication B-to-A non-injective Weak Authentication A-to-B Injective Strong Authentication B-to-A Injective Strong Authentication Result False False True False False False A-to-B Non-Injective Strong Authentication True B-to-A non-injective Strong Authentication 共有した再生攻撃が可能 Kcは秘匿なりすましが可能秘匿性を満たす False

18 2(SKa,PKa) A M B A,IOcapA,PKa 1 事前に B,IOcapB,m PIN A,IOcapA,PKa PINを共有 M PIN A,IOcapA,PKa PIN 2(SKb,PKb) A,IOcapA,PKa PIN 3A,IOcapA,PKa PIN なりすまし再生攻撃前のセッションで送られた情報とかわっていない 4DHKey=P192(Skb,PIN 4DHKey=P192(Skb,PKa) m M ) なりすましが可能再生攻撃が可能 Cb Cb=f1(DHKey,IOcapB, IOcapA,B,A) IOcapB,B,B) 5B,IOcapB,PKb PIN,Cb DHKey=P192(Ska,Pkb) Cb の生成 ( ハッシュ値 ) b =f1(dhkey,iocapb,iocapa,b,a) Cb=Cb の時 Cb 8Ca 9Ca の生成 ( ハッシュ値 ) Ca =f1(dhkey,iocapa, Ca =f1(dhkey,iocapb, IOcapB,A,B) IOcapB,B,B) Ca=Ca の時

19 ProVerif による SSP に対する形式的な安全性検証 PasskeyEntry モードに対して中間者攻撃新たな Numericarison モードに対して再生攻撃

[1]SIMPLE PAIRING WHITEPAPER [2] Tzu-Chang Yeh,Jian-Ren Peng, Sheng-Shih Wang,and Jun-Ping Hsu Securing Bluetooth Communications international Journal of Network Security,July 2012 [3] 野村大翼松尾和人

20 [1]SIMPLE PAIRING WHITEPAPER [2] Tzu-Chang Yeh,Jian-Ren Peng, Sheng-Shih Wang,and Jun-Ping Hsu Securing Bluetooth Communications international Journal of Network Security,July 2012 [3] 野村大翼松尾和人 Bluetooth のセキュアシンプルペアリングに対する中間者攻撃情報処理学会論文誌 (Sep.2012) [4] Bruno Blanchet,and Ben Smyth ProVerif 1.86pl4: Automatic Cryptographic Protocol Verifier,User Manual and Tutorial [5]Richard Chang andvitaly Shmatikov Formal Analysis of Authentication in Bluetooth Device Pairing

スライド 1

スライド 1 ProVerif によるワンタイムパスワード認証方式に対する形式的な安全性検証 2014 年 3 月 19 日荒井研一 *, 岩本智裕, 金子敏信 * * 東京理科大学東京理科大学大学院理工学研究科 1 はじめに本研究ワンタイムパスワード認証方式について Proverif を用いて形式的に記述し, 安全性検証を行うワンタイムパスワード認証方式に対する ProVerif の有用性を示す