協(xié)議組合邏輯在實(shí)例化空間模型中的語(yǔ)義解釋

肖茵茵，蘇開樂

（1.廣東技術(shù)師范學(xué)院計(jì)算機(jī)學(xué)院，廣東 廣州 510665；2.中山大學(xué)信息科學(xué)與技術(shù)學(xué)院廣東省信息安全重點(diǎn)實(shí)驗(yàn)室，廣東 廣州 510275；3.浙江師范大學(xué)數(shù)理與信息工程學(xué)院，浙江 金華 321004）

協(xié)議組合邏輯在實(shí)例化空間模型中的語(yǔ)義解釋

肖茵茵1，2，蘇開樂2，3

（1.廣東技術(shù)師范學(xué)院計(jì)算機(jī)學(xué)院，廣東 廣州 510665；2.中山大學(xué)信息科學(xué)與技術(shù)學(xué)院廣東省信息安全重點(diǎn)實(shí)驗(yàn)室，廣東 廣州 510275；3.浙江師范大學(xué)數(shù)理與信息工程學(xué)院，浙江 金華 321004）

安全協(xié)議的驗(yàn)證是個(gè)不可判問題.為了對(duì)實(shí)例化空間邏輯ISL的語(yǔ)義表達(dá)能力給出理論上的衡量與評(píng)價(jià)，選擇另一種實(shí)用的協(xié)議組合邏輯PCL，分析了ISL和PCL之間的關(guān)系.在此基礎(chǔ)上，將PCL的索狀空間語(yǔ)義模型轉(zhuǎn)換為ISL的實(shí)例化空間語(yǔ)義模型，在實(shí)例化空間下對(duì)PCL的主要公式、定理、推導(dǎo)規(guī)則做了語(yǔ)義解釋.研究表明，實(shí)例化空間能夠完全表示PCL的語(yǔ)義，且ISL的語(yǔ)義表達(dá)能力強(qiáng)于PCL.新的模型解釋使PCL更易于擴(kuò)展，且使得用PCL理論驗(yàn)證的協(xié)議能夠利用ISL的自動(dòng)化驗(yàn)證工具SPV進(jìn)行分析.

安全協(xié)議驗(yàn)證；實(shí)例化空間；協(xié)議組合邏輯；索狀空間；語(yǔ)義解釋

1 引言

安全協(xié)議形式化驗(yàn)證邏輯是檢驗(yàn)安全協(xié)議正確性的一類重要方法.其中，實(shí)例化空間邏輯ISL（Instantiation Space Logic）［1-2］以實(shí)例化空間為語(yǔ)義模型，并擁有一組盡可能完備的純命題邏輯的公理模式，可驗(yàn)證工業(yè)級(jí)復(fù)雜協(xié)議的認(rèn)證性、秘密性等相關(guān)安全性質(zhì).因?yàn)閰f(xié)議的驗(yàn)證是個(gè)不可判問題［3］，所以無法直接對(duì)ISL進(jìn)行嚴(yán)格的完備性證明.為了對(duì)ISL的語(yǔ)義表達(dá)能力給出理論上的衡量與評(píng)價(jià)，本文選取Dolev-Yao模型下的另一種實(shí)用的安全協(xié)議驗(yàn)證邏輯-協(xié)議組合邏輯PCL（Protocol Compositional Logic）［4-5］，利用PCL與ISL的相似性，用ISL的實(shí)例化空間語(yǔ)義模型解釋PCL，轉(zhuǎn)換的成功說明ISL的語(yǔ)義表達(dá)能力足以描述PCL.另一方面，我們還說明了現(xiàn)有的PCL不能夠完全表示ISL的語(yǔ)義，這種單向的語(yǔ)義對(duì)應(yīng)關(guān)系證明ISL的公理集比現(xiàn)有的一些驗(yàn)證邏輯刻畫了更一般的情形，具有較強(qiáng)的語(yǔ)義表達(dá)能力.目前，國(guó)內(nèi)外對(duì)安全協(xié)議形式化驗(yàn)證邏輯語(yǔ)義方面的研究較少，因此該工作在一定程度上填補(bǔ)了這方面研究的空白.

PCL主要用于驗(yàn)證公鑰加密體制下協(xié)議的認(rèn)證性和秘密性，是一種包含模態(tài)算子和描述協(xié)議動(dòng)作的進(jìn)程算子的邏輯，其推理過程是基于動(dòng)作的：即把協(xié)議的執(zhí)行過程看成是參與主體的動(dòng)作集合，其公理和推導(dǎo)規(guī)則與每一步協(xié)議的執(zhí)行動(dòng)作相關(guān)，每個(gè)動(dòng)作導(dǎo)致一個(gè)推理結(jié)果的產(chǎn)生，最后在協(xié)議動(dòng)作執(zhí)行完畢時(shí)檢驗(yàn)相應(yīng)的邏輯結(jié)果是否滿足相關(guān)的安全性質(zhì).這種“模態(tài)動(dòng)作邏輯”在驗(yàn)證過程中的系統(tǒng)狀態(tài)會(huì)隨著協(xié)議規(guī)模的增大而迅速增加，難以自動(dòng)化.迄今為止，還未見到與PCL對(duì)應(yīng)的自動(dòng)化驗(yàn)證工具.而ISL的公理集在算法上可完全實(shí)現(xiàn)，其自動(dòng)化驗(yàn)證工具SPV（Security Protocol Verifier）能高效驗(yàn)證大規(guī)模復(fù)雜協(xié)議的性質(zhì)［1，6-7］.本文把PCL的語(yǔ)義轉(zhuǎn)化到實(shí)例化空間下，將使得用PCL理論驗(yàn)證的協(xié)議能夠利用SPV進(jìn)行自動(dòng)化驗(yàn)證.另外，因?yàn)閷?shí)例化空間更具有一般性，因此該模型解釋下的PCL具有更好的擴(kuò)展性.

