運(yùn)用SPIN 對(duì)開(kāi)放授權(quán)協(xié)議OAuth 2.0的分析與驗(yàn)證＊

程道雷，肖美華，劉欣倩，梅映天，李 偉

（華東交通大學(xué)軟件學(xué)院，江西 南昌330013）

1 引言

OAuth（Open Authorization）［1］作為一種授權(quán)標(biāo)準(zhǔn)，用戶無(wú)需將用戶名和密碼等信息提交給第三方應(yīng)用，便能在第三方應(yīng)用中獲取其存儲(chǔ)于其它平臺(tái)的私密資源，該標(biāo)準(zhǔn)主要用于解決賬號(hào)關(guān)聯(lián)與資源共享問(wèn)題。OAuth 2.0是OAuth協(xié)議的最新版本，不兼容OAuth 1.0，但降低了OAuth協(xié)議的編碼復(fù)雜度，且為各平臺(tái)的相關(guān)應(yīng)用提供了對(duì)應(yīng)的認(rèn)證方式。近年來(lái)，OAuth 2.0協(xié)議的安全性漏洞引發(fā)了許多互聯(lián)網(wǎng)安全問(wèn)題，包括CSDN、facebook、亞馬遜、新浪微博在內(nèi)的眾多著名網(wǎng)站遭受黑客攻擊。因此，OAuth 2.0協(xié)議形式化分析與驗(yàn)證具有重要社會(huì)價(jià)值。

Pai S等［2］運(yùn)用Alloy框架對(duì)OAuth 2.0進(jìn)行形式化分析；Sun San－Tsai［3］通過(guò)利用基于OAuth 2.0的單點(diǎn)登錄系統(tǒng)的實(shí)例表明OAuth 2.0雖然內(nèi)容簡(jiǎn)單，但不安全；陳偉等［4］運(yùn)用“數(shù)字簽名技術(shù)”對(duì)OAuth 2.0進(jìn)行改進(jìn)，并基于Blanchet演算對(duì)其進(jìn)行安全性分析；王煥孝等［5］運(yùn)用協(xié)議分析工具SATMC，得出OAuth 2.0協(xié)議在失去https通道保護(hù)下的危險(xiǎn)狀態(tài)。由于OAuth 2.0協(xié)議當(dāng)前依賴https 通道傳輸相關(guān)數(shù)據(jù)，而https 要運(yùn)行SSL（Secure Sockets Layer）對(duì)傳輸數(shù)據(jù)加密，降低了https傳輸效率。根據(jù)相關(guān)調(diào)查研究，在北上廣深以外的中國(guó)廣大城市，有20%～25% 的用戶都會(huì)遇到https連接困難，排查發(fā)現(xiàn)問(wèn)題和接入點(diǎn)無(wú)關(guān)，信號(hào)和網(wǎng)絡(luò)不穩(wěn)定導(dǎo)致https 請(qǐng)求很難完成，導(dǎo)致一旦遭遇ARP（Address Resolution Protocol）攻擊或中間人攻擊，用戶信息將遭竊取或破壞。本文提出使OAuth 2.0脫離https通道，通過(guò)“http＋消息加密”的方式傳輸數(shù)據(jù)，并將公鑰密鑰體系運(yùn)用到該協(xié)議上，使用模型檢測(cè)技術(shù)對(duì)協(xié)議進(jìn)行安全性驗(yàn)證。

形式化方法主要包括模型檢測(cè)（Model Checking）［6］與 定 理 證 明［7］兩 個(gè) 分 支。SPIN（Simple Promela INterpreter）［8，9］是 一 種 著 名 的 協(xié) 議 模 型檢測(cè)驗(yàn) 證 工 具。Maggi P 等［10］以Ndddam－Schroeder協(xié)議為實(shí)例，基于Dolev－Yao攻擊模型［11］的思想，提出一種用于安全協(xié)議模型檢測(cè)的建模方法。本文對(duì)該方法進(jìn)行擴(kuò)展，運(yùn)用到包含多主體的授權(quán)協(xié)議的模型檢測(cè)上。

