王文濤

91033部隊 山東 266034

0 引言

密碼協(xié)議分析領(lǐng)域有兩類值得注目的方法：符號方法和計算方法。符號方法大都基于DolevYao- 模型，采用模型檢測或定理證明。此方法可有效實現(xiàn)自動化，但均假設(shè)協(xié)議所采用的算法是完美的，攻擊者在進行密碼分析時得不到任何有用的信息，沒有考慮由密碼算法以及密碼算法與協(xié)議交互所產(chǎn)生的安全問題。計算方法假定密碼算法是不完美的，攻擊者在多項式時間內(nèi)對協(xié)議進行任意攻擊，若攻擊者能以不可忽略的概率和較少的計算代價偽造協(xié)議消息成功，則認為協(xié)議是不安全的，這種方法為密碼原語和協(xié)議提供精確的安全定義，可提供較強的安全保證，但是大都采用手工證明，自動化程度低。

1 計算可靠性論證

1.1 聯(lián)系N-PAT與IND-CCA

定理 1：如公鑰加密方案Aε=(KG,ε,D)是N-PAT安全的，則Aε也是IND-CCA安全的。

證明：假定A為攻擊IND-CCA的攻擊者，因IND-CCA不允許加密秘密密鑰，所以A不能詢問加密預(yù)言機對 □key,l(term)類型消息的加密，因此不能攻擊N-PAT。但因為A對加密預(yù)言機的詢問為比特串對，而比特串對也可看作模式對，因此可以構(gòu)建一攻擊者B攻擊N-PAT，并將A作為B的子程序。假定N-PAT產(chǎn)生n個密鑰對(keyi,keyi-1)。

