スライド 1

Size: px

Start display at page:

Download "スライド 1"

おきみちやすこ
5 years ago
Views:

1 ProVerif によるワンタイムパスワード認証方式に対する形式的な安全性検証 2014 年 3 月 19 日荒井研一 *, 岩本智裕, 金子敏信 * * 東京理科大学東京理科大学大学院理工学研究科 1

2 はじめに本研究ワンタイムパスワード認証方式について Proverif を用いて形式的に記述し, 安全性検証を行うワンタイムパスワード認証方式に対する ProVerif の有用性を示す本発表の検証対象 :ROSI,SAS-X(2) 2

3 ワンタイムパスワード認証方式ワンタイムパスワード (OTP) 認証方式セッション毎にパスワードを変更することにより, 通信路が盗聴されたとしても安全性を保つことのできる認証方式 OTP 認証方式の満たすべき安全性サーバに保存されている情報が流出したとしてもなりすましができない通信データが改ざんされたとしてもサーバが改ざんデータを受理しないことが求められる 3

4 ProVerif 形式モデル (Dolev-Yao モデル ) での暗号プロトコルの自動検証ツール Blanchet らが開発 ( 自身のサイトで公開 ) ホーン節によるプロトコル表現秘匿, 認証などの安全性特性を検証可能さまざまな暗号プロトコルの安全性が検証されている 4

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

6 ProVerif による検証 Blanchet らのプロセス計算暗号プリミティブ ( 関数 ) 定義域, 値域, 性質 etc 安全性特性秘匿, 認証 etc 検証対象のプロトコルホーン節 ProVerif (Resolution アルゴリズム ) 攻撃なし (true) 攻撃あり (false) 6

7 Blanchet らのプロセス計算の構文規則について拡張 π 計算暗号プロトコルの記述 7

8 Constructor 及び Destructor の例 ( 例 ) 共通鍵暗号方式 : Constructor: 暗号化 encrypt(m,k) Destructor: 復号 decrypt(c,k) decrypt(encrypt(m,k),k) m fun reduc or equation ProVerif のコード fun encrypt(bitstring,key): bitstring. reduc forall x: bitstring, y: key; decrypt(encrypt(x,y),y) = x. 公開鍵暗号, 署名, MAC, ハッシュ, Diffie-Hellman 鍵交換,etc 8

9 プロトコル表現 ( ホーン節 ) メッセージ = terms M = x f M 1,, M n k M 1,, M n encrypt(m, sk) 特性 ( 性質 ) = facts F = attacker(m) プロトコル, 攻撃者 = Horn clauses F 1 F n F attacker(m) attacker(sk) attacker(encrypt(m,sk)) 9

10 ProVerif におけるホーン節について ProVerifにおけるホーン節の例 ( 例 ) 共通鍵暗号 : 暗号化 encrypt(m, k) attacker(m) attacker(k) attacker(encrypt(m, k)) 復号 decrypt encrypt(m, k), k m attacker(encrypt(m, k)) attacker(k) attacker(m) 10 10

11 ProVerif におけるホーン節について (2) ProVerif におけるホーン節の例 ( 例 ) プロトコル表現参加者 B は pencrypt(sign(y, SK A ), PK B ) を受信したときに, encrypt(s, y) を返信する attacker(pencrypt(sign(y, SK A ), PK B )) attacker(encrypt(s, y)) 攻撃者は B に対して pencrypt(sign(y, SK A ), PK B ) を送信し, B の返信である encrypt(s, y) をインターセプトする攻撃者視点 11

12 ProVerif による検証ホーン節への自動変換 Free selection( 単一化 ) ProVerif Phase1:Saturation 後向き深さ優先探索 Phase2:Derivation Search 攻撃なし (true) 攻撃あり (false) 12

13 ProVerif での認証について対応表明通信のプロセス中で情報が生成された時を事前 event, 確認した時を事後 event 事後 event が出現した際にそれに対応する事前 event が必ず存在しているか否かを検証存在していない場合なりすましが可能存在している場合認証 true 13

14 OTP 認証方式に求められる安全性ある時点でサーバに保存されている情報が流出したとしても攻撃者はユーザになりすませない Stolen-Verifier(SV)attack に対する耐性 SV attack: 攻撃者がある時点でサーバが保存している情報過去のセッションの通信データを入手しユーザになりすます攻撃 14