由于OAuth 2.0 是一個(gè)嶄新的授權(quán)協(xié)議，可供參考的運(yùn)用形式化方法對(duì)該協(xié)議安全性驗(yàn)證研究成果仍然不足，本文探索使用模型檢測(cè)技術(shù)對(duì)OAuth 2.0協(xié)議進(jìn)行形式化分析與驗(yàn)證。首先，將OAuth 2.0協(xié)議進(jìn)行簡(jiǎn)化，并用形式化方法對(duì)其進(jìn)行描述，再運(yùn)用公鑰加密體系對(duì)協(xié)議進(jìn)行加密，在對(duì)OAuth 2.0協(xié)議進(jìn)行建模后，驗(yàn)證該協(xié)議是否能安全用在消息傳輸中，模型檢測(cè)實(shí)驗(yàn)發(fā)現(xiàn)了中間人攻擊序列圖，因此得出公鑰加密體系不能夠保證OAuth 2.0協(xié)議安全的方法。

本文結(jié)構(gòu)安排如下：第2 節(jié)對(duì)OAuth 2.0 協(xié)議進(jìn)行簡(jiǎn)化及形式化表示，并運(yùn)用公鑰密碼體系對(duì)協(xié)議加密；第3節(jié)闡述了OAuth 2.0 協(xié)議建模過(guò)程；第4節(jié)運(yùn)用SPIN 對(duì)OAuth 2.0協(xié)議進(jìn)行驗(yàn)證與分析；第5節(jié)為結(jié)束語(yǔ)。

2 OAuth 2.0協(xié)議及形式化表示

OAuth是一種第三方授權(quán)協(xié)議。首先，客戶端發(fā)送Authorization Request（授權(quán)申請(qǐng)），向Resource Owner（資源擁有者）申請(qǐng)Access Grant（訪問(wèn)授權(quán)）；然后，使用Access Grant和Client Credentials（身份證書(shū)）與Authorization Server（授權(quán)服務(wù)器）交換Access Token（訪問(wèn)令牌，包含持續(xù)時(shí)間、作用范圍等信息），最后客戶端提交Access Token至Resource Owner（資源擁有者）獲取受保護(hù)資源。具體過(guò)程如圖1所示。

Figure 1 Flow of the abstract protocol圖1 抽象協(xié)議流程

根據(jù)圖1所示的協(xié)議流程，將OAuth 2.0 協(xié)議進(jìn)行形式化表示，獲得如下協(xié)議：

（1）Client→Resource Owner：Authorization Request；

（2）Resource Owner→Client：Access Grant；

（3）Client→Authorization Server：Access Grant，Client Credentials；

（4）Authorization Server→Client：Access Token；

（5）Client→Resource Server：Access Token；

（6）Resource Server→Client：Protected Resource。

如果將以上協(xié)議中未加密的消息直接通過(guò)http通道傳輸數(shù)據(jù)，所有的信息都將被攻擊者輕而易舉截獲。因此，將OAuth 2.0 協(xié)議簡(jiǎn)化，并用公鑰加密體系對(duì)消息進(jìn)行加密，得到如下OAuth 2.0協(xié)議：

（1）C→RO：｛A＿r｝PKRO；

（2）RO→C：｛A＿g｝PKC；

（3）C→AS：｛A＿g，C＿c｝PKAS；

（4）AS→C：｛A＿t｝PKC；

（5）C→RS：｛A＿t｝PKRS；

（6）RS→C：｛P＿r｝PKC。

其中，PKC表示以C的公鑰加密，任意經(jīng)C的公鑰加密的消息，只有C才能通過(guò)其私鑰解開(kāi)，其它主體類似。本文將運(yùn)用模型檢測(cè)技術(shù)對(duì)以上協(xié)議進(jìn)行驗(yàn)證分析。

3 OAuth 2.0 協(xié)議建模

將OAuth 2.0 協(xié)議建模分為誠(chéng)實(shí)主體建模和攻擊者建模兩個(gè)部分，其中，攻擊者建模以Dolev－Yao攻擊者模型為指導(dǎo)理論。

3.1 誠(chéng)實(shí)主體建模

OAuth 2.0 協(xié)議的誠(chéng)實(shí)主體包括Client、Resource Owner、Authorization Server 和Resource Server。結(jié)合Promela語(yǔ)言性質(zhì)，我們分別為四個(gè)誠(chéng)實(shí)主體定義各自的進(jìn)程，依次命名為proctypePC（）、proctypePRO（）、proctypePAS（）和proctypePRS（）。由于誠(chéng)實(shí)主體進(jìn)程的定義方法非常類似，本文將以proctypePC（）的定義過(guò)程為例進(jìn)行闡述。

