黃鵬

摘要：安全協(xié)議是以密碼學(xué)為基礎(chǔ)的消息交換協(xié)議。針對(duì)傳統(tǒng)的改進(jìn)NSSK安全協(xié)議，通過(guò)使用Promela語(yǔ)言對(duì)協(xié)議進(jìn)行建模，并使用SPIN模型檢測(cè)工具進(jìn)行驗(yàn)證，發(fā)現(xiàn)仍然存在安全漏洞，攻擊者可以冒充合法者進(jìn)行通信。針對(duì)上述缺陷，提出了一種有效的改進(jìn)方案，主要是在協(xié)議中增加了自身產(chǎn)生的隨機(jī)數(shù)和發(fā)送者的身份標(biāo)識(shí)，該改進(jìn)方案提高了協(xié)議安全性。

關(guān)鍵詞：安全協(xié)議； 安全漏洞；NSSK；SPIN；模型檢測(cè)

DOIDOI：10.11907/rjdk.171239

中圖分類號(hào)：TP309文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)：16727800（2017）010018504

0引言

如今，隨著信息逐漸成為重要的戰(zhàn)略資源，信息化水平已成為衡量一個(gè)國(guó)家現(xiàn)代化水平和綜合國(guó)力的重要標(biāo)志。同時(shí)，信息安全問(wèn)題也成為人們重點(diǎn)關(guān)注的一個(gè)問(wèn)題。安全協(xié)議是以密碼學(xué)為基礎(chǔ)的消息交換協(xié)議，其目的是在網(wǎng)絡(luò)環(huán)境下提供各種安全服務(wù)。安全協(xié)議可以分為密鑰交換協(xié)議、認(rèn)證協(xié)議、電子商務(wù)協(xié)議、安全多方計(jì)算協(xié)議等多種類型。簡(jiǎn)單安全協(xié)議雖然只是簡(jiǎn)單消息的傳遞，但消息之間存在微妙、復(fù)雜的關(guān)系。NSSK協(xié)議[12]是一個(gè)經(jīng)典的認(rèn)證密碼協(xié)議，不少學(xué)者在NSSK協(xié)議研究中提出了一些NSSK認(rèn)證方案，但這些方案也不是完全安全的，仍然存在風(fēng)險(xiǎn)。2014年Hu等主要根據(jù)GSMR系統(tǒng)現(xiàn)有的安全威脅和必須采取的安全措施，采用一種改進(jìn)的NSSK安全協(xié)議來(lái)保障車載設(shè)備與RBC之間的安全通信。通過(guò)分析發(fā)現(xiàn)，其存在著一些安全缺陷，因此提出了改進(jìn)方案。

本文使用SPIN模型檢測(cè)工具對(duì)NSSK協(xié)議的改進(jìn)方案進(jìn)行驗(yàn)證和分析，發(fā)現(xiàn)存在著攻擊。因此，針對(duì)該攻擊提出一種改進(jìn)方案，以提高協(xié)議安全性。

1模型檢測(cè)及工具SPIN

系統(tǒng)的設(shè)計(jì)和驗(yàn)證需要SPIN模型檢測(cè)器的支持，首先形式化描述整個(gè)系統(tǒng)模型，對(duì)模型進(jìn)行分析，發(fā)現(xiàn)語(yǔ)法錯(cuò)誤，如果沒(méi)有發(fā)現(xiàn)語(yǔ)法錯(cuò)誤，則需要對(duì)系統(tǒng)進(jìn)行交互模擬運(yùn)行，直到系統(tǒng)設(shè)計(jì)達(dá)到預(yù)期為止。然后，SPIN會(huì)生成一個(gè)優(yōu)化的onthefly驗(yàn)證程序，該程序?qū)⒈痪幾g后執(zhí)行，如果在執(zhí)行過(guò)程中發(fā)現(xiàn)了任何違背正確性的反例，則會(huì)返回交互模擬執(zhí)行狀態(tài)，繼續(xù)進(jìn)行檢測(cè)診斷，以確定產(chǎn)生反例的原因。因此，它的建模方法是：定義進(jìn)程模板，將每個(gè)進(jìn)程模板的行為視為一種行為規(guī)范，實(shí)際系統(tǒng)可以被看作一個(gè)或多個(gè)異步進(jìn)程模板實(shí)例的組合。SPIN是一種基于計(jì)算機(jī)科學(xué)的形式化方法，它將先進(jìn)的理論驗(yàn)證方法應(yīng)用于大型軟件系統(tǒng)的驗(yàn)證中，目前在工業(yè)界和學(xué)術(shù)界得到了廣泛應(yīng)用。

