主動攻擊下公鑰加密的計算可靠性研究

王文濤

91033部隊 山東 266034

0 引言

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

1 計算可靠性論證

1.1 聯系N-PAT與IND-CCA

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

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

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

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

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

1.2 符號與計算安全性質

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

1.2.1 跡性質

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

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

證明：每個計算跡Exec(η,R)通過函數c-1:bit→termA,∏建立的映射關系將比特串匹配到消息項，從而確定惟一符號跡tf。下面通過反證法證明tf有效，即如符號攻擊者Af執行下的符號跡tf是NDY的，則計算攻擊者可攻破Aε。記Af為攻擊協議的符號攻擊者，Ac是與Af對應的計算攻擊者(不攻擊密碼算法)，我們構建攻擊Aε的計算攻擊者B，并將Ac作為B的子程序。Af,Ac,B的運行關系如下：如Af發送模式對(pat0,pat1)，相應的，Ac發送的消息為 (pat0,pat1)的計算解釋 (c(pat0) ,c(pat1))，通過c:term→bit得到。因Ac為B的子程序，Ac將消息 (c(pat0) ,c(pat1))作為輸入給B，B解析(c(pat0) ,c(pat1))，調用加密預言機得到對c(patb) 的加密，最后猜測協議中使用的比特串輸出b'∈ [ 0,1]并返回給Ac，相應的，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的解析樹中，至少存在一條路徑，其葉子節點m|p不是Ei的子項，因為如所有葉子者在Ei中，就與矛盾，又因葉子節點為原子消息(主體標識符、密鑰、隨機數)，且m|p?Ei，則m|p不屬于主體標識符、不屬于公鑰、不屬于攻擊者A產生的隨機數、也不屬于A所擁有的私鑰，因此m|p只能為誠實主體的私鑰或誠實主體的隨機數。如m|p為誠實主體的隨機數(或私鑰)，如m|p的父節點是串接，則攻擊者都可提取該隨機數(或私鑰)，即Ei|-mp，這與m|p?Ei相矛盾；如m|p的父節點存在一個為公鑰加密{t}key，其中m|p為t的子項，因，則t和m|p都是秘密的。由此可見，如，則存在加密子模式 □key={t}key∈m且。因攻擊者Af發送消息mf，這意味著者Af可從它不能解密的密文□key中提取出誠實主體的私鑰或誠實主體的隨機數，那么B可推導出c(□key)，與N-PAT相矛盾，則tf有效。

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

記Pf為符號模型中的跡安全性質，由符號跡集合給定，如所有有效跡滿足Pf，即Execf(∏)∈pf，則∏|=fPf。如密碼協議運行進入某一狀態(Sidi,Si,Ki) ，該狀態下違背了密碼協議的某些預期的安全特性，此時便認為發生了針對密碼協議的攻擊。Pc為計算模型中相應的跡安全性質，由計算跡集合給定，如所有有效跡滿足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 秘密性

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

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

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

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

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

2 結束語

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

[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.