2 實(shí)例化空間邏輯ISL與協(xié)議組合邏輯PCL簡(jiǎn)介

為便于理解，本節(jié)將對(duì)實(shí)例化空間邏輯ISL與協(xié)議組合邏輯PCL作簡(jiǎn)單介紹，關(guān)于本節(jié)內(nèi)容的詳細(xì)論述可參見文獻(xiàn)［1-2］和［4-5］，本文未特別說明的符號(hào)和術(shù)語(yǔ)均與文獻(xiàn)一致.

2.1 實(shí)例化空間邏輯ISL

ISL的加密消息交換CME(Cryptographical Message Exchange)模型Σ=（M，K，e，Ag，Pk，Sk，Label，Nonce，Gn，Dh，Init，Recv，Sent）定義在消息代數(shù)（M，K）基礎(chǔ)上，用于說明主體之間如何進(jìn)行加密消息的交換.為方便起見，CME模型中定義了一些有用的函數(shù)，如Sub、Recvs、Poss、Encr、Computes、Fresh等等.另一方面，安全協(xié)議P是由原子消息符號(hào)集和協(xié)議體構(gòu)成的多元組（AG，PK，SK，INIT，BODY），P中所有消息符號(hào)用MSGP來表示.協(xié)議中的各個(gè)角色都有自己的局部協(xié)議，用于刻畫與自身有關(guān)的行為.對(duì)于一個(gè)協(xié)議P和CME模型Σ，二元組（ρ，c）表示以隨機(jī)數(shù)或時(shí)戳c為標(biāo)識(shí)消息的主體ρ的局部運(yùn)行.對(duì)于每個(gè)局部運(yùn)行（ρ，c），可定義一個(gè)消息賦值函數(shù)：f:MSGP→M，對(duì)于每個(gè)MP∈MSGP，f（MP）是在P中的局部運(yùn)行（ρ，c）中扮演協(xié)議所定義的MP的具體消息.若f描述了局部運(yùn)行（ρ，c）中主體ρ的動(dòng)作與角色A的行為間的對(duì)應(yīng)關(guān)系，則稱f為一個(gè)（ρ，c，A，l）-函數(shù)（l是協(xié)議執(zhí)行的某一步，必須小于A的局部協(xié)議的長(zhǎng)度），又稱為A的實(shí)例化函數(shù)，記為

實(shí)例化空間Ω=（Σ，L，F(xiàn)，譓）是一個(gè)基于實(shí)例化函數(shù)和CME模型的安全協(xié)議驗(yàn)證邏輯語(yǔ)義模型.其中，Σ是CME模型，L是協(xié)議P相關(guān)聯(lián)的標(biāo)識(shí)消息集，F(xiàn)是實(shí)例化函數(shù)集，譓是關(guān)于主體Ag行為的假設(shè)集.

實(shí)例化空間邏輯是以實(shí)例化空間為語(yǔ)義模型的邏輯理論ΘP.ΘP中的role、norm、poss、sees、said、fresh和secr等原子公式描述了主體在局部運(yùn)行中如何扮演協(xié)議角色.ΘP的公理模式基于純命題邏輯，其中最重要的公理為角色假設(shè)定理和（n，1）-Secrecy定理.這些公理比現(xiàn)有的一些驗(yàn)證邏輯刻畫了更一般的情形，可有效地驗(yàn)證協(xié)議的安全性質(zhì).

2.2 協(xié)議組合邏輯PCL

PCL的基本概念有項(xiàng)、動(dòng)作、索帶和索狀空間.

串S為動(dòng)作序列：S：=aS|a，a∈action.～為作用于串上的關(guān)系：ST～TS當(dāng)且僅當(dāng)S、T之間沒有值的相互依賴（S、T為串）.設(shè)≈為包含～的自反傳遞閉包的最小等價(jià)關(guān)系，則索帶C為串集合在≈劃分下的等價(jià)類.直觀上看，索帶就是不存在值傳遞的串拼接的集合.每個(gè)索帶都用中括號(hào)［］括起來，［］表示空索帶.

協(xié)議角色與具體主體的對(duì)應(yīng)通過為索帶提供靜態(tài)接口實(shí)現(xiàn).設(shè)協(xié)議P的角色集合為A主體集合為定義Asi為增加靜態(tài)接口操作：，其中為角色A中需要實(shí)例化的角色名，（A，B，…）稱為A的靜態(tài)接口.定義Sb為靜態(tài)綁定操作：Sb（A，ρ，μ，…）=（）［］<ρ，μ，…>；Asi（A），其中ρ，μ，…∈<ρ，μ，…>；Asi（A）表示將Asi（A）中的角色名依次替換成<ρ，μ，…>中的具體主體名.靜態(tài)綁定操作將靜態(tài)接口中的抽象變量替換成具體值，使協(xié)議角色對(duì)應(yīng)于具體主體.

協(xié)議P的一個(gè)運(yùn)行R是P中角色發(fā)生消息交互的狀態(tài)序列.一個(gè)初始狀態(tài)可能產(chǎn)生不同的狀態(tài)序列，因此可能產(chǎn)生不同的運(yùn)行.索狀空間包含了協(xié)議P所有角色之間消息交互的所有可能狀態(tài)，從而包含了P的所有可能運(yùn)行.狀態(tài)的每次轉(zhuǎn)換使得索帶中的某個(gè)變量x被某個(gè)確定的項(xiàng)m替代，事件則為動(dòng)作a中所有變量都被確定的項(xiàng)替代的結(jié)果.設(shè)A為協(xié)議P的角色，稱為A在R中的軌跡，其中為作用在ai上且在R中發(fā)生的事件.直觀理解，R|A表示了角色A在R中的局部運(yùn)行.