本文所研究的內(nèi)容為檢測(cè)協(xié)議本身存在的漏洞，因此首先需要對(duì)模型做出如下幾點(diǎn)假設(shè)：

（1）公鑰加密算法本身沒(méi)有漏洞；

（2）只有對(duì)應(yīng)的密鑰才能解密加密消息；

（3）攻擊者可以是任何主體。

由于攻擊者建模遵循Dolev－Yao攻擊模型，因此誠(chéng)實(shí)主體發(fā)送的所有消息都將被攻擊者截獲，而誠(chéng)實(shí)主體所接收的消息，也全部由攻擊者根據(jù)已有的知識(shí)組合生成或者直接轉(zhuǎn)發(fā)截獲的消息。依據(jù)該思想，建模過(guò)程需要借助Promela語(yǔ)言中的通道（chan）這一數(shù)據(jù)結(jié)構(gòu)。將協(xié)議中傳輸?shù)南⒏鶕?jù)數(shù)據(jù)項(xiàng)的數(shù)目進(jìn)行分類，同一類的消息使用同一個(gè)通道進(jìn)行傳輸，因此，OAuth 2.0數(shù)據(jù)傳輸模擬需要兩個(gè)參數(shù)不同的通道，將其進(jìn)行如下定義：

chanca＝［0］of｛mtype，mtype，mtype｝

chancb＝［0］of ｛mtype，mtype，mtype，mtype｝

其中，協(xié)議中的消息（1）、（2）、（4）、（5）、（6）通過(guò)通道ca傳輸，消息（3）通過(guò)通道cb傳輸。值得注意的是ca和cb所定義的單位元素個(gè)數(shù)都比所需表示的消息元素多一項(xiàng)，這是因?yàn)橥ǖ乐行枰A(yù)留一個(gè)元素應(yīng)對(duì)會(huì)話過(guò)程中的優(yōu)化需要。具體原因如下：由于本文所要構(gòu)建的是一個(gè)并發(fā)系統(tǒng)，因此各進(jìn)程之間的交叉運(yùn)行所產(chǎn)生的狀態(tài)遷移量將非常龐大，甚至足以導(dǎo)致?tīng)顟B(tài)爆炸［12～15］，為了減少狀態(tài)遷移的數(shù)量，在建模過(guò)程中，以ca為例，對(duì)通道作如下定義：發(fā)送語(yǔ)句ca！x1，x2，x3 中，x1 為消息接收者，x2是知識(shí)項(xiàng)，x3 是對(duì)x2 進(jìn)行加密的公鑰。接收語(yǔ)句ca？eval（x1），x2，eval（x3）中，eval函數(shù)被用作判斷知識(shí)項(xiàng)是否與預(yù)期一致，從左到右依次判斷，如果某處不一致，直接拒絕接收該消息。但是，攻擊者需要截獲所有誠(chéng)實(shí)主體發(fā)送的消息，因此不需要通過(guò)eval來(lái)判斷消息發(fā)送方，可直接定義為ca？＿，x1，x2。如此，可以減少大量無(wú)效消息。對(duì)Client的建模，具體如以下proctypePC（）的詳細(xì)代碼所示：

在PC進(jìn)程中，self表 示 消 息 發(fā) 起 者，party1、party2、party3為消息接收者，g1和g2為泛型變量，用作表示主體C接收到的消息中的未知數(shù)據(jù)項(xiàng)。atomic為Promela語(yǔ)言中用來(lái)定義原子序列的語(yǔ)法規(guī)則，旨在減少進(jìn)程交叉運(yùn)行的次數(shù)，達(dá)到優(yōu)化系統(tǒng)的目的。init＿start＿C＿RO、init＿commit＿C＿RO、init＿start＿C＿AS、init＿commit＿C＿AS和init＿start＿C＿RS為模型程序中定義的宏，被用來(lái)更新記錄原子謂詞的變量的值，這些原子謂詞被用來(lái)表示協(xié)議性質(zhì)。如果主體C發(fā)起對(duì)主體RO的協(xié)議會(huì)話，表示主體C參與了主體RO運(yùn)行的協(xié)議。如果主體C完成了與主體RO的會(huì)話，則表明主體C提交了與主體RO的會(huì)話。根據(jù)以上原理，模型的每一條性質(zhì)都需要用一個(gè)全局的Promela布爾變量表示，它們將在協(xié)議運(yùn)行的特定階段為真。通過(guò)對(duì)協(xié)議的分析，定義了如下原子謂詞變量：

