计算可靠的Diffie-Hellman密钥交换协议自动证明

?32??10? 2011?10?

? ? ? ?

Journal on Communications

Vol.32 No.10 October 2011

?????Diffie-Hellman??????????

?бē??ē?д?

??????? ????????┦??? ?? 410073?

?????????Diffie-Hellman????????????????????????????????????????????????CryptoVerif????????????Kerberos??????Ё????????┻???????????????CryptoVerif???????Diffie-Hellman?Kerberos??????????????????????????????????????????Н???????????????????????????

?????????Diffie-Hellman???Kerberos????????

Ё?????TP393 ??????B ?????1000-436X(2011)10-0118-09

Computationally sound mechanized proofs for

Diffie-Hellman key exchange protocols

FENG Chao, ZHANG Quan, TANG Chao-jing

(School of Electronic Science and Engineering, National University of Defense Technology, Changsha 410073, China)

Abstract: A computationally observational equivalence model for the Diffe-Hellman key agreement primitive was pro-posed and the soundness of the model was proved. Compared with prior works, this model can extend the power of the mechanized prover CryptoVerif directly. When applying the model to proving the public-key Kerberos, the de?ciency of the adversary’s capability was uncovered and an enhanced model for the adversary was presented. The model was vali-dated by verifying the public-key Kerberos in Diffie-Hellman mode with CryptoVerif automatically. Being different from current approaches, the verification procedure is both automatic and computationally sound. Key words: security protocols; Diffie-Hellman primitives; Kerberos protocol; mechanized proofs

1 ??

Diffie-Hellman????[1](DHKE)????????????????2???????????????????????????????????????SSL/TLS?SSH?Kerberos?ISO-9798-3?Just Fast Key?PKI????Ё???????

????DHKE??????????2??

???????????????????????????????Ё????????Dolev- Yao?????????-????????????????????????????????????DHKE???????▂??????????[2, 3]?Dolev-Yao?????????????Diffie-Hellman?????????????????????????????????????????????????????Ё[4,5]?

?????2010-12-07??????2011-04-04

??-????????????-??60872052?

Foundation Item: The National Natural Science Foundation of China (60872052)

?10? ?????????Diffie-Hellman?????????? g119g

??????????????????????-??????????????????????????Ё????????????????L?????????????????????????????

??????????????????????????????????????????[6]?????DHKE??????????????????Backes????????Kerberos??[7]?????????[8]????????Diffie-Hellman??(???DHINIT)?Lakhnech??????????Diffie-Hellman??????[9]?Datta?????????????[10]?????Diffie-Hellman?????????[11]??????????????

Blanchet???[11]Ё????????????CryptoVerif??????????????????????????????????????????[12,13]???????????[12]????DHKE????????????????DHKE????????

?????????????DHKE????????????DHKE?????????????CryptoVerif???????????????CryptoVerif?????????DHKE???????????????????????????????????????Ё???????????┻???[13]?????KerberosЁ???????????????????????

???????Kerberos??????????

???????????????????Diffie- Hellman?????Kerberos????????????????????????????????????????????????????DHKE???(?IKE, Just Fast Key?)?????

????????2?????????CryptoVerif??3???DHKE????????????????????????4????Kerberos??????????????[13]Ё????????┻??5??????

2 ??????

??????????CryptoVerif?????

?????[12]?

CryptoVerif??????????????????????????π?????c<M>?????c?????M?c(m)?????c??????????mЁ?new m:T????T???╓????m?P|Q????P?Q??????if M then P else Q?????????P; Q???

?P?Q?.????!i??

nP??P?n???????????????i?????Ё???x?x[i]???????find i?n such that defined(M) then P else Q??????????????i???Н???M????P?????Q?

CryptoVerif??????????????????????Ё???????????????????????????Ё????????????????????????????????????????Ё????????????????????????????

CryptoVerif????????(G1,?,Gm)≈ (G1′,?,Gm′)????????????????Ё???G??????Н??1???

?1

??????????