SPIN的基本結(jié)構(gòu)如圖1所示，其描述了整個(gè)檢測(cè)過(guò)程。

2協(xié)議介紹

2.1NSSK協(xié)議原理及存在的問(wèn)題

NSSK協(xié)議是一個(gè)經(jīng)典的認(rèn)證密碼協(xié)議。協(xié)議先通過(guò)對(duì)兩個(gè)主體的身份進(jìn)行認(rèn)證，通信主體需要經(jīng)過(guò)5個(gè)階段的通信過(guò)程，才能獲得安全通信過(guò)程的會(huì)話密鑰。

協(xié)議符號(hào)說(shuō)明：A表示用戶A的身份標(biāo)識(shí)；B表示用戶B的身份標(biāo)識(shí)；S表示服務(wù)器；Nb表示用戶B產(chǎn)生的隨機(jī)數(shù)；Na表示用戶A產(chǎn)生的隨機(jī)數(shù)；Kbs表示用戶B與S之間的共享密鑰；Kas表示用戶A與S之間的共享密鑰；Kab表示用戶A和用戶B的會(huì)話密鑰。

協(xié)議的步驟如下：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）A→B：{Kab，A}Kbs

（4）B→A：{Nb}Kab

（5）A→B：{Nb-1}Kab

在此協(xié)議中，用戶A和用戶B進(jìn)行秘密通信，用戶A會(huì)向服務(wù)器S請(qǐng)求分配一個(gè)會(huì)話密鑰來(lái)保證通信內(nèi)容的秘密性。協(xié)議前3個(gè)消息主要是服務(wù)器分配會(huì)話密鑰給合法用戶，后兩個(gè)消息主要是合法用戶之間的相互驗(yàn)證。

具體過(guò)程為：①協(xié)議開始時(shí)，合法用戶A將用戶A的身份標(biāo)識(shí)、用戶B的身份標(biāo)識(shí)以及用戶A產(chǎn)生的隨機(jī)數(shù)Na組成消息1，發(fā)送給服務(wù)器S，告訴服務(wù)器它將與用戶B進(jìn)行通信；②服務(wù)器S在接收到消息1時(shí)，隨機(jī)產(chǎn)生一個(gè)Kab，這是為雙方分配的會(huì)話密鑰，同時(shí)將A的身份標(biāo)識(shí)和Kab用B的密鑰Kbs加密生成一個(gè)證書，然后將證書、用戶A在消息1發(fā)送的Na、用戶B的身份標(biāo)識(shí)和會(huì)話密鑰Kab用A的密鑰Kas加密組成消息2發(fā)送給A；③用戶A接收到消息2時(shí)，用密鑰Kas解密消息得到會(huì)話密鑰Kab和證書{Kab，A}Kbs，然后再將證書組成消息3發(fā)送給用戶B；④用戶B接收到消息3時(shí)，用密鑰Kbs解密得到會(huì)話密鑰Kab，再用Kab加密自身產(chǎn)生的隨機(jī)數(shù)Nb組成消息4，發(fā)送給用戶A；⑤用戶A接收到消息4后，用會(huì)話密鑰Kab解密得到Nb，再將Nb與1進(jìn)行運(yùn)算后，將得到的結(jié)果用Kab進(jìn)行加密組成消息5發(fā)送給用戶B。這里的Nb-1可以用Nb來(lái)代替，只是用來(lái)區(qū)別消息4，而消息4和消息5是為了防止中間人攻擊。

在此協(xié)議中，在消息4中用戶A是通過(guò)Nb來(lái)確認(rèn)用戶B的身份，在消息5中用戶B是通過(guò)Nb-1來(lái)確認(rèn)用戶A的身份。這里的Kab表示用戶A和用戶B之間的會(huì)話密鑰，只有用戶A和用戶B可以對(duì)其解密。