為了將模型中的所有性質(zhì)運(yùn)用到SPIN 工具的仿真過(guò)程中，本文將協(xié)議性質(zhì)用LTL（線性時(shí)態(tài)邏輯）［16，17］刻畫(huà)如下：

［］（（［］！commitCRO）‖（！commitCRO∪startROC））

［］（（［］！startCAS）‖（！startCAS∪commitCRO））

［］（（［］！commitCAS）‖（！commitCAS∪startASC））

［］（（［］！startCRS）‖（！startCRS∪commitCAS））

［］（（［］！commitCRS）‖（！commitCRS∪startRSC））

根據(jù)相同的規(guī)則，類似地定義主體RO的進(jìn)程PRO和主體AS的進(jìn)程PAS以及主體RS的進(jìn)程PRS。

除定義好誠(chéng)實(shí)主體進(jìn)程之外，還要對(duì)初始進(jìn)程作如下定義：

主體C作為整個(gè)協(xié)議的發(fā)起者，在協(xié)議模型中，他有可能向任意主體發(fā)起協(xié)議，如主體RO和主體HACKER。

3.2 攻擊者建模

攻擊者建模中，攻擊者知識(shí)庫(kù)創(chuàng)建最為關(guān)鍵，其主要由兩部分知識(shí)項(xiàng)構(gòu)成：第一部分為攻擊者本身的初始知識(shí)庫(kù)；另一部分知識(shí)項(xiàng)學(xué)習(xí)方法如下：攻擊者每攔截到一條新消息后，便將學(xué)到的知識(shí)添加到知識(shí)庫(kù)中。其添加方式分為兩種：如截獲的消息未經(jīng)加密，則可直接獲取其所有知識(shí)項(xiàng)并添加入庫(kù)；如截獲的消息已加密或者部分加密，則未經(jīng)加密部分或者可以解密部分，直接或者解密后添加入庫(kù)，如無(wú)法解密，將整個(gè)密文部分存入知識(shí)庫(kù)中，以備需要時(shí)提取使用。

為簡(jiǎn)化知識(shí)項(xiàng)表示，攻擊者知識(shí)項(xiàng)表示須遵循以下兩點(diǎn)原則：（1）不表示攻擊者不可能學(xué)會(huì)的知識(shí)項(xiàng)；（2）不表示誠(chéng)實(shí)主體拒絕接受的消息（通過(guò)類型檢查的方式判斷）。基于以上兩點(diǎn)，可以計(jì)算出需要表示的攻擊者知識(shí)，如圖2所示，攻擊者潛在能學(xué)會(huì)的知識(shí)和攻擊者需要學(xué)會(huì)的知識(shí)的交集為攻擊者模型需要表示的知識(shí)。

Figure 2 Schematic of the attacker acquiring the knowledge which need to be indicated圖2 攻擊者模型中需要表示的知識(shí)項(xiàng)求解示意圖

首先求解攻擊者可以學(xué)會(huì)的知識(shí)。因?yàn)楣粽呖梢詫W(xué)會(huì)的知識(shí)，都是通過(guò)截獲誠(chéng)實(shí)主體發(fā)送的消息并對(duì)其進(jìn)行相應(yīng)處理所得，故可通過(guò)對(duì)誠(chéng)實(shí)主體的發(fā)送消息語(yǔ)句進(jìn)行分析，獲得所需知識(shí)。攻擊者 初 始 知 識(shí) 庫(kù) 為 ｛C，RO，AS，RS，H，gD，R，PKH，PKRO，PKRS，PKAS，PKC｝，變量g1～g5的取值范圍為｛C，RO，AS，RS，H，gD，PKH，PKRO，PKRS，PKAS，PKC｝，因此，可獲得如表1所示的攻擊者可學(xué)會(huì)的知識(shí)。

Table 1 Knowledge elements that the intruder can acquire表1 攻擊者可學(xué)會(huì)的知識(shí)

接下來(lái)需要求解的是攻擊者需學(xué)會(huì)的知識(shí)項(xiàng)。攻擊者需要學(xué)會(huì)的知識(shí)，就是組成攻擊者發(fā)送給誠(chéng)實(shí)主體的消息的知識(shí)項(xiàng)。故可通過(guò)對(duì)誠(chéng)實(shí)主體的接收消息語(yǔ)句進(jìn)行分析，根據(jù)變量的不同取值，組合得到如表2所示的攻擊者需要學(xué)會(huì)的知識(shí)。