?? ?Н G::=

??? !????

?? new y??:T??,?,y :T (G??,?,G??)

╓???? (x??:T??,??,x??:T??)→FP ???? FP::= ???? M

- new x[i]:T;FP ╓???? let x[i]:T=M in FP

?? find (⊕????=??u????[??i]?n????suchthat defined

????

(M????,?,M?? )^??M?? then FP?? ) else FP

!i??

n new y1:T1,?,yl:Tl(G1,?,Gm)????T1,?,Tl???╓??y1,?,yl?????????

?G1,?,Gm????????????????!i??

n???????n??????????????????x?x[i]???

????(x1:T1,?,xl:Tl)→FP????????????8??????T1,?,Tl?????x1,?,xl???8??????FP?????????new x[i]:T;FP?????T???╓????

g120g ? ? ? ? ?32?

??xЁ????FP???let x[i]:T=M in FP??

?M???x????FP???find (⊕mj=1u??j[i??]?n??j suchthat defined(Mj1,?,Mjl)^Mj then FPj) else FP?

?????Mj1,?,Mjl?u

??j[i??]???????Mj?????FPj?????FP?????????

??G[i]??????????????G[j]Ё??????????????????IND-CCA2???Ё??????????????cchallenge???8????????????find (j?n suchthat defined(cchallenge)^cchallenge [j]= c then Error) else Decrypt(c,sk)?

?????????????(G1,?,Gm)≈ (G1′,?,Gm′)?????????????????????b??????2?8???(G1,?,Gm)?(G1′,?,Gm′)???????8????b?????b=0???????(G1,?,Gm)???????(G1′,?,Gm′)???????????????b′???b?????b′=b???????????????????????8????????2???([[G1]]|?|[[Gm]])?([[G1′]]|?|[[Gm′]])?[[G]]??8???G???????????????????????Ё???????????????2???????

3 DHKE??????

???CryptoVerif?????DHKE????????????DHKE???????????????????????????????????????????????? 3.1 DHKE?????

??????????DHKE???????????

1) ??Alice?Bob????????????p??Zp*????g?

2) Alice╓????Zp-1???x???X=gx mod p???X???Bob?

3) Bob╓????Zp?1???y?

??Y=gy mod p???Y???Alice?

4) Alice??Bob???Y??K=Yx mod p=(gy)x mod p = (gy)x mod p = gxy mod p??????Bob??????

5) Bob??Alice???X??K=Xy mod

p=(gx)y mod p = (gx)y mod p = gxy mod p??????Alice??????

6) Alice?Bob??K??????????????????????

DHKE?????????????Diffie- Hellman??(DDHA, decisional Diffie-Hellman as-sumption )???DDHA?????????A??

????<ga, gb, gab>?<ga, gb, gc>????

?Ёa, b, c??G?╓??????DDHA???????gx?gy??gxy????????3.2 ?????

CryptoVerif??????????????????????[12]?DDHA??????????

!i??

n new a:T; new b:T (()→ga, ()→gb, () →gab) ≈!i??

n new a:T ;new b:T ;new c:T (() →ga ,() → gb, ()→gc))

???????????????DDHA???????????Ё╓??a?b????????Ё????DHKEЁa?b????????╓????CryptoVerif???????????????Ё?

?CryptoVerif??????????????

??DHKE??????????3??????

1) ???????????(x,gy)?(y,gx)?????????????????????????????:(gx)y=(gy)x=gxy?

????????????????????????????????Ё?

2) ????

???????????????G???╓????

3) ????CryptoVerif???????????????????Ё?????????????????

???????????????[12]??????DHKE?????Ё? 3.3 ??????

DHKEЁ??????????????????????????gx(?gy)?????gxy???????????????????P?K??????gx(?gy)?gxy?????, ?S????x(?y)????????????????Н╓?????seed?

?Н1 (Diffie-Hellman??)????Trg?

?10? ?????????Diffie-Hellman?????????? g121g