該協(xié)議比較簡(jiǎn)單，實(shí)現(xiàn)起來(lái)也較為容易，但在文獻(xiàn)[8]中，Denning和Sacco在1981年發(fā)現(xiàn)了一個(gè)攻擊，發(fā)現(xiàn)此協(xié)議不能抵抗“新鮮性”攻擊，如果一個(gè)攻擊者擁有過(guò)期的會(huì)話密鑰，能夠冒充用戶A，通過(guò)重放消息3，來(lái)實(shí)施以下攻擊：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）I（A）→B：{ K′ab，A}Kbs

（4）B→I（A）：{N′b}K′ab

（5）I（A）→B：{N′b-1}K′ab

其中，I（X）表示攻擊者可以冒充合法用戶X接收和發(fā)送消息。通過(guò)上面的攻擊過(guò)程，使合法用戶B相信自己得到的會(huì)話密鑰K′ab是執(zhí)行當(dāng)前協(xié)議回合的結(jié)果。因此，該攻擊是有效的。endprint

在2001年，王貴林、卿斯?jié)h等在文獻(xiàn)[12]又提出攻擊者可以冒充合法用戶B實(shí)施以下攻擊：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）A→I（B）：{Kab，A}Kbs

（4）I（B）→A：NI

（5）A→I（B）：{{NI}K-1ab-1}Kab

其中，NI和{Nb}Kab格式相同，攻擊者冒充用戶B發(fā)送消息給用戶A，用戶A收到消息4，然后對(duì)其進(jìn)行所謂的解密，并將得到的結(jié)果與1進(jìn)行運(yùn)算后，將運(yùn)算后的結(jié)果用Kab加密發(fā)給用戶B。用戶A以為用戶B知道了會(huì)話密鑰，但實(shí)際上，B根本沒(méi)有參加整個(gè)協(xié)議的執(zhí)行過(guò)程，甚至可能還是離線的。因此，該攻擊是有效的。

2.2協(xié)議改進(jìn)方案

文獻(xiàn)[7]分析了NSSK協(xié)議后，提出一種改進(jìn)方案，該方案采用的符號(hào)與原協(xié)議相同，而且消息形式與原協(xié)議相似，修改后的完整協(xié)議簡(jiǎn)單描述如下：

（1）A→S：A，B，Na。用戶A通過(guò)發(fā)送消息1給服務(wù)器S，它將與用戶B進(jìn)行通信，主要將用戶A的身份標(biāo)識(shí)、用戶B的身份標(biāo)識(shí)和用戶A產(chǎn)生的隨機(jī)數(shù)Na組成消息1提供給服務(wù)器S。

（2）S→B：A。當(dāng)服務(wù)器S接收到消息1后，隨即發(fā)送A的用戶標(biāo)識(shí)給用戶B。S通過(guò)發(fā)送消息告訴用戶B，用戶A要與其進(jìn)行通信。

（3）B→S：{ Nb} Kbs。當(dāng)用戶B接收到消息2后，知道用戶A將與它通信，然后將自身產(chǎn)生的隨機(jī)數(shù)Nb用密鑰Kbs進(jìn)行加密組成消息3，將其發(fā)送給服務(wù)器S。

（4）S→A：{ Na ，B，Kab} Kas。當(dāng)服務(wù)器S收到消息3后，將用戶A產(chǎn)生的隨機(jī)數(shù)Na、用戶B的身份標(biāo)識(shí)、用戶A與用戶B之間的密鑰Kab用A的密鑰Kas進(jìn)行加密，組成消息4發(fā)送給用戶A，告訴用戶A，用戶B已經(jīng)準(zhǔn)備好與之通信。

（5）S→B：{ Nb ，A，Kab} Kbs。服務(wù)器S收到消息3后，解密消息3得到Nb，然后再將用戶B的隨機(jī)數(shù)Nb、用戶A的身份標(biāo)識(shí)、用戶A與用戶B之間的密鑰Kab用B的密鑰Kbs進(jìn)行加密，組成消息5發(fā)送給用戶B，通知用戶B，用戶A已經(jīng)準(zhǔn)備好與之通信。

（6）B→A：{N′b}Kab。當(dāng)用戶B接收到消息5后，將自己產(chǎn)生的隨機(jī)數(shù)N′b用會(huì)話密鑰Kab加密組成消息6，再發(fā)送給用戶A。