Table 2 Knowledge elements the intruder needs表2 攻擊者需要學(xué)會(huì)的知識(shí)項(xiàng)

由表1和表2的第2列求交集，可得到攻擊者模型中需要表示的知識(shí)項(xiàng)，具體如圖3所示。

Figure 3 Knowledge elements that need to be indicated in the attacker model圖3 攻擊者模型中需要表示的知識(shí)項(xiàng)

根據(jù)以上的研究基礎(chǔ)與理論，編寫(xiě)攻擊者模型代碼，框架如下所示：

在Windows 7 64位系統(tǒng)、Cygwin 2.510.2.2以及SPIN 5.2.0構(gòu)建的環(huán)境下進(jìn)行仿真實(shí)驗(yàn)，發(fā)現(xiàn)了如圖4所示的OAuth 2.0協(xié)議的中間人攻擊序列。

Figure 4 Attack sequence diagram圖4 攻擊序列圖

4 實(shí)驗(yàn)結(jié)果與分析

使用SPIN 工具，對(duì)上述模型進(jìn)行驗(yàn)證，獲得了如圖4所示的攻擊序列，并得到如下攻擊過(guò)程：

（1）C→HACKER： ｛A＿r｝PKHACKER；HACKER→RO：｛A＿r｝PKRO；

（2）RO→HACKER：｛A＿g｝PKC；HACKER→C：｛A＿g｝PKC；

（3）C→HACKER： ｛A＿g，C＿c｝PKAS；HACKER→AS：｛A＿g，C＿c｝PKAS；

（4）AS→HACKER：｛A＿t｝PKC；HACKER→C：｛A＿t｝PKC；

（5）C→HACKER： ｛A＿t｝PKHACKER；HACKER→RS：｛A＿t｝PKRS；

（6）RS→HACKER： ｛P＿r｝PKHACKER；HACKER→C：｛P＿r｝PKC。

協(xié)議運(yùn)行的第（6）步，資源服務(wù)器將受保護(hù)資源加密發(fā)送出來(lái)后，被攻擊者截獲后利用自己的私鑰解密，從而竊取受保護(hù)資源，而C 并不知道自己接收到的消息實(shí)際是HACKER 轉(zhuǎn)發(fā)而來(lái)的。

5 結(jié)束語(yǔ)

OAuth 2.0協(xié)議關(guān)系到用戶賬號(hào)、密碼等個(gè)人隱私信息，與人們生活息息相關(guān)。本文提出使用http通道對(duì)OAuth 2.0協(xié)議數(shù)據(jù)進(jìn)行傳輸，運(yùn)用模型檢測(cè)技術(shù)，通過(guò)Promela語(yǔ)言以及SPIN 工具對(duì)經(jīng)公鑰體系加密的OAuth 2.0協(xié)議運(yùn)行過(guò)程進(jìn)行仿真，發(fā)現(xiàn)一條中間人攻擊路徑。仿真結(jié)果表明，利用公鑰加密體系對(duì)OAuth 2.0協(xié)議加密并不安全。下一步工作將嘗試?yán)盟借€體系對(duì)OAuth 2.0進(jìn)行加密改進(jìn)，并對(duì)其安全性進(jìn)行驗(yàn)證。

［1］ Hardt D.The OAuth 2.0authorization framework（draft－ietfoatuth－v2－31）［EB/OL］.［2012－08－01］.https：//tools.ietf.org/id/draft－ieft.org/id/draft－ietf－oauth－v2－31.html.

［2］ Pai S，Sharma Y，Kumar S，et al.Formal verification of OAuth 2.0using Alloy framework［C］∥Proc of 2011International Conference on Communication Systems and Network Technologies（CSNT），2011：655－659.

［3］ Sun San－Tsai.Simple but not secure：An empirical security analysis of OAuth2.0－based single sign－on systems［D］.Vancouver：University of British Columbia，2012.

［4］ Chen Wei，Yang Yi－tong，Niu Le－yuan.Improved OAuth2.0 protocol and analysis of its security［J］.Computer Systems＆Applications，2014，23（3）：25－30.（in Chinese）

［5］ Wang Huan－xiao，Gu Chun－xiang，Zheng Yong－h(huán)ui.Formal security analysis of OAuth 2.0authorization protocol［J］.Journal of Information Engineering University，2014，15（2）：141－147.（in Chinese）