15 OTP 認証方式に求められる安全性 (2) 通信データが改ざんされたとしてもサーバが改ざんデータを受理しない Denial-of-Service (DoS) attack に対する耐性 DoS attack: 攻撃者が過去のセッションの通信データを入手しある時点の通信データを改ざんして誤った情報をサーバに受理させ次のセッションにおいてユーザからの接続要求を拒否させる攻撃ユーザ i 回目 i+1 回目攻撃者改ざん受理拒否サーバ 15

16 ProVerif による OTP 認証方式の形式化 ProVerif は,i 回目認証時にサーバ ( ユーザ ) が保持した値を i+1 回目認証時に利用するという概念が扱えない let processs(uid:id,x:sskey,h2sn1:bitstring)= in(c,(uid2':id,c12':bitstring,c22':bitstring)); let h1xuid2=hash((x,uid)) in let c12''=hash(xor(h1xuid2,h2sn1)) in let h2sn2''=xor(c12',c12'') in let h3sn2'=hash(h2sn2'') in let h1sn1'=xor(c22',h3sn2') in if hash(h1sn1')=h2sn1 then if h2sn2'' <> h2sn2 then out(c,xor(h2sn1,h3sn2')); ( 例 )ROSI プロトコルのサーバ処理サーバの処理を逐次的に記述 i 回目認証時に保持した h2sn2'' = i+1 回目認証時の h2sn1 h2sn2'' の値を i+1 回目に渡せない 16