（7）A→B：{N′b-1}Kab。當(dāng)用戶A接收到消息6后，用會(huì)話密鑰Kab解密消息6，得到N′b，然后將N′b與1計(jì)算后得到N′b-1，用會(huì)話密鑰Kab加密N′b-1組成消息7，再發(fā)送給用戶B。

此改進(jìn)協(xié)議也是用戶A通過(guò)N′b來(lái)確認(rèn)用戶B的身份。同樣，用戶B通過(guò)N′b-1來(lái)確認(rèn)用戶A的身份。

3改進(jìn)協(xié)議Promela建模及分析

3.1攻擊者建模

攻擊者[11]可以根據(jù)自身的知識(shí)能力對(duì)網(wǎng)絡(luò)和信息采取敵意的行為，其可以具備如下知識(shí)能力：①在合法主體通信過(guò)程中，對(duì)其進(jìn)行截獲或者轉(zhuǎn)發(fā)任何消息；②可以冒充合法用戶或服務(wù)器參與協(xié)議運(yùn)行；③可以對(duì)協(xié)議里的任何消息進(jìn)行解密和加密；④可以對(duì)協(xié)議里的任何消息進(jìn)行重構(gòu)，通過(guò)重構(gòu)消息來(lái)試圖欺騙用戶和服務(wù)器。

3.2協(xié)議系統(tǒng)屬性

NSSK協(xié)議及其改進(jìn)方案都是在秘密狀態(tài)下，用戶與用戶之間身份的相互鑒別，同時(shí)協(xié)商了會(huì)話密鑰，所以該協(xié)議必須滿足認(rèn)證性和秘密性。認(rèn)證性的含義為：A與B如果成功運(yùn)行了一次協(xié)議，那么用戶A要相信通信對(duì)方就是用戶B，同時(shí)用戶B相信通信對(duì)方就是用戶A，即通信雙方的真實(shí)身份要相互鑒別。用LTL公式表示如下：

[]（（statusA==ok&&partnerA==responserID）？（statusB=ok&&partnerB==askerID））

其中&&表示邏輯與，←→表示邏輯等價(jià)，[]表示always。

秘密性的含義為：要確保需要加密的協(xié)議消息內(nèi)容在傳送過(guò)程中不被攻擊者非法竊取。根據(jù)協(xié)議特點(diǎn)，從消息3到消息7都有密鑰進(jìn)行加密，攻擊者無(wú)法獲得其隨機(jī)數(shù)N′b，也無(wú)法冒充用戶或服務(wù)器進(jìn)行攻擊。因此，只要成功運(yùn)行了一次協(xié)議，LTL公式則能保證其秘密性。

3.3驗(yàn)證結(jié)果分析

通過(guò)模型檢測(cè)工具Xspin檢測(cè)改進(jìn)后的協(xié)議可發(fā)現(xiàn)漏洞，并得到入侵者的攻擊路徑。入侵者利用獲得的消息，重構(gòu)消息冒充B與A通信，最終使A誤認(rèn)為它與B通信，其實(shí)是I與之進(jìn)行通信，成功地對(duì)其進(jìn)行了攻擊。

其中askerID代表A的身份標(biāo)識(shí)，responserID代表B的身份標(biāo)識(shí)，nonceA、nonceI分別代表A、I產(chǎn)生的隨機(jī)數(shù)，nonceB1和nonceB2分別代表B在協(xié)議消息1和消息6產(chǎn)生的隨機(jī)數(shù)，keyAB代表A與B之間的會(huì)話密鑰，keyBS代表B的密鑰，keyAS代表A的密鑰，key代表I產(chǎn)生的密鑰，temp代表空值。為了簡(jiǎn)化建模過(guò)程，最后一步驗(yàn)證消息沒(méi)有減1。攻擊路徑如圖2所示。

圖2協(xié)議改進(jìn)受攻擊軌跡

由圖2得知入侵者攻擊時(shí)序如下：

（1）A→S：A，B，Na

（2）S→B：A

（3）B→S：{ Nb} Kbs

（4）S→A：{ Na，B，Kab} Kas

（5）S→I（B）：{ Nb，A，Kab} Kbs