Tsg?Tpg?Tkg????DHKEЁ╓????????????????????????g????????Щ??Н??exp:Ts→Tp???g??????????Ts????x???Tp????gx?Diffie-Hellman??DHA=(S, P, K)??3?????

1) DH??????S:Tr→Ts?????Tr?????r?????Ts????(?x?y)?

2) DH??????P:Tr→Tp?????Tr?????r?????Tp????(?gx?gy)?P????????????P(r)??r???

3) DH????????K:Ts×Tp?Tk???Ts(?x)?Tp(?gy)????????????(?gxy)?

?????????????????DH???DH???????????r:Tr; exp(S(r))? P(r)????????????????x?Ts, ?y?Ts,?gx?Tp,?gy?Tp, (K(x, gy)=K(y,gx)) ? ((exp(x)= gx?exp(y)=gy)?(x =y?gx=gy))???ā??????????CryptoVerif??K(x,gy)=K(y,gx)??????????(exp(x)= gx?exp(y)=gy)?(x =y?gx=gy)?

??DHA??????DHKE?????????Lg≈Rg, ??g????????Щ?

Lg=!i??N new r:Ts;(() →P(r), !i??

N??(gy : Tp) →K(S(r), gy))

Rg=!i??N new r:Ts;(() →P′(r), !i??

N??(gy : Tp) → find j?N1 suchthat defined(gy[j], r1[j])?otheruses (r1[j])?gy = gy[j] then r1[j]

orfind j?N1, k?N suchthat defined(r[k], gy[j,k], r1[j,k])?otheruses(r1[j,k])?(exp(S′(r)) = gy[j,k] ?gy=exp(S′(r[k]))) then r1[j,k]

else new r1: Tk;r1).

??S′?P′??S?P??????????L?R??????????????CryptoVerif???????????????

???DHKE????CryptoVerif?????L??????R?????????????????Ё??LЁ??????????RЁ??????R????2??????????????j?N1, ??gy[j]??gy????????????K(S(r),gy), ??????????r1[j]???????????????????j?N1, k?N?

??exp(S′(r)) = gy[j,k]?gy=exp(S′(r[k]))?????????????????K(S′(r[k]),P′(r))??Ё?gy=exp(S′(r[k]))=P′(r[k])??+???????K(S′(r[k]),P′(r))?K(S′(r), P′(r[k]))????????2??????????????r1[j,k]??2???????????Tk???╓??r1???????

L≈R?????????????Ё?????????????????Ё??? 3.4 ?????

????CryptoVerif?DHKE????????????????G??DDHA?????????????Lg≈Rg?????ˊ1???

?ˊ1 ?????G?????g??G????Diffie-Hellman??(DDHA)??МLg≈Rg?

??ˊ?????????Н??ˊ??Ё??Н2??Н3???DDHA???????Lg≈Rg?????????ˊ1?????2??????

?Н2 (DDHA????ExpgDDHA(ADDHA,b))??????????2?Tr???╓??ra?rb????Tk???╓??rc??????????SDHra,rb,rc()8?????????8??????b=0???<P(ra),P(rb),K(S(ra),P(rb))>?????<P(ra),P(rb),rc>????????????b???

?b′???????1????Ё????r←?R

?Tā????T???╓???????rЁ???

?rR

1=r2←??Tā????T???╓???????r1?r2Ё?

??Exp?????? ??(A?????? ,b)

??r?? ←?

?Tr????

??,??←??T???r??←??T??b′←A?????????????? ??????

????

??????????b′

?1 DDHA????

????????Н??ADDHA???AdvDDHA

g