AdvB(η) = P r[(b' =b)]- 1 2，由全概率公式可得到

因A是B的子程序，則可用A的執(zhí)行代替B，且IND-CCA所使用的密鑰對屬于 (keyi,keyi-1)，預(yù)言機屬于(Oencrypti,Odecrypti)，我們密鑰對為 (key1,key1-1)，預(yù)言機為(Oencrypt1,Odecrypt1)。

因Aε是N-PAT安全的，則AdvB(η)≤η，所以AdvA(η)≤η，所以Aε是IND-CCA安全的。

1.2 符號與計算安全性質(zhì)

協(xié)議的認證性與完整性都是跡性質(zhì)，即可從跡中觀察性質(zhì)是否保持。以認證性“如Bob接受某一密鑰K用于與Alice通信，則Alice也參與產(chǎn)生K的協(xié)議的相同會話中”為例，對給定的任意跡我們都可看出 Bob是否接受此密鑰以及Alice是否參與相同協(xié)議的相同會話，因此認證性是跡性質(zhì)。但秘密性不是基于跡的，如計算不可區(qū)分規(guī)定計算觀察者不可以區(qū)分秘密信息傳遞的情況與非秘密信息傳遞的情況，但從一個單獨的跡上不能看出觀察者是否成功區(qū)分，這時，需觀察在跡上的概率分布，并決定在此分布上的成功概率。

1.2.1 跡性質(zhì)

此部分借鑒Micciancio-Warinschi方法證明跡性質(zhì)。

定理2：如公鑰加密方案滿足N-PAT，則與計算跡相對應(yīng)的抽象表示的符號跡一定是有效Dolev-Yao跡，即Pr[?tf∈Execf( ∏ ) |tfExecA,∏(η,R) ]≥1 -f(η)。

證明：每個計算跡Exec(η,R)通過函數(shù)c-1:bit→termA,∏建立的映射關(guān)系將比特串匹配到消息項，從而確定惟一符號跡tf。下面通過反證法證明tf有效，即如符號攻擊者Af執(zhí)行下的符號跡tf是NDY的，則計算攻擊者可攻破Aε。記Af為攻擊協(xié)議的符號攻擊者，Ac是與Af對應(yīng)的計算攻擊者(不攻擊密碼算法)，我們構(gòu)建攻擊Aε的計算攻擊者B，并將Ac作為B的子程序。Af,Ac,B的運行關(guān)系如下：如Af發(fā)送模式對(pat0,pat1)，相應(yīng)的，Ac發(fā)送的消息為 (pat0,pat1)的計算解釋 (c(pat0) ,c(pat1))，通過c:term→bit得到。因Ac為B的子程序，Ac將消息 (c(pat0) ,c(pat1))作為輸入給B，B解析(c(pat0) ,c(pat1))，調(diào)用加密預(yù)言機得到對c(patb) 的加密，最后猜測協(xié)議中使用的比特串輸出b'∈ [ 0,1]并返回給Ac，相應(yīng)的，A接收c-1(b')，通過c-1:bit→term得到。如公鑰加

f密方案滿足N-PAT，則Adv= | Pr[(b' =b) ]-12|≤f(η)，。

如tf是NDY的，則當

(Sidi+1,Si+1,Ei+1)時，。則在mf的解析樹中，至少存在一條路徑，其葉子節(jié)點m|p不是Ei的子項，因為如所有葉子者在Ei中，就與矛盾，又因葉子節(jié)點為原子消息(主體標識符、密鑰、隨機數(shù))，且m|p?Ei，則m|p不屬于主體標識符、不屬于公鑰、不屬于攻擊者A產(chǎn)生的隨機數(shù)、也不屬于A所擁有的私鑰，因此m|p只能為誠實主體的私鑰或誠實主體的隨機數(shù)。如m|p為誠實主體的隨機數(shù)(或私鑰)，如m|p的父節(jié)點是串接，則攻擊者都可提取該隨機數(shù)(或私鑰)，即Ei|-mp，這與m|p?Ei相矛盾；如m|p的父節(jié)點存在一個為公鑰加密{t}key，其中m|p為t的子項，因，則t和m|p都是秘密的。由此可見，如，則存在加密子模式 □key={t}key∈m且。因攻擊者Af發(fā)送消息mf，這意味著者Af可從它不能解密的密文□key中提取出誠實主體的私鑰或誠實主體的隨機數(shù)，那么B可推導(dǎo)出c(□key)，與N-PAT相矛盾，則tf有效。

由此我們知道通過雙射函數(shù)c:term→bit，符號跡與計算跡可以互相轉(zhuǎn)化，如公鑰加密方案Aε滿足N-PAT，計算攻擊者的能力與符號攻擊者的能力相同。

記Pf為符號模型中的跡安全性質(zhì)，由符號跡集合給定，如所有有效跡滿足Pf，即Execf(∏)∈pf，則∏|=fPf。如密碼協(xié)議運行進入某一狀態(tài)(Sidi,Si,Ki) ，該狀態(tài)下違背了密碼協(xié)議的某些預(yù)期的安全特性，此時便認為發(fā)生了針對密碼協(xié)議的攻擊。Pc為計算模型中相應(yīng)的跡安全性質(zhì)，由計算跡集合給定，如所有有效跡滿足Pc的概率是不可忽略的，即對任意概率多項式時間下的攻擊者Ac而言，P r[ExecA,∏(η,R)?Pc]≤η，則∏|=cPc。

定義 1[可信抽象]：如(?tf∈Execf(∏),?tc∈ExecA,∏(η,R))

(tftc,tf∈pf) → P r [tc?Pc] ≤η，則稱Pf是Pc的可信抽象，記為concr(pf)?pc。

定理3：如Pf是Pc的可信抽象，且Aε滿足N-PAT，則 ∏ |=fPf→∏|=cPc。即如加密方案滿足N-PAT，且符號模型中某命題成立，則在計算模型中該命題也成立。

證明：由定理2可知，對任一計算跡tc∈ExecA,∏(η,R)，都存在一符號跡tf∈Execf( ∏ ),tf∈Pf使得tf?tc，又因為∏|=fPf，則tf∈pf，由定義1可知 ?tc∈ExecA,∏(η,R)(tc∈pc)，即∏|=cPc。形式化表示如下：則|ccP∏=。

1.2.2 秘密性

在符號模型中，秘密性可以描述為跡性質(zhì)，如某消息不能由攻擊者推導(dǎo)出來，則稱該消息是秘密的。在計算模型中，只有當某消息的任意部分都不能由攻擊者推導(dǎo)出來，才稱該消息是秘密的。

借鑒Véronique Cortier對協(xié)議秘密性的定義，將協(xié)議秘密性描述為隨機數(shù)的秘密性，并證明隨機數(shù)秘密性的可靠性。在符號模型中，對任一有效符號跡 (Sid0,S0,E0)…(Sidn,Sn,En)，如攻擊者都不能推導(dǎo)出隨機數(shù)n，則此隨機數(shù)是秘密的。在計算模型中，隨機數(shù)nc的秘密性描述如下：N-PAT博弈產(chǎn)生兩個隨機數(shù)n0、n1(與pat0、pat1類似)。攻擊者目的是猜測nb,b∈ { 0,1}，如攻擊者猜測成功的概率可忽略，則稱nc是秘密的。

定理4：記N為協(xié)議∏的隨機數(shù)。如公鑰加密方案Aε滿足N-PAT，且在符號模型中N是秘密的，則在計算模型中與N對應(yīng)的隨機數(shù)Nc也是秘密的。

證明：與定理2類似，構(gòu)建攻擊者Af,Ac,B，如Af發(fā)送包含N的模式對 (pat0,pat1)，其中，在pat0中N為N0，在pat1中N為N1，則Ac發(fā)送的消息為 (pat0,pat1)的計算解釋(c(pat0) ,c(pat1))，其中，在c(pat0)中與N對應(yīng)的隨機數(shù)Nc為Nc0，在c(pat1)中Nc為Nc1。因公鑰加密方案Aε滿足N-PAT，則pat0,pat1不可區(qū)分。則根據(jù)定理2，符號攻擊者的攻擊能力與計算攻擊者的能力相同，所以

因為在符號模型中N是秘密的，即，又因為由定理 2中的證明過程可知，存在加密子項如在計算模型中Nc不是秘密的，即Ac|-Nc，則相對應(yīng)的，攻擊者Af可從它不能解密的密文{t}key中提取出誠實主體的隨機數(shù)，產(chǎn)生NDY跡，由推論的逆否命題得到公鑰加密方案Aε不滿足N-PAT，B可攻破Aε，這與前提加密方案滿足N-PAT相矛盾。

2 結(jié)束語

原始Micciancio-Warinschi方法不能分析包含類型消息的協(xié)議，這限制了它的應(yīng)用領(lǐng)域。本文對Micciancio-Warinschi方法進行了擴展，并證明了在公鑰加密方案滿足安全定義N-PAT時，符號形式化系統(tǒng)所得結(jié)論在計算模型中也成立。基于該結(jié)論，可以構(gòu)建或改進符號形式化分析系統(tǒng)，使其具有計算可靠性。下一步，我們將在符號模型下考慮密碼算法的影響，實現(xiàn)密碼協(xié)議的安全性驗證。

[1]ABADI M,ROGAWAY P.Reconciling two views of cryptography(The computational soundness of formal encryption)[C].In Proc.1st IFIP International Conference on Theoretical Computer Science.Springer.2000.volume 1872 of LNCS 3-22.

[2]ABADI M,JURJENS J.Formal eavesdropping and its computational interpretation[C].In Proc.4th International Symposium on Theoretical Aspects of Computer Software (TACS). 2001.

[3]MICCIANCIO D,WARINSCHI B.Completeness theorems for the Abadi-Rogaway logic of encrypted expressions[J].Journal of Computer Security.2004.