（6）I（B）→A：NI

（7）A→I（B）：{{NI}K-1ab-1}Kab

攻擊過(guò)程描述如下：攻擊過(guò)程的前4個(gè)消息都是A、S、B接收消息或轉(zhuǎn)發(fā)消息，攻擊過(guò)程主要是在后面3個(gè)消息中：先是入侵者I冒充用戶B發(fā)送NI給A，其中NI與{N′b}Kab格式相同，A接收到消息6后對(duì)其進(jìn)行所謂的解密，得到結(jié)果后，將結(jié)果與1運(yùn)算后用Kab加密后組成消息7發(fā)送給B，I將其截獲。endprint

通過(guò)上述分析，在文獻(xiàn)[7]的改進(jìn)協(xié)議中，前5個(gè)消息是分配會(huì)話密鑰，在消息4和消息5分別加上了隨機(jī)數(shù)，從而可以抵抗文獻(xiàn)[8]提出的新鮮性攻擊。但發(fā)現(xiàn)的攻擊與王貴林、卿斯?jié)h等在文獻(xiàn)[12]發(fā)現(xiàn)的攻擊類似，B在消息4之后就沒(méi)有收到消息，一直在等待消息，但A不知B在等待消息，以為它還在與B進(jìn)行通信，其實(shí)I在與A進(jìn)行通信，攻擊有效，所以說(shuō)其無(wú)法抵抗該攻擊。

3.4NSSK協(xié)議改進(jìn)

NSSK協(xié)議受攻擊的原因是，文獻(xiàn)[7]改進(jìn)的協(xié)議消息6太過(guò)簡(jiǎn)單，容易被重構(gòu)騙過(guò)合法的參與者。

針對(duì)上述攻擊，對(duì)協(xié)議的改進(jìn)如下：

（1）A→S：A，B，Na

（2）S→B：A

（3）B→S：{ Nb} Kbs

（4）S→A：{ Na ，Nb，B，Kab} Kas

（5）S→B：{ Na，Nb，A，Kab} Kbs

（6）B→A：{Nb，Na，B}Kab

（7）A→B：{Nb-1，Nb，A}Kab

對(duì)其改進(jìn)的協(xié)議進(jìn)行建模，改進(jìn)的協(xié)議和文獻(xiàn)[7]改進(jìn)協(xié)議格式相同，只是傳遞的消息內(nèi)容有所差別，建模過(guò)程和上文的建模過(guò)程相似，用模型檢測(cè)工具Xspin對(duì)上述改進(jìn)后的協(xié)議進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如圖3所示。

圖3對(duì)改進(jìn)NSSK協(xié)議的驗(yàn)證結(jié)果

通過(guò)驗(yàn)證結(jié)果發(fā)現(xiàn)，結(jié)果顯示錯(cuò)誤為0，則新改進(jìn)的協(xié)議沒(méi)有發(fā)現(xiàn)漏洞，說(shuō)明新改進(jìn)的協(xié)議是安全的。

3.5改進(jìn)方案安全性分析

定理1改進(jìn)方案能加強(qiáng)雙向認(rèn)證。

證明在協(xié)議的后兩條消息中分別加上了自己之前產(chǎn)生的隨機(jī)數(shù)，在消息6中，當(dāng)合法用戶A解密消息得到自己的隨機(jī)數(shù)和B的身份標(biāo)識(shí)，才會(huì)相信是用戶B發(fā)來(lái)的消息，在消息7中原理相同。因此，該協(xié)議能夠加強(qiáng)雙向認(rèn)證。

定理2改進(jìn)方案能抵抗中間人攻擊。

證明對(duì)于文獻(xiàn)[7]的改進(jìn)協(xié)議，主要是消息6容易被攻擊者篡改，偽裝攻擊欺騙合法用戶，所以在消息6和消息7中分別增加前面產(chǎn)生的隨機(jī)數(shù)和身份標(biāo)識(shí)，如果解密消息不是自己產(chǎn)生的隨機(jī)數(shù)和身份標(biāo)識(shí)，用戶會(huì)拒絕該消息，攻擊者則無(wú)法重構(gòu)信息來(lái)欺騙合法用戶。因此，改進(jìn)方案能抵抗中間人攻擊。