PCL基于一階邏輯與模態(tài)邏輯，以協(xié)議P的一次運(yùn)行R為語(yǔ)義模型.該邏輯除了通常的一階謂詞公式外，還有一個(gè)描述主體行為的原子公式集以及模態(tài)算子.在此基礎(chǔ)上，PCL提出了一系列依賴于主體動(dòng)作的定理和推導(dǎo)規(guī)則，用于驗(yàn)證協(xié)議相關(guān)的安全性質(zhì).

2.3 PCL與ISL的相似性

PCL理論與ISL理論具有一定的相似性：

1.兩個(gè)理論都屬于安全協(xié)議邏輯證真法，基于Dolev-Yao攻擊者模型對(duì)協(xié)議所有可能的運(yùn)行進(jìn)行推理，證明協(xié)議在無窮會(huì)話中的正確性，并且在推理過程中允許存在未完成的會(huì)話；

2.兩個(gè)理論都無需對(duì)攻擊者的行為進(jìn)行顯式的模型化和推理，而是將攻擊者模型視為協(xié)議運(yùn)行環(huán)境的一個(gè)因素；

3.兩個(gè)邏輯的語(yǔ)義都很自然，不像BAN類邏輯［8-9］一樣需要對(duì)協(xié)議進(jìn)行非標(biāo)準(zhǔn)的理想化.

這些相似性使PCL和ISL存在著某些對(duì)應(yīng)關(guān)系.在下一節(jié)中，我們將證明ISL的實(shí)例化空間語(yǔ)義模型可以完全解釋PCL；但是，PCL具有一定的局限性，因此不能夠完全解釋ISL的語(yǔ)義，這將在第4節(jié)中進(jìn)一步說明.

3 用實(shí)例化空間解釋PCL

PCL以索狀空間作為語(yǔ)義模型，ISL以實(shí)例化空間作為語(yǔ)義模型.因此，實(shí)現(xiàn)從PCL到ISL語(yǔ)義轉(zhuǎn)換的前提是索狀空間能夠轉(zhuǎn)換成對(duì)應(yīng)的實(shí)例化空間.本節(jié)首先將索狀空間中有關(guān)消息的概念對(duì)應(yīng)到實(shí)例化空間的CME模型集合中，并將協(xié)議形式做相應(yīng)轉(zhuǎn)換，再為索狀空間生成對(duì)應(yīng)的實(shí)例化空間集合，最后實(shí)現(xiàn)兩種邏輯語(yǔ)義模型的轉(zhuǎn)換，證明由索狀空間語(yǔ)義模型解釋的PCL能夠被實(shí)例化空間語(yǔ)義模型解釋，將PCL的主要公式、定理、推導(dǎo)規(guī)則對(duì)應(yīng)到ISL中.

3.1 由索狀空間構(gòu)建CME模型

3.1.1 從消息項(xiàng)到消息代數(shù)

直觀上看，索狀空間的項(xiàng)集包括協(xié)議所需的全體消息集，索狀空間的密鑰項(xiàng)集則對(duì)應(yīng)消息代數(shù)中的密鑰消息集，因此PCL的項(xiàng)集可以對(duì)應(yīng)CME模型的消息代數(shù).

3.1.2 構(gòu)建CME模型

索狀空間只描述主體動(dòng)作之間的順序關(guān)系，不考慮動(dòng)作執(zhí)行的具體時(shí)間，是一個(gè)相對(duì)抽象的模型；而實(shí)例化空間更為具體，需要描述主體行為的具體執(zhí)行時(shí)間.因此，一個(gè)索狀空間對(duì)應(yīng)了無窮多個(gè)具體的CME模型.

證明：首先，每個(gè)Σ都是一個(gè)描述C中消息交換的CME模型：由定理1可知與構(gòu)成了消息代數(shù)；黑客控制下的通信環(huán)境e由C的非誠(chéng)實(shí)主體集構(gòu)成；Ag對(duì)應(yīng)的誠(chéng)實(shí)通信主體集；Pk元組集合描述了中每個(gè)主體的公鑰和對(duì)應(yīng)的私鑰；索狀空間主要描述了公鑰體制下的協(xié)議，在對(duì)稱密鑰體制下只對(duì)DH密鑰進(jìn)行了描述，因此主體間的共享密鑰集Sk只包含DH密鑰；索狀空間未引入時(shí)戳的概念，因此標(biāo)識(shí)信息集Label只包含隨機(jī)數(shù)集Nonce；Nonce函數(shù)將每個(gè)主體映射到該主體通過新建動(dòng)作產(chǎn)生的消息集，由于在索狀空間中新建動(dòng)作產(chǎn)生的項(xiàng)具有隨機(jī)數(shù)的作用，因此Nonce函數(shù)可以看作是從每個(gè)主體到其產(chǎn)生的隨機(jī)數(shù)集的映射，而且索狀空間假定新建動(dòng)作在主體執(zhí)行協(xié)議前一次性完成，與CME模型中隨機(jī)數(shù)在初始化過程中產(chǎn)生是一致的；Init將主體映射到其初始擁有的明文消息；Recv和Sent函數(shù)分別將主體映射到該主體通過接收動(dòng)作和發(fā)送動(dòng)作收到和發(fā)出的消息集.

其次，因?yàn)樗鳡羁臻g不描述主體行為的具體時(shí)間，所以CME模型中的t是任意的，所有滿足定理2中條件的CME模型都描述了.因此一個(gè)索狀空間C的消息交換對(duì)應(yīng)了一個(gè)CME模型的集合.

備注1在索狀空間對(duì)應(yīng)的CME模型中，Sk和Label包含的內(nèi)容都比原有的定義有所縮減，這證明CME模型比索狀空間下的消息定義、交換等概念更具一般性.

3.2 協(xié)議形式的轉(zhuǎn)換