17 ProVerif による OTP 認証方式の形式化 (2) 対応方法 : サーバ ( ユーザ ) の処理を複数回分まとめて記述 ( 複数回分を 1 単位とする ) let processs(uid:id,x:sskey,h2sn1:bitstring)= in(c,(uid2':id,c12':bitstring,c22':bitstring)); let h1xuid2=hash((x,uid)) in let c12''=hash(xor(h1xuid2,h2sn1)) in let h2sn2''=xor(c12',c12'') in let h3sn2'=hash(h2sn2'') in let h1sn1'=xor(c22',h3sn2') in if hash(h1sn1')=h2sn1 then if h2sn2'' <> h2sn2 then out(c,xor(h2sn1,h3sn2')); in(c,(uid3':id,c13':bitstring,c23':bitstring)); let h1xuid3=hash((x,uid)) in let c13''=hash(xor(h1xuid3,h2sn2'')) in let h2sn3''=xor(c13',c13'') in let h3sn3'=hash(h2sn3'') in let h1sn2'=xor(c23',h3sn3') in if hash(h1sn2')=h2sn2'' then out(c,xor(h2sn2'', h2sn3'')). ( 例 )ROSI プロトコルのサーバ処理 (2 回分をまとめて記述 ver.) 17

18 ProVerif による OTP 認証方式の形式化 (3) SV attack の検証 i 回目認証時に SV attack を試みる場合, その直前 (i-1 回目認証終了時 ) にサーバに保存されている情報を故意に通信路に流出この条件下で, 攻撃者がサーバに対して正規ユーザになりすますことができるかを検証 i 回目認証及び i+1 回目認証を続けてパスできるかを検証 DoS attack の検証 ProVerif における ( 通常の ) 認証の検証法を利用 i 回目認証時に Dos attack を試みる場合, 攻撃者が i 回目認証時の通信データを改ざんして誤った情報をサーバに受理させることができるかを検証 i 回目認証をパスできる Dos attack 成功 (i 回目認証はパスできるが i+1 回目認証はパスできない ) 18

19 ROSI プロトコル Chienらによって提案されたOTP 認証プロトコル [1] 辻らによりSV attackに対するぜい弱性の発見 [2] DoS attackに対して耐性を持つ登録フェーズ, 認証フェーズが存在相互認証 [1] H.Y.Chien and J.K.Jan, Robust and Simple Authentication Protocol, Computer Journal, vol.46, no.2, pp , [2] T. Tsuji, and A. Shimizu, One-Time Password Authentication Protocol aganist Theft Attacks, IEICE Trans. Commun., vol.e87-b, no.3, pp ,

20 ROSI プロトコル : 準備 ID : ユーザID P : ユーザパスワード x : サーバ秘密鍵 h : ハッシュ関数 i : セッション番号 N i : i 回目セッションの乱数 : 結合 : 排他的論理和 VR j i: h j ( P N i ), 例. VR 2 3 = h 2 ( P N 3 ) = h( h( P N 3 ) ) 20

21 ROSI プロトコル : 登録フェーズユーザサーバ Inputs ID,P,N 1 ID,P,N 1 VR 2 1 = h( h( P N 1 ) ) を計算 (ID, x, VR 2 1 を保持 ) h( x ID ) P, VR 1 1=h(P N1) を計算 h( x ID ) P, VR 1 1 Stores h( x ID ) P, VR 1 1 Stores ID, x, VR 2 1 * 登録フェーズはセキュアな通信路を用いて最初に一回だけ行われる 21

22 ROSI プロトコル :i 回目認証フェーズユーザサーバ Stored :h( x ID ) P, VR 1 i Inputs ID,P N i+1 を生成 VR 2 i,vr 2 i+1,vr 3 i+1 を計算 ID α i =h( h( x ID) VR 2 i ) VR 2 i+1 β i = VR 3 i+1 VR 1 i Stored : ID, x, VR 2 i VR 2 i VR 3 i+1 : 認証処理 VR 2 i VR 3 i+1 h( x ID ) を計算 VR 2 i+1 α i h( h( x ID ) VR 2 i ) VR 1 i β i h(vr 2 i+1 ) (α i,β i から VR 2 i+1,vr 1 i を取り出す ) VR 2? i = h(vr 1 i ) : 認証処理 Stored: VR 1 i VR 1 i+1 Stored: VR 2 i VR 2 i+1 22

23 ROSI プロトコルに対する辻らの攻撃法ユーザ攻撃者サーバサーバから ID, x, VR 2 i を盗む Stored :ID, x, VR 2 i ID α i =h( h( x ID ) VR 2 i ) VR 2 i+1 β i = VR 3 i+1 VR 1 i ID, α i, β i をインターセプト h( h( x ID) VR 2 i ) を計算 VR 2 i+1 α i h( h( x ID) VR 2 i ) VR 1 i β i h(vr 2 i+1 ) α i,β i から VR 2 i+1,vr 1 i を取り出す 23

24 ROSI プロトコルに対する辻らの攻撃法 (2) ユーザ攻撃者サーバ y (Atacker s key) を生成 N i+1 を生成 (VR 2 i+1 ) = h( h( y N i+1 ) ) (VR 3 i+1 ) = h( (VR 2 i+1 ) ) Stored : ID, x, VR 2 i ID α i =h( h( x ID) VR 2 i ) (VR 2 i+1 ) β i = (VR 3 i+1 ) VR 1 i VR 2 i = h(vr 1 i ) : 認証処理 VR 2 i VR 3 i+1 : 認証処理 VR 2 i VR 3 i+1 VR 3 i+1 (VR 3 i+1 ) VR 2 i (VR 3 i+1 ) Stored: VR 1 i VR 1 i+1 Stored: VR 2 i (VR 2 i+1 ) なりすましが可能で以降サーバは攻撃者を正規ユーザとして認証し続ける 24

25 ProVerif によって導出された攻撃法について ProVerif による検証既存の攻撃法とは異なる攻撃法辻らによる攻撃法サーバの処理に条件文を加える 25

26 ProVerif によって導出された攻撃法攻撃者サーバサーバから ID, x, VR 2 i を盗む Stored : ID, x, VR 2 i ID α i =h( h( x ID) VR 2 i ) VR 2 i β i = VR 3 i VR 1 i h( x ID) を計算同一の ID, α i, β i を送り続けることでなりすましが可能 VR 2 i α i h( h( x ID ) VR 2 i ) VR 1 i β i h(vr 2 i ) (α i,β i から VR 2 i, VR 1 i を取り出す ) VR 2? i = h(vr 1 i ) : 認証処理 VR 2 i VR 3 i+1 VR 3 i+1 VR 3 i VR 2 i VR 3 i Stored: VR 2 i VR 2 i 26

27 ProVerif による ROSI の形式的な検証既存攻撃法とは異なる SV attack を検出同一の認証用情報を送り続けることでなりすましが可能既存攻撃法も検出可能 DoS Attack は不可能 ProVerif による検証結果と既知の研究結果が一致 27

28 SAS-X(2) プロトコル辻らによって提案されたOTP 認証プロトコル [3] 鵜尾らによりDoS attackに対するぜい弱性の発見 [4] SV attackに対しては耐性を持つ登録フェーズ, 認証フェーズが存在一方向認証 [3] T. Tsuji, T. Nakahara, and A. Shimizu, A one time password authentication method, IEICE Technical Report, OIS , vol.105, no.529, pp.23 28, [4] 鵜尾健司, 白石善明, 森井昌克, Stolen Verifier attack に耐性のあるワンタイムパスワード方式の評価と提案, IPSJ Symposium Series,vol.2006,no.11, pp ,

29 SAS-X(2) プロトコル : 準備 ID : ユーザID P : ユーザパスワード h : ハッシュ関数 i : セッション番号 N i : i 回目セッションの乱数 : 結合 + : 算術加算 : 排他的論理和 E F (M): 共通鍵暗号方式の暗号化関数, F i を鍵としてMを暗号化 i D F (C): 共通鍵暗号方式の復号関数, F i を鍵としてCを復号 i 29

30 SAS-X(2) プロトコル : 登録フェーズユーザサーバ Inputs ID,P N 1, N 2, K を生成 A 1 = h( ID P N 1 ) F 1 = h( ID A 1 ) A 2 = h( ID P N 2 ) F 2 = h( ID A 2 ) γ 1 = E F ( A 1 ) を計算 2 ID, K, F 1, γ 1 Stores A 1, F 1, A 2, F 2, K, N 2 Stores ID, K, F 1, γ 1 * 登録フェーズはセキュアな通信路を用いて最初に一回だけ行われる 30

31 SAS-X(2) プロトコル :i 回目認証フェーズユーザサーバ Stored: A i, F i, A i+1, F i+1, K, N i+1 Input : ID, P N i+2 を生成 A i+2 = h( ID P N i+2 ) F i+2 = h( ID A i+2 ) α i = F i+1 F i β i = ( F i+1 + K ) A i γ i+1 = E F ( A i+1 ) を計算 i+2 ID, α i, β i, γ i+1 Stored: ID, K, F i, γ i F i+1 α i F i A i β i ( F i+1 + K ) を計算? F i = h( ID A i )? A i = D F ( γ i ) により認証処理 i+1 Store: A i A i+1, F i F i+1, N i+1 N i+2, A i+1 A i+2, F i+1 F i+2 Store: F i F i+1, γ i γ i+1 31

32 SAS-X(2) プロトコルに対する鵜尾らの攻撃法ユーザ攻撃者サーバ Stored: A i, F i, A i+1, F i+1, K, N i+1 Input : ID, P N i+2 を生成 A i+2 = h( ID P N i+2 ) F i+2 = h( ID A i+2 ) α i = F i+1 F i β i = ( F i+1 + K ) A i γ i+1 = E F i+2 ( A i+1 ) を計算送信された γ i+1 を乱数 γ i+1 に改ざん ID, α i, β i, γ i+1 Stored: ID, K, F i, γ i F i+1 α i F i A i β i ( F i+1 + K ) を計算? F i = h( ID A i )? A i = D F ( γ i ) により認証処理 i+1 Store: A i A i+1, F i F i+1, N i+1 N i+2, A i+1 A i+2, F i+1 F i+2 Store: F i F i+1, γ i γ i+1 32

33 ProVerif による SAS-X(2) の形式的な検証 ProVerif による検証鵜尾らによる攻撃法と同一の DoS attack が検出 SV Attack は不可能 ProVerif による検証結果と既知の研究結果が一致 33

34 まとめと今後の課題 ProVerif による SAS-X(2) と ROSI の安全性検証検証結果と既知の耐性評価が一致プロトコル SV attack 耐性 DoS attack 耐性 SAS-X(2) ROSI 表 1 各プロトコルの既知の攻撃耐性評価プロトコル SV attack 耐性 DoS attack 耐性 SAS-X(2) ROSI 表 2 ProVerif により導出された攻撃耐性評価 ProVerif は DoS attack SV attack を検出可能 OTP 認証方式に対して有用今後の課題 : さまざまな OTP 認証プロトコルの検証 34

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

ProVerifによる暗号プロトコルの形式的検証東京理科大学大学院電気工学専攻井上博之, 荒井研一, 金子敏信序論 ProVerif の概要検証方法セキュアシンプルペアリングの概要 Passkey Entry モード形式的な検証検証結果新たな Numeric Comparison モード形式的な検証検証結果結論 Bluetooth の SSP において中間者攻撃に対する安全性が謳われている [1] 様々な研究本研究 ProVerif