(ADDHA)=Pr[ExpDDHADDHA

g(ADDHA,0)=1]??Pr[Expg(ADDHA, 1)=1]????????AdvDDHA)=max{DDHAg(tAAdv ??????

g

(ADDHA)}??Ё?t???????

????ExpgDDHA?DDHA????????????G??DDHA?????????g?

g122g ? ? ? ?

?32?

?МAdvgDDHA(t)???Щ???

?Н3 (DHKE????ExpgDHKE(ADHKE,b))??????????qn?Tr???╓??ra[i]?qn2?Tk???╓??rc[i,j] (0<i,j?qn)????????qn?8???EGi()?KGi(·)?????qn???????????????

?EGi()????????P(ra[i])?????? ?KGi(·)??????????????????gb?????????gb???????EGj()8??????????b=0?1????K(S(ra[i]),gb)?rc[i,j]???????Tk???╓??r??????????????b′???b??????b′=b?????????Ё??????????????Ё?????ExpgDHKE???????2?????

??Exp

???? ????

(A???? ??,b)

??i,j∈[1,q ],??r??[i]←????T????r??[i,j]=r??[j,i]←???

?T??

b′←A??????????????????????????????????? ??

????????

?????

??b′

?2 DHKE????

??????????Н??ADHKE???

AdvgDHKE(ADHKE)=Pr[ExpgDHKE(ADHKE,0)=1]??Pr[ExpgDHKE·

(ADHKE, 1)=1]????????AdvDHKE

g

(t)= max{AAdvDHKE

g(ADHKE)}??Ё?t??????? ???? ??

?????ExpgDHKE

(ADHKE,0)??????L????ExpgDHKE(ADHKE,1)????R????М??Lg≈Rg????AdvgDHKE(t)???Щ???

?ˊ1 ???G???AdvgDDHA(t)???Щ????AdvgDHKE(t)???Щ???

?? ????????????A?????ExpgDHKE??М???????ExpgDDHA???BA? 1) ??ExpgDHKE????Ё?????ExpHl(?Ё?0?l?qn)???3???

??ExpHl????????l?i?8??KGi(·)???╓????НPl=Pr[ExpHl=1]???ExpHl??1???????l=qn??ExpHl?ExpgDHKE(ADHKE,0)????l=0??ExpHl?ExpgDHKE(ADHKE,1)???????AdvgDHKE(A)= Pqn??P0?

2) ????A????ExpgDDHA???BA?BA???????4???

?? ExpH??(?Ё?0?l?q??)

a) ??i,j∈[1,q??],??r [i]←?

???T????r??[j,i]=r??[i,j]←????T

???b) ????A???????????A?EG ()?KG (·)8?????:

??????EG ()???????P(r??[i])???A? ??????KG (·)??????????gb??????? ??i?l????????j?l??gb?EG??()???????K(S(r??[i]),gb)???A??????????

??i>l????????j?l??gb?EG??()???????r??[i,j]???A?????????? c) ??????A??b′? d) ????b′?

?3 Ё?????

a) ??SDH???? ???? ????()8?????<gx,gy,gz>? b) ╓?????[1,q??]Ё???l? c) ??i∈[1,??,l?1]∪[l+2,??,q??] j∈[i,q??],

??r??[i]←????T r??[i,j]←???

?T???

d) ????A?

?+?????????EG ()?KG (·)???? ??????EG ()????

??i≠l,?i≠l+1?????P(r??[i])???A? ??i=l????gx?

??i=l+1????gy?

??????KG (·)??????????gb?????????

??i<l??????????gb?EG??()??j<l???K(S(r??[i]),gb)???A????r??[i, j]???A????????EG??()?????????

??i>l+1??????????gb?EG??()???r??[i, j]???A????????EG??()?????????

??i=l??????gb=gy????gz?????????gb?EG??()??j<l???K(S(r??[i]),gb)???A????r??[i,j]???A????????EG??()????????? ??i=l+1??????gb= gx????gz?????????gb?EG??()??j<l???K(S(r??[i]),gb)???A????r??[i,j]???A????????EG??()????????? e) ??A??????b′? f) ??b′???b????

?4 ??B?????

?????ExpgDDHA(BA,0)??SDHra,rb,rc()??<P(ra),P(rb),K(S(ra),P(rb))>?KGl(·),KGl+1(·)????????????????l+1?i, KGi(·)???╓??????ExpHl+1????????