［6］ Yu Peng，Wei Ou，Han Lan－sheng，et al.Model checking network transmission intervention policies［J］.Journal of Frontiers of Computer Science and Technology，2014，8（8）：906－918.（in Chinese）

［7］ Xiao M H，Ma C L，Deng C Y，et al.A novel approach to automatic security protocol analysis based on authentication event logic［J］.Chinese Journal of Electronics，2014，23（2）：235－241.

［8］ Holzmann G J.The model checker SPIN［J］.IEEE Transactions on Software Engineering，1997，23（5）：279－295.

［9］ Hu Liang－wen，Ma Jin－jing，Sun Bo.SPIN－based verification framework for SysML activity diagram［J］.Journal of Frontiers of Computer Science and Technology，2014，8（7）：836－847.（in Chinese）

［10］ Maggi P，Sisto R.Using SPIN to verify security properties of cryptographic protocols［C］∥Proc of the 9th International SPIN Workshop Grenoble，2002：187－204.

［11］ Dolev D，Yao A C.On the security of public key protocols［J］.IEEE Transactions on Information Theory，1983，29（2）：198－208.

［12］ Hou Gang，Zhou Kuan－jiu，Yong Jia－wei，et al.Survey of state explosion problem in model checking［J］.Computer Science，2013，40（z1）：77－85.（in Chinese）

［13］ Jamal B，Mohamed El－M，Hongyang Q，et al.Communicative commitments：Model checking and complexity analysis［J］.Knowledge－Based Systems，2012，35：21－34.

［14］ Yang Yuan－yuan，Ma Wen－ping，Liu Wei－bo.The construction of changeable intruder model in model checking［J］.Journal of Beijing University of Posts and Telecommunications，2011，34（2）：54－57.（in Chinese）

［15］ Li Xing－feng，Zhang Xin－chang，Yang Mei－h(huán)ong，et al.Study on modularized model checking method based on SPIN［J］.Journal of Electronics ＆Information Technology，2011，33（4）：902－907.（in Chinese）

［16］ Xiao Mei－h(huán)ua，Xue Jin－yun.Formal description of properties of concurrency system by temporal logic［J］.Journal of Naval University of Engineering，2004，16（5）：10－13.（in Chinese）

［17］ Salamah S，Ochoa O，Jacquez Y.Using pairwise testing to verify automatically－generated formal specifications［C］∥Proc of 2015IEEE 16th International Symposium on High Assurance Systems Engineering（HASE），2015：279－280.

附中文參考文獻(xiàn)：

［4］ 陳偉，楊伊彤，牛樂(lè)園.改進(jìn)的OAuth2.0協(xié)議及其安全性分析［J］.計(jì)算機(jī)系統(tǒng)應(yīng)用，2014，23（3）：25－30.

［5］ 王煥孝，顧純祥，鄭永輝.開(kāi)放授權(quán)協(xié)議OAuth2.0的安全性形式化分析［J］.信息工程大學(xué)報(bào)，2014，15（2）：141－147.

［6］ 余鵬，魏歐，韓蘭勝，等.模型檢測(cè)網(wǎng)絡(luò)傳播干預(yù)策略［J］.計(jì)算機(jī)科學(xué)與探索，2014，8（8）：906－918.

［9］ 胡良文，馬金晶，孫博.基于SPIN 的SysML 活動(dòng)圖驗(yàn)證框架［J］.計(jì)算機(jī)科學(xué)與探索，2014，8（7）：836－847.

［12］ 侯剛，周寬久，勇嘉偉，等.模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述［J］.計(jì)算機(jī)科學(xué)，2013，40（z1）：77－85.

［14］ 楊元原，馬文平，劉維博.模型檢測(cè)中可變攻擊者模型的構(gòu)造［J］.北京郵電大學(xué)學(xué)報(bào)，2011，34（2）：54－57.

［15］ 李興鋒，張新常，楊美紅，等.基于SPIN 的模塊化模型檢測(cè)方法研究［J］.電子與信息學(xué)報(bào)，2011，33（4）：902－907.

［16］ 肖美華，薛錦云.時(shí)態(tài)邏輯形式化描述并發(fā)系統(tǒng)性質(zhì)［J］.海軍工程大學(xué)學(xué)報(bào)，2004，16（5）：10－13.