索狀空間與實(shí)例化空間對(duì)協(xié)議有著不同的形式化描述，索狀空間下的協(xié)議形式能夠轉(zhuǎn)換到實(shí)例化空間下.設(shè)索狀空間?描述了協(xié)議P，則有如下定理：

定理3的證明與定理2類似，在此不再詳述.可以看到，轉(zhuǎn)換后角色的共享密鑰集只包含DH密鑰.

3.3 從索狀空間到實(shí)例化空間

1.R中存在靜態(tài)綁定操作：Sb（A，ρ，…）=（）［］<ρ，…>；Asi（A）=（）［］<ρ，…>；（A，…）Create（A）；

3.設(shè)［a1…ai…an］A中發(fā)送動(dòng)作和接收動(dòng)作的個(gè)數(shù)為lA，則l

以上條件說明在R中ρ為扮演角色A的主體，c為ρ產(chǎn)生的隨機(jī)數(shù).可證明，P在實(shí)例化空間下的運(yùn)行完全等價(jià)于在索狀空間下的運(yùn)行，并且（ρ，c）標(biāo)識(shí)的局部運(yùn)行等價(jià)于索狀空間的R|A，lA為（ρ，c）標(biāo)識(shí)的局部運(yùn)行會(huì)話的長(zhǎng)度.該證明方法與文獻(xiàn)［10］中從串空間模型到智能體系統(tǒng)的轉(zhuǎn)換類似，這里不再詳述.

1.Σ屬于索狀空間C的消息交換對(duì)應(yīng)的CME模型集合；

2.L是與協(xié)議P相關(guān)聯(lián)的標(biāo)識(shí)消息集（隨機(jī)數(shù)集）；

3.F為協(xié)議P的所有角色在Σ下的實(shí)例化函數(shù)集合；

定理4是在之前幾部分的理論基礎(chǔ)上提出的.該定理說明，索狀空間能夠完全轉(zhuǎn)換成實(shí)例化空間的集合.

3.4 語(yǔ)義模型的轉(zhuǎn)換

協(xié)議組合邏輯PCL以P的某次運(yùn)行R為語(yǔ)義模型：設(shè)尷為PCL中的公式，P，R|=尷表示尷在P的運(yùn)行R中成立；實(shí)例化空間邏輯ISL以實(shí)例化空間Ω為語(yǔ)義模型：設(shè)φ為實(shí)例化空間邏輯中的公式，Ω|=φ表示φ在Ω模型中成立.

ISL公式的語(yǔ)義涉及到具體時(shí)間，我們用Ω，t|=φ表示在t時(shí)刻，φ在Ω模型中成立，其中t∈時(shí)間集合.

證明：Ω是實(shí)例化空間.根據(jù)實(shí)例化函數(shù)的假設(shè)，ρ∈Ag產(chǎn)生的隨機(jī)數(shù)c最多只在協(xié)議的一次運(yùn)行中使用.給定P的運(yùn)行R，c是否在R中使用是可判的，所以F的子集必定是關(guān)于運(yùn)行R的實(shí)例化函數(shù)集，因此每個(gè)都是與（P，R）對(duì)應(yīng)的實(shí)例化空間.為解釋PCL中的公式，需要指明實(shí)例化空間中對(duì)應(yīng)公式的成立時(shí)間，所以引入時(shí)間點(diǎn)t.因此，{（，t）}是與（P，R）對(duì)應(yīng)的實(shí)例化空間語(yǔ)義模型集合.

3.5 PCL公理系統(tǒng)在實(shí)例化空間中的語(yǔ)義解釋

3.5.1 主要公式的語(yǔ)義解釋

為描述公式的語(yǔ)義，PCL定義了兩個(gè)謂詞：EVENT（R，ρ，action）表示動(dòng)作action在運(yùn)行R中發(fā)生，由ρ執(zhí)行；LAST（R，ρ，action）表示在運(yùn)行R的最后階段，有EVENT（R，ρ，action）成立.PCL的主要公式分為三類：

1.動(dòng)作公式：New（ρ，m）、Send（ρ，m）、Receive（ρ，m）、Encrypt（ρ，m）、Sign（ρ，m）、Decrypt（ρ，m）和Verify（ρ，m）分別表示在協(xié)議運(yùn)行的最后階段，主體ρ進(jìn)行了新建、發(fā)送、接收、加密、簽名、解密、驗(yàn)證動(dòng)作，相關(guān)項(xiàng)為m.

2.普通公式：Has（ρ，m）表示主體ρ在運(yùn)行中擁有項(xiàng)m；Fresh（ρ，m）表達(dá)了新鮮性；Honest（ρ）表示在協(xié)議運(yùn)行中ρ是誠(chéng)實(shí)的；Contains（m，）表示為m的子項(xiàng)；Start（ρ）表示ρ還未執(zhí)行任何動(dòng)作；Source（m，ρ，，k）表示ρ之外的主體只能從中直接或間接地獲得m，即ρ是項(xiàng)m的“源”；ψ∧尷、┐尷和堝x.尷與普通一階邏輯中的對(duì)應(yīng)公式含義相同；時(shí)態(tài)算子（◇尷和扌尷與線性時(shí)態(tài)邏輯LTL（Linear Temporal Logic）［11］中的時(shí)態(tài)算子含義相同，在運(yùn)行的一系列狀態(tài)中，前者表示尷在過去的某個(gè)狀態(tài)下成立，后者表示尷在過去的所有狀態(tài)下都成立.

3.模態(tài)公式：模態(tài)公式ψ［action］ρ尷表示在公式ψ成立且主體ρ執(zhí)行了動(dòng)作action的情況下，有尷成立.