定理3改進(jìn)方案能夠抵抗重放攻擊。

證明對(duì)于文獻(xiàn)[7]的改進(jìn)協(xié)議，攻擊者截取到消息6后，會(huì)重放該消息來(lái)騙過(guò)合法用戶，所以在消息6加上合法用戶前面產(chǎn)生的隨機(jī)數(shù)和身份標(biāo)識(shí)，如果解密消息得不到期望的消息，用戶會(huì)拒絕該消息，使攻擊者無(wú)法通過(guò)重放消息6來(lái)欺騙合法用戶。因此，改進(jìn)方案能抵抗重放攻擊。

4結(jié)語(yǔ)

本文使用Promela語(yǔ)言對(duì)NSSK協(xié)議[7]的改進(jìn)方案進(jìn)行建模，根據(jù)協(xié)議必須滿足的安全性質(zhì)描述（LTL公式、斷言）進(jìn)行驗(yàn)證，用模型檢測(cè)工具Xspin進(jìn)行檢測(cè)，成功地找出了反例。通過(guò)分析攻擊序列產(chǎn)生的原因，給出了一種修改方案。通過(guò)驗(yàn)證和分析發(fā)現(xiàn)，改進(jìn)后的協(xié)議可以滿足安全協(xié)議要求。SPIN模型檢測(cè)技術(shù)是分析安全協(xié)議的有效工具，下一步工作可以使用SPIN工具檢測(cè)和改進(jìn)其它安全協(xié)議。

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

[1]LIAO J， ZHU B， YONG H. Security analysis of NSSK protocol and its improvement[C].Eighth IEEE International Conference on Dependable， Autonomic and Secure Computing， Dasc 2009， Chengdu， China， DBLP， 2009：115118.

[2]CHEN L， WANG W. An improved NSSK protocol and its security analysis based on logic approach[C]. International Conference on Communications， Circuits and Systems. IEEE， 2008：772775.

[3]TINGYUAN L， XIAODONG L， ZHIGUANG Q， et al. An improved security protocol formal analysis with BAN logic[C].International Conference on Electronic Commerce and Business Intelligence. IEEE Xplore， 2009：102105.

[4]WANG X， YUAN C W. Formal analysis method of security protocol[J]. Computer Engineering， 2010， 36（7）：8284.

[5]CHEN H，CLARK J A，JOCOB J L.A searchbased approach to the automated design of security protocols，YCS 376[R].New York：University of York，Department of Computer Science，2004.

[6]LERDA F， SISTO R. Distributedmemory model checking with SPIN[C]. SpringerVerlag， 1999：2239.

[7]胡曉輝，陳慧麗，石廣田，等.CTCT4級(jí)安全通信協(xié)議的形式化建模與驗(yàn)證[J]. 計(jì)算機(jī)工程與應(yīng)用， 2014，50（4）：8185.

[8]DENNING D E， SACCO G M. Timestamps in key distribution protocols[J]. Communications of the Acm， 1981，24（8）：533536.

[9]王巧麗.SPIN模型檢測(cè)的研究與應(yīng)用[D].貴陽(yáng)：貴州大學(xué)，2006.

[10]楊霓霏，劉曉斌，盧佩玲，等.CTCS3級(jí)列控系統(tǒng)車地?zé)o線通信消息認(rèn)證和加密技術(shù)的研究[J].鐵道通信信號(hào)，2010，46 （10）：15.

[11]尤啟房，楊晉吉.SIP協(xié)議的SPIN模型檢測(cè)[J].計(jì)算機(jī)工程與應(yīng)用，2014，50（13）：8789.

[12]王貴林，卿斯?jié)h，周展飛.認(rèn)證協(xié)議的一些新攻擊方法[J].軟件學(xué)報(bào)，2001，12（6）：907913.

[13]萬(wàn)子龍.基于模型檢測(cè)的SET協(xié)議形式化驗(yàn)證與改進(jìn)[D].南昌：南昌大學(xué)，2014.

[14]李翠翠.基于SPIN模型檢測(cè)的電子商務(wù)協(xié)議分析與驗(yàn)證[D].上海：華東理工大學(xué)，2012.

責(zé)任編輯（責(zé)任編輯：黃?。〆ndprint