fun H(bitstring): bitstring. (* SHA1 ) fun P_hash(bitstring, bitstring): bitstring. ( P_SHA1 *) reduc forall secret: bitstring, label: bitstring, se

Size: px

Start display at page:

Download "fun H(bitstring): bitstring. (* SHA1 *) fun P_hash(bitstring, bitstring): bitstring. (* P_SHA1 *) reduc forall secret: bitstring, label: bitstring, se"

このかいなくら
5 years ago
Views:

1 暗号プロトコル評価結果独立行政法人情報通信研究機構 1. プロトコル名 :EAP-TLS 2. 関連する標準 IETF:RFC2716 ( 3. 使用したツール :Proverif 4. 評価の概要 :Proverif による評価では攻撃は発見されなかった 5.ProVerif による評価以下ではロール S(Authenticator) をロール A で表す 5.1. シーケンス記述 free c: channel. type skey. type pkey. type nonce. type host. const Request: bitstring [data]. const Response: bitstring [data]. const Success: bitstring [data]. const MASTER_SECRET: bitstring [data]. const SERVER_FINISHED: bitstring [data]. const CLIENT_FINISHED: bitstring [data]. free hostp, hosta: host. (* Hash and PRF *)

2 fun H(bitstring): bitstring. (* SHA1 *) fun P_hash(bitstring, bitstring): bitstring. (* P_SHA1 *) reduc forall secret: bitstring, label: bitstring, seed: bitstring; PRF(secret, label, seed) = P_hash(secret, (label, seed)). (* PKE *) fun pk(skey): pkey. fun encrypt(bitstring, pkey): bitstring. reduc forall x: bitstring, sk: skey; decrypt(encrypt(x, pk(sk)), sk) = x. (* Sig *) fun sign(bitstring, skey): bitstring. reduc forall x: bitstring, sk: skey; check(sign(x, sk), pk(sk)) = x. reduc forall x: bitstring, sk: skey; getmsg(sign(x, sk)) = x. (* encryption for describing secrety *) fun hide(bitstring, bitstring): bitstring. reduc forall x: bitstring, k: bitstring; reveal(hide(x, k), k) = x. (* fun n2b(nonce): bitstring [data, typeconverter]. fun n2k(nonce): key [data, typeconverter]. *) free secretpeer, secretauthenticator, secrettest: bitstring [private]. (* events *) event beginpeer(host, host, bitstring, nonce, nonce, bitstring,

3 bitstring, bitstring). event endpeer(host, host, bitstring, nonce, nonce, bitstring, bitstring, bitstring). event beginauthenticator(host, host, bitstring, nonce, nonce, bitstring, bitstring, bitstring). event endauthenticator(host, host, bitstring, nonce, nonce, bitstring, bitstring, bitstring). event end(). (**) (* not attacker(new KEKpa). not attacker(new KCKpa). *) (* queries *) query attacker(secretpeer). query attacker(secretauthenticator). query p: host, a: host, k: bitstring, rp: nonce, ra: nonce, v: bitstring, s: bitstring, c: bitstring; inj-event(endauthenticator(p, a, k, rp, ra, v, s, c)) ==> inj-event(beginpeer(p, a, k, rp, ra, v, s, c)). query p: host, a: host, k: bitstring, rp: nonce, ra: nonce, v: bitstring, s: bitstring, c: bitstring; inj-event(endpeer(p, a, k, rp, ra, v, s, c)) ==> inj-event(beginauthenticator(p, a, k, rp, ra, v, s, c)). query attacker(secrettest).

4 let procpeer(p: host, skp: skey, client_certificate: bitstring, pkca: pkey) = in(c, (A: host, client_version: bitstring, cipher_suites: bitstring, compression_methods: bitstring)); (* Request/Identity *) in(c, =Request); (* Response/Identity *) out(c, (Response, P)); (* Request/EAP_TLS/Start *) in(c, =Request); (* Response/EAP_TLS/client_hello *) new client_random: nonce; (* gmt_unix_time is omitted *) let client_hello = (client_version, client_random, cipher_suites, compression_methods)in out(c, (Response, client_hello)); (* Request/EAP_TLS/server_hello, server_certificate *) in(c, (=Request, server_hello: bitstring, server_certificate: bitstring)); let (server_version: bitstring, server_random: nonce, server_cipher_suites: bitstring, server_compression_methods: bitstring) = server_hello in if server_version = client_version && server_cipher_suites = cipher_suites && server_compression_methods = compression_methods then let (=A, pka: pkey) = check(server_certificate, pkca) in (* Response/EAP_TLS/client_certificate, client_key_exchange, certificate_verify, finished*) new pre_master_secret: bitstring; (* RSA key exchange *) let client_key_exchange = encrypt(pre_master_secret, pka) in

5 let certificate_verify = sign((client_hello, server_hello, server_certificate, client_certificate, client_key_exchange), skp) in let master_secret = PRF(pre_master_secret, MASTER_SECRET, (client_random, server_random)) in let client_finished = PRF(master_secret, CLIENT_FINISHED, H((client_hello, server_hello, server_certificate, client_certificate, client_key_exchange, certificate_verify))) in event beginpeer(p, A, master_secret, client_random, server_random, client_version, cipher_suites, compression_methods); out(c, (Response, client_certificate, client_key_exchange, certificate_verify, client_finished)); (* Request/EAP_TLS/change_cipher_spec, finished *) in(c, (=Request, server_finished: bitstring)); if server_finished = PRF(master_secret, SERVER_FINISHED, H((client_hello, server_hello, server_certificate, client_certificate, client_key_exchange, certificate_verify, client_finished))) then (* Response/EAP_TLS*) out(c, Response); (* Success *) in(c, =Success); (* For security analysis *) if A = hosta then event endpeer(p, A, master_secret, client_random, server_random,

6 client_version, cipher_suites, compression_methods); out(c, hide(secretpeer, master_secret)); event end(). let procauthenticator(a: host, ska: skey, server_certificate: bitstring, pkca: pkey) = in(c, (server_version: bitstring, server_cipher_suites: bitstring, server_compression_methods: bitstring)); (* Request/Identity *) let m1 = Request in out(c, m1); (* Response/Identity *) in(c, m2: bitstring); let (=Response, P: host) = m2 in (* Request/EAP_TLS/Start *) let m3 = Request in out(c, m3); (* Response/EAP_TLS/client_hello *) in(c, (=Response, client_hello: bitstring)); let (client_version: bitstring, client_random: nonce, cipher_suites: bitstring, compression_methods: bitstring) = client_hello in if client_version = server_version && cipher_suites = server_cipher_suites && compression_methods = server_compression_methods then (* Request/EAP_TLS/server_hello,... *) new server_random: nonce; (* gmt_unix_time is omitted *) let server_hello = (server_version, server_random, server_cipher_suites, server_compression_methods) in out(c, (Request, server_hello, server_certificate));

7 (* Response/EAP_TLS/certificate,... *) in(c, (=Response, client_certificate: bitstring, client_key_exchange: bitstring, certificate_verify: bitstring, client_finished: bitstring)); let (=P, pkp: pkey) = check(client_certificate, pkca) in if (client_hello, server_hello, server_certificate, client_certificate, client_key_exchange) = check(certificate_verify, pkp) then let pre_master_secret = decrypt(client_key_exchange, ska) in let master_secret = PRF(pre_master_secret, MASTER_SECRET, (client_random, server_random)) in if client_finished = PRF(master_secret, CLIENT_FINISHED, H((client_hello, server_hello, server_certificate, client_certificate, client_key_exchange, certificate_verify))) then event beginauthenticator(p, A, master_secret, client_random, server_random, server_version, server_cipher_suites, server_compression_methods); let server_finished = PRF(master_secret, SERVER_FINISHED, H((client_hello, server_hello, server_certificate, client_certificate, client_key_exchange, certificate_verify, client_finished))) in out(c, (Request, server_finished)); (* Response/EAP_TLS *)

8 in(c, =Response); (* Sucess *) out(c, Success); (* For security analysis *) if P = hostp then event endauthenticator(p, A, master_secret, client_random, server_random, server_version, server_cipher_suites, server_compression_methods); out(c, hide(secretauthenticator, master_secret)); event end(). let procca(skca: skey) = in(c, (h: host, k: pkey)); if h <> h then (*!!!! *) if h <> hostp && h <> hosta then out(c, sign((h, k), skca)). process new skca: skey; let pkca = pk(skca) in out(c, pkca); (**) new skp: skey; let certp = sign((hostp, pk(skp)), skca) in out(c, certp); (**) new ska: skey; let certa = sign((hosta, pk(ska)), skca) in out(c, certa); ( (!procpeer(hostp, skp, certp, pkca))

9 ) (!procauthenticator(hosta, ska, certa, pkca)) (!procca(skca)) 5.2. 攻撃者モデルシーケンスの表記に含まれる 5.3. セキュリティプロパティの記述 (* (2) *) query p: host, a: host, k: bitstring, rp: nonce, ra: nonce, v: bitstring, s: bitstring, c: bitstring; inj-event(endauthenticator(p, a, k, rp, ra, v, s, c)) ==> inj-event(beginpeer(p, a, k, rp, ra, v, s, c)). (* (1) *) query p: host, a: host, k: bitstring, rp: nonce, ra: nonce, v: bitstring, s: bitstring, c: bitstring; inj-event(endpeer(p, a, k, rp, ra, v, s, c)) ==> inj-event(beginauthenticator(p, a, k, rp, ra, v, s, c)). (* (3) *) query attacker(secretpeer); attacker(secretauthenticator). (1) ロール P(Peer) がロール A(authenticator) を正しく認証することすなわちロール P(Peer) が実行を完了したとき同じパラメータを用いて実行を完了したロール A(authenticator) が存在する (2) ロール A(authenticator) がロール P(Peer) を正しく認証することすなわちロール A(authenticator) が実行を完了したとき同じパラメータを用いて実行を完了したロール P(Peer) が存在する (3) 交換したセッション鍵 (master_secret) の秘匿性 5.4. 検証結果評価ツールの出力

10 RESULT inj-event(endpeer(p,a,k_2800,rp,ra,v_2801,s,c_2802)) ==> inj-event(beginauthenticator(p,a,k_2800,rp,ra,v_2801,s,c_2802)) true. RESULT inj-event(endauthenticator(p_5784,a_5785,k_5786,rp_5787, ra_5788,v_5789,s_5790,c_5791)) ==> inj-event(beginpeer(p_5784,a_5785,k_5786,rp_5787,ra_5788,v_5789, s_5790,c_5791)) is true. RESULT not attacker(secretauthenticator[]) is true. RESULT not attacker(secretpeer[]) is true. is 安全性はともに成り立つ攻撃に関する解説攻撃は発見されなかった 5.5. モデル化モデル化プロセスハッシュ関数公開鍵暗号電子署名のみを用いるためそのまま Dolev-Yao モデル上で記述できた 5.6. モデル化の妥当性特になし 5.7. 評価ツールとの相性暗号プロトコルの記述可能性特に制限はなかったセキュリティプロパティの記述可能性特に制限はなかった 5.8. 評価ツールの性能評価は瞬時に完了した

11 実行環境は以下のとおり Intel Core i7 L HGz Windows7 上の VirtualBox 仮想マシン上の Ubuntu Linux LTS メモリ 512MB ProVerif 1.86pl 備考本文書は総務省暗号認証技術等を用いた安全な通信環境推進事業に関する実証実験の請負成果報告書からの引用である

reduc forall k: key, x: bitstring; HMAC_SHA1(k, x) = hmac(k, x). reduc forall k: key, r: nonce; f1(k, r) = hmac(k, nonce_to_bitstring(r)). reduc foral

reduc forall k: key, x: bitstring; HMAC_SHA1(k, x) = hmac(k, x). reduc forall k: key, r: nonce; f1(k, r) = hmac(k, nonce_to_bitstring(r)). reduc foral 暗号プロトコル評価結果独立行政法人情報通信研究機構 1. プロトコル名 :EAP-AKA 2. 関連する標準 IETF:RFC4187 (http://www.ietf.org/rfc/rfc4187.txt) 3. 使用したツール :ProVerif 4. 評価の概要 :ProVerif による評価によりプロトコル内部で利用する異なる関数が同一あるいは相関がある場合になりすましおよび中間データの秘匿性を行う手順が発見された