這些公式在（P，R）模型下的形式化語(yǔ)義詳見文獻(xiàn)［4-5］，這里給出這些形式化語(yǔ)義在，t）模型中的語(yǔ)義對(duì)應(yīng)關(guān)系（由于項(xiàng)實(shí)質(zhì)上就是消息，在下文的描述中不再專門區(qū)分“項(xiàng)”和“消息”這兩個(gè)概念）：

如果LAST（R，ρ，（vm））成立，則有P，R|= New（ρ，m），即主體ρ在R中新建了消息m，這與nonce（ρ，m）語(yǔ)義一致.根據(jù)實(shí)例化空間的假設(shè)，隨機(jī)數(shù)在0時(shí)刻即生成，因此這里有t≥0.

如果LAST（R，ρ，）成立，則有P，R|= Send（ρ，m），即主體ρ在R中發(fā)送了消息m，這與sent（ρ，m）語(yǔ)義一致.

如果LAST（R，ρ，（m））成立，則有P，R|= Receive（ρ，m），即主體ρ在R中接收了消息m，這與recv（ρ，m）語(yǔ)義一致.

Encrypt（ρ，{m}k）和encr（ρ，{m}k）都表示主體ρ構(gòu)造了加密消息.具體分析，若LAST（R，ρ，{m}k）成立，則ρ構(gòu)造了加密消息，因此P，R|=Encrypt（ρ，{m}k）.在Ω'模型下，若ρ構(gòu)造了加密消息{m}k表示{m}k∈Encr（ρ，t），因此有{Ω'，t}|=encr（ρ，{m}k）成立.反之亦然.

Sign（ρ，{m}k）和sign（ρ，{m}k）都表示主體ρ構(gòu)造了簽名消息{m}k.兩者的語(yǔ)義關(guān)系與公式Encrypt和encr的關(guān)系類似.

Decrypt（ρ，{m}k）和decr（ρ，{m}k）都表示主體ρ能夠?qū)m}k消息用k進(jìn)行解密.具體分析，若LAST（R，ρ，（{m}k/{m}k））成立，則ρ能對(duì){m}k進(jìn)行解密匹配，因此P，R|=Decrypt（ρ，{m}k）.在模型下，若ρ擁有逆鑰k，才可對(duì){m}k解密，即若{m}k∈Poss（ρ，t）∧k∈Poss（ρ，t）成立，才有{，t}|=decr（ρ，{m}k）成立.兩者語(yǔ)義相同.要注意的是，當(dāng)Decrypt和decr公式中的消息不為{m}k形式時(shí)，兩個(gè)公式都為假.

Verify（ρ，{m}k）和veri（ρ，{m}k）都表示主體ρ能夠用密鑰k驗(yàn)證簽名{m}k.兩者的語(yǔ)義關(guān)系與公式Decrypt和decr的關(guān)系類似.當(dāng)Verify和veri公式中的消息不為{m}k形式時(shí)，兩個(gè)公式都為假.

Has（ρ，m）和poss（ρ，m）都表示主體ρ擁有消息m.具體分析，Has成立的幾種情況都可對(duì)應(yīng)于poss成立的情況：

（3）若P，R|=Has（ρ，m1）∧…∧Has（ρ，mn）∧（m=［m1，…，mn］），或有P，R|=Has（ρ，∧Has（ρ，k）∧（m={}k），則P，R|=Has（ρ，m）.即m可由主體ρ對(duì)已知的消息進(jìn)行加密或聯(lián)合得到，并且該嵌套過程從情況（1）開始.對(duì)應(yīng)到模型下，與情況（2）類似，有m∈cl（Init（ρ）∪Recvs（ρ，t）），即{，t}|=poss（ρ，m）成立.反之亦然.

Fresh（ρ，m）表示若ρ曾新建消息m，或曾新建且m=g（），且ρ未發(fā)送包含m的消息，則m為新鮮的.因此在Ω'模型下有以上對(duì)應(yīng).我們沒有使用ISL的新鮮性公式fresh直接對(duì)應(yīng)PCL下的新鮮性，是由于CME模型的Fresh函數(shù)包含了更多的情況（如當(dāng)消息m是新鮮的，則包含m的加密消息也是新鮮的），因此fresh（ρ，c，m）比Fresh（ρ，m）描述了更一般的情況.

10.對(duì)于Honest（ρ），如果主體ρ是誠(chéng)實(shí)主體，則有P，R|=Honest（ρ）.在模型中，沒有將該謂詞對(duì)應(yīng)成公式，而是作為假設(shè)，假定Ag集合中都為誠(chéng)實(shí)主體.

δ尷表示通過置換δ替換公式尷中的所有自由變量得到的新公式.由于實(shí)例化空間邏輯中的公式不考慮自由變量，也沒有置換的概念，因此δ尷在P，R中為真相當(dāng)于尷在模型中為真.

18.由于實(shí)例化空間邏輯ISL的公理系統(tǒng)基于一階邏輯，因此PCL的合取公式、非公式和存在公式語(yǔ)義與ISL中相同.

3.5.2 主要定理的語(yǔ)義證明

下面證明PCL的定理在實(shí)例化空間解釋下也是成立的.定義：

首先給出PCL中與主體動(dòng)作相關(guān)的定理（表1）的語(yǔ)義證明：

表2 PCL主要基本定理

定理ORIG表示當(dāng)ρ產(chǎn)生隨機(jī)數(shù)m時(shí)，ρ也擁有消息m.

定理REC表示當(dāng)ρ收到消息m時(shí)，ρ即擁有m.

定理ENC表示當(dāng)ρ擁有消息m和密鑰k時(shí)，ρ也擁有加密消息{m}k.

定理PROJ表示當(dāng)ρ擁有組合消息時(shí)，ρ也擁有其中的子消息.

定理DEC1表示當(dāng)ρ擁有加密消息{m}k和密鑰k時(shí)，ρ也擁有原來的消息m.因?yàn)榍疤釛l件說明ρ有能力構(gòu)造{m}k，所以ρ自然也知道未加密之前的消息.

定理DEC2表示若ρ能夠?qū)m}k解密，則必定知道m(xù)，因?yàn)閙是對(duì){m}k解密的結(jié)果.

定理SEC說明誠(chéng)實(shí)主體不會(huì)竊取其它主體的私鑰，因此只能對(duì)用自身公鑰加密的消息解密.

10.定理VER在實(shí)例化空間中成立.因?yàn)閠

定理N1表示每個(gè)隨機(jī)數(shù)只能由一個(gè)主體產(chǎn)生.在實(shí)例化空間中，這個(gè)定理的成立由CME模型的假設(shè)保證.

定理CON表示組合消息包含了其中的每個(gè)子消息.

PCL中還有一系列與DH密鑰假設(shè)相關(guān)的定理（表3），對(duì)于其中描述的性質(zhì)，實(shí)例化空間中也有對(duì)應(yīng)的解釋：

1.定理DH 1在實(shí)例化空間中成立.因?yàn)槿鬋ompute（ρ，）成立，根據(jù)該公式的語(yǔ)義，可得在實(shí)例化空間中有∈Computes（ρ，t）.又根據(jù)Poss函數(shù)的定義，可得∈Poss（ρ，t），即|=poss（ρ，）.

表3 PCL中DH假設(shè)相關(guān)定理

PCL中存在時(shí)態(tài)算子，因此還提出了一系列與時(shí)序相關(guān)的定理來描述主體動(dòng)作間的順序關(guān)系.而實(shí)例化空間模型描述了主體行為的具體執(zhí)行時(shí)間，因此，我們可以利用語(yǔ)義模型集合{（，t）}中時(shí)間t的大小關(guān)系給出與這些定理相應(yīng)的描述.這部分定理與普通線性時(shí)序邏輯中的定理類似，這里不再詳述.

3.5.3 推導(dǎo)規(guī)則的對(duì)應(yīng)

PCL的推導(dǎo)規(guī)則分為三種：

1.通用規(guī)則

與∧，圯等一階邏輯連接符相關(guān)的推導(dǎo)規(guī)則.如：

等.實(shí)例化空間邏輯ISL基于一階邏輯，因此也有對(duì)應(yīng)的通用規(guī)則.

2.順序規(guī)則

提供了順序合并動(dòng)作的規(guī)則：

在ISL中，此規(guī)則等價(jià)于（┐ψ∨覫）∧（┐ψ∨φ）圯（┐ψ∨φ），這可由一階邏輯的性質(zhì)推出.

3.保持規(guī)則

描述了主體執(zhí)行某些動(dòng)作后，謂詞的真值是否能保持的規(guī)則.具體分析，New（ρ，m）、Send（ρ，m）、Receive（ρ，m）、Decrypt（ρ，m）、Verify（ρ，m）、Has（ρ，m）等公式一旦為真，則無論主體再執(zhí)行什么動(dòng)作，這些謂詞仍然為真；而對(duì)于Source（m，ρ，k）和Fresh（ρ，m），接收、新建、匹配動(dòng)作能夠保持其真值，但對(duì)發(fā)送動(dòng)作有限制.以Source（m，ρ，，k）為例，若ρ執(zhí)行<>，則要求m芫，Source才能保持真值.因?yàn)槿鬽哿，ρ執(zhí)行<>后將泄漏m，m不再唯一由{}k解密得到，Source（m，ρ，，k）的值將為假.而對(duì)于Fresh（ρ，m），只要主體ρ發(fā)送了包含m的消息，則Fresh（ρ，m）的值就變?yōu)榧?由前面定理的語(yǔ)義轉(zhuǎn)換，不難推出ISL也有類似的保持規(guī)則.

4 PCL與ISL關(guān)系的進(jìn)一步討論

我們已經(jīng)證明，PCL的語(yǔ)義能夠完全被實(shí)例化空間模型解釋.但是，ISL的描述能力強(qiáng)于PCL，因此現(xiàn)有的PCL不能完全表示ISL.具體體現(xiàn)在以下幾個(gè)方面：

首先，PCL主要用來驗(yàn)證公鑰加密體制下協(xié)議的認(rèn)證性和秘密性，也成功地驗(yàn)證了許多應(yīng)用協(xié)議.例如，在文獻(xiàn)［4］中，該邏輯被用于模塊化地驗(yàn)證一組密鑰交換協(xié)議集合；在文獻(xiàn)［12］中，Kerberos V5協(xié)議通過PCL得到了驗(yàn)證；在文獻(xiàn)［13-15］中，PCL被用于驗(yàn)證無線網(wǎng)絡(luò)與移動(dòng)網(wǎng)絡(luò)中的安全協(xié)議；文獻(xiàn)［16］著重分析了PCL的組合證明方法.但是，PCL在對(duì)稱密鑰體制下只對(duì)DH密鑰進(jìn)行了描述，只有對(duì)PCL作適當(dāng)擴(kuò)充，該邏輯才能夠完整地驗(yàn)證共享密鑰加密體制下的協(xié)議.而ISL可以靈活地在公鑰、私鑰、共享密鑰（包括動(dòng)態(tài)生成的會(huì)話密鑰，如DH密鑰等）和hash密鑰等加密系統(tǒng)中推導(dǎo)協(xié)議性質(zhì)，其自動(dòng)化工具SPV已經(jīng)被成功地應(yīng)用到Kerberos協(xié)議、SET協(xié)議等工業(yè)級(jí)協(xié)議的驗(yàn)證上［1，6-7］.

其次，ISL的定理比PCL中的定理更具有一般性.例如，根據(jù)PCL中Source謂詞的定義，如果一個(gè)加密隨機(jī)數(shù)的產(chǎn)生者發(fā)送了兩個(gè)以上的包含該隨機(jī)數(shù)的消息，PCL將不能推導(dǎo)出該隨機(jī)數(shù)的來源.而實(shí)例化空間邏輯的（1，0）-Secrecy定理則沒有這種限制：假設(shè)主體ρ產(chǎn)生了一個(gè)隨機(jī)數(shù)c，并分別用主體ρ1和ρ2的公鑰k1和k2進(jìn)行加密，發(fā)送{c}k1和{c}k2，那么當(dāng)ρ收到隨機(jī)數(shù)c時(shí)，由（1，0）-Secrecy定理可以推出said（ρ1，c）∨said（ρ2，c）（ρ1對(duì){c}k1解了密，或ρ1對(duì){c}k2解了密）.另外，PCL只支持一對(duì)一的消息交換，而ISL的（n，1）-Secrecy定理能夠描述多個(gè)主體對(duì)一個(gè)主體的消息交換.

第三，PCL只描述了主體的誠(chéng)實(shí)性，不能表達(dá)實(shí)例化空間中的主體行為假設(shè)集譓.

5 相關(guān)研究工作

索狀空間模型是在串空間模型［17］的基礎(chǔ)上發(fā)展改進(jìn)而來的，因此PCL驗(yàn)證法在分析安全協(xié)議時(shí)與串空間模型驗(yàn)證法比較相似［18］，只是前者還加入了邏輯推理的內(nèi)容，其公理和推導(dǎo)規(guī)則又與協(xié)議的每一步執(zhí)行動(dòng)作相關(guān)；而ISL驗(yàn)證法是一個(gè)知識(shí)推理的多智能體系統(tǒng).Halpern和Pucella比較完整地對(duì)串空間模型與多智能體系統(tǒng)進(jìn)行了比較［10］，并嘗試將兩者互相轉(zhuǎn)換，但文中討論的情況比較簡(jiǎn)單和抽象，對(duì)于具體、復(fù)雜的安全協(xié)議驗(yàn)證邏輯之間關(guān)系的研究工作，目前還比較缺乏.本文將這兩個(gè)復(fù)雜的具體邏輯進(jìn)行具體比較和語(yǔ)義轉(zhuǎn)換，得出的結(jié)果具有一定的實(shí)用性.

Cremers等給出了普通安全協(xié)議的一個(gè)通用的形式化的操作語(yǔ)義［19］.在該操作語(yǔ)義下，能使用模型檢測(cè)工具檢驗(yàn)安全協(xié)議的秘密性，卻不能檢驗(yàn)安全協(xié)議的認(rèn)證性［20］.如果找出實(shí)例化空間語(yǔ)義模型與安全協(xié)議通用操作語(yǔ)義的對(duì)應(yīng)關(guān)系，并實(shí)現(xiàn)安全協(xié)議的操作語(yǔ)義在實(shí)例化空間下的完全表示，將從理論上更進(jìn)一步說明實(shí)例化空間語(yǔ)義模型具有足夠強(qiáng)的表示能力描述安全協(xié)議.另一方面，通過語(yǔ)義模型的轉(zhuǎn)換，將使原形式下的安全協(xié)議能夠直接利用SPV進(jìn)行認(rèn)證性等重要安全性質(zhì)的自動(dòng)驗(yàn)證.

結(jié)束語(yǔ)實(shí)例化空間邏輯ISL與協(xié)議組合邏輯PCL是兩種有效的安全協(xié)議形式化驗(yàn)證方法.為了在理論上衡量與評(píng)價(jià)ISL的語(yǔ)義表達(dá)能力，給出了PCL在ISL語(yǔ)義模型下的語(yǔ)義解釋，并且說明現(xiàn)有的PCL不能夠完全表示ISL的語(yǔ)義，這種單向的語(yǔ)義對(duì)應(yīng)關(guān)系證明ISL的公理集比現(xiàn)有的一些安全協(xié)議驗(yàn)證邏輯刻畫了更一般的情形，具有較強(qiáng)的語(yǔ)義表達(dá)能力.把PCL的語(yǔ)義轉(zhuǎn)化到ISL語(yǔ)義模型下，還使得用PCL理論驗(yàn)證的協(xié)議能夠利用ISL的自動(dòng)化驗(yàn)證工具SPV進(jìn)行自動(dòng)驗(yàn)證.另外，新語(yǔ)義模型下的PCL也將更容易擴(kuò)展.

下一步的工作將著眼于以下幾個(gè)方面：首先，經(jīng)過語(yǔ)義轉(zhuǎn)換后，PCL下的協(xié)議可以使用SPV進(jìn)行自動(dòng)驗(yàn)證，但是語(yǔ)義轉(zhuǎn)換的過程目前只能用手工實(shí)現(xiàn)，為提高分析效率，可嘗試開發(fā)相應(yīng)的自動(dòng)化語(yǔ)義轉(zhuǎn)換工具.其次，將對(duì)ISL與其它相關(guān)工作進(jìn)行比較，剖析它們之間的聯(lián)系和優(yōu)缺點(diǎn)，從而進(jìn)一步擴(kuò)充ISL，使其具有更強(qiáng)的語(yǔ)義表達(dá)能力.另外，改進(jìn)PCL，如消除PCL中公式對(duì)主體動(dòng)作的依賴等，使其能夠完全表示ISL的語(yǔ)義，達(dá)到兩種邏輯的一一對(duì)應(yīng)，也是未來的工作方向.

［1］蘇開樂，岳偉亞，陳清亮，等.實(shí)例化空間:一種新的安全協(xié)議驗(yàn)證邏輯的語(yǔ)義模型［J］.計(jì)算機(jī)學(xué)報(bào)，2006，29（9）:1657-1665.

［2］Xiao Yinyin,Su Kaile.The DH exponentiation extension in a verification logic of local sessions［C］//CSAE 2012,Zhangjiajie:IEEE CPS,2012:499-503.

［3］薛銳,馮登國(guó).安全協(xié)議的形式化分析技術(shù)與方法［J］.計(jì)算機(jī)學(xué)報(bào),2006,29（1）:1-20.

［4］A.Datta,A.Derek,J.C.Mitchell,el al.A derivation system and compositional logic for security protocols［J］. Journal of Computer Security,2005,13:423-482.

［5］A.Datta,A.Derek,J.C.Mitchell,el al.Protocol composition logic（PCL）［J］.Electronic Notes in Theoretical Computer Science,2007,172:311-358.

［6］肖茵茵,蘇開樂,馬震遠(yuǎn),等.實(shí)例化空間邏輯下的SET支付協(xié)議驗(yàn)證及改進(jìn)［J］.華中科技大學(xué)學(xué)報(bào), 2013,41（7）:97-102.

［7］肖茵茵,蘇開樂,岳偉亞,等.SET證書申請(qǐng)協(xié)議在SPV下的自動(dòng)化驗(yàn)證及改進(jìn)［J］.計(jì)算機(jī)學(xué)報(bào), 2008,31（6）:1035-1045.

［8］Burrows M,Abadi M,Needham R.A logic of authentication［J］.ACM Transactions on Computer Systems, 1990,8（1）:18-36.

［9］M.Abadi,M.R.Tuttle.A semantics for a logic of authentication［C］//Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing,1991:201-216.

［10］Joseph Y.Halpern,Riccardo Pucella.On the relationship between strand spaces and multi-agent systems［J］.ACM Transactions on Information and System Security（TISSEC）,2003,6（1）:43-70.

［11］Zohar Manna,Amir Pnueli.The Temporal Logic of Reactive and Concurrent Systems:Specification［M］. Springer-Verlag,1992.

［12］A.Roy,A.Datta,A.Derek,et al.Secrecy analysis in protocol composition logic［C］//Proceedings of 11th Asian Computing Science Conference,Tokyo,Japan: Springer,2006,4435:197-213.

［13］郭顯,馮濤,袁占亭.協(xié)議組合邏輯安全的Ad Hoc網(wǎng)絡(luò)路由協(xié)議安全驗(yàn)證方法［J］.小型微型計(jì)算機(jī)系統(tǒng),2013,34（12）:2794-2799.

［14］王麗麗,馮濤,馬建峰.協(xié)議組合邏輯安全的4G無線網(wǎng)絡(luò)接入認(rèn)證方案［J］.通信學(xué)報(bào),2012,33（4）: 77-84.

［15］C.He,M.Sundararajan,A.Datta,et al.A modularcorrectness proof of IEEE 802.11i and TLS［C］//ACM CCS 2005:2-15.

［16］魯來鳳.安全協(xié)議形式化分析理論與應(yīng)用研究［D］.西安:西安電子科技大學(xué),2012.

［17］F.J.Thayer Fabrega,J.C.Herzog,and J.D.Guttman. Strand spaces［R］.The MITRE Corporation,November, 1997.

［18］皮建勇,楊雷,劉心松,等.一種新的安全協(xié)議及其串空間模型分析［J］.計(jì)算機(jī)科學(xué),2010,37（1）:118-121.

［19］C.J.F.Cremers and S.Mauw.Operational semantics of security protocols［M］.Springer-Verlag,2011.

［20］Cremers C,Mauw S.Checking secrecy by means of partial order reduction［C］//The 4th System Analysis and Modeling Workshop.Berlin:Springer,2004:177-194.

［責(zé)任編輯：劉向紅］

Semantic Interpretation of Protocol Com positional Logic in Instantiation Space M odel

XIAO Yin-yin1，2，SU Kai-le2，3
（1.Department of Computer Science,Guangdong Polytechnic Normal University,Guangzhou 510665,China；2.Guangdong Province Key Lab for Information Security,College of Information Science&Technology, Sun Yat-Sen University,Guangzhou 510275,China；3.College of Mathematics,Physics and Information Engineering,Zhejiang Normal University,Jinhua 321004,China）

The verification of protocols is an undecidable problem.In order to evaluate the semantics expressive ability of Instantiation Space Logic（ISL）theoretically,another practical protocol logic called Protocol Compositional Logic（PCL）was chosen,and the relationship between ISL and PCL was analyzed.Based on the relationship,the PCL semantic model called Cord Space was changed into the ISL semantic model,and themain formulas,axioms and inference rules of PCL were interpreted in Instantiation Space.The research shown that the Instantiation Space could express the semantics of PCL completely,and the expressive ability of ISL was stronger than that of PCL.The new interpreted PCL could be extended more easily,and those security protocols described in PCL could be verified by Security Protocol Verifier（SPV)of ISL automatically.

Security protocols analyzing；Instantiation space；Protocol compositional logic；Cord space；Semantic interpretation

TP 301.2

B

1672-402X（2016）02-0008-12

10.13408/j.cnki.gjsxb.2016.02.003

2015-11-11

國(guó)家自然科學(xué)基金（60903054，61379019），國(guó)家“973”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃資助項(xiàng)目(2010CB328103)，中國(guó)博士后科學(xué)基金面上項(xiàng)目（2013M540704），廣東高校優(yōu)秀青年創(chuàng)新人才培育項(xiàng)目(LYM11085，LYM11084)資助.

肖茵茵（1983－），女，廣東梅州人，博士，廣東技術(shù)師范學(xué)院講師，研究方向：電子商務(wù)、網(wǎng)絡(luò)安全、安全協(xié)議驗(yàn)證、形式化方法.

蘇開樂（1964－），男，湖南長(zhǎng)沙人，博導(dǎo)，暨南大學(xué)教授，研究方向：數(shù)理邏輯、形式化方法.