基于Spi演算的密碼協(xié)議自動化分析技術(shù)研究

◆江 濤

?

基于Spi演算的密碼協(xié)議自動化分析技術(shù)研究

◆江 濤

(國務(wù)院法制辦公室秘書行政司 北京 100000)

密碼協(xié)議可以維護(hù)網(wǎng)絡(luò)通信和其中的各個分布式系統(tǒng)的安全，為了讓惡意攻擊者無法獲取機密信息或者借安全漏洞進(jìn)行不公平認(rèn)證，需要對協(xié)議所運行的環(huán)境安全性進(jìn)行提升和技術(shù)改進(jìn)。而通過以前的靜態(tài)分析測試和人工手動驗證，對密碼協(xié)議的所存在的威脅和漏洞檢測不夠全面，由此其重要性得以體現(xiàn)。根據(jù)這一研究模塊，本文將對其演算基礎(chǔ)以及實現(xiàn)自動化的分析方式，還有Spi演算方式在密碼協(xié)議中對其秘密性的驗證和認(rèn)證性的分析演算做基本闡述。

Spi演算；密碼協(xié)議；自動化；分析技術(shù)

0 引言

密碼協(xié)議是為了針對預(yù)防攻擊者而以密碼體制為基礎(chǔ)來建立相互傳遞信息的協(xié)議，運用對密鑰進(jìn)行分配、對身份進(jìn)行認(rèn)證等技術(shù)，用以加強協(xié)議的正確性、安全性和抗變換性這三大要點?？赏谶壿嬯P(guān)系千變?nèi)f化，會因為當(dāng)時對協(xié)議所運行環(huán)境的了解不足而致使遺漏設(shè)計細(xì)節(jié)。如何完善密碼協(xié)議成為了人們的思考焦點，而在Spi演算基礎(chǔ)上的密碼協(xié)議的自動化分析技術(shù)應(yīng)運而生，并受到了廣泛關(guān)注。

1 基于Spi演算密碼協(xié)議的形式化分析

在形式化分析種存在一些不同的驗證方法，例如在知識和信念方面實現(xiàn)推理的模態(tài)邏輯方法，以定理證明為基礎(chǔ)的方法和以進(jìn)程演算為基礎(chǔ)的方法。1997年Abadi和Gordon建立的Sp i演算[1]，除了能夠?qū)M(jìn)程信息、間值和通道名稱進(jìn)行同步傳遞，還可以用其簡單語法和豐富的描述能力，為密碼協(xié)議進(jìn)一步提供密碼操作原語，在運用Dolev-Yao模型的基礎(chǔ)上，面對密碼協(xié)議所執(zhí)行的每一個進(jìn)程分析其與攻擊者所執(zhí)行進(jìn)程相交替的可能，用以驗證其各項性質(zhì)。

在Spi演算的基礎(chǔ)上，我們需要運用相應(yīng)的操作語義來對已經(jīng)建模的密碼協(xié)議驗證其所滿足的安全屬性，通常會用的有程序分析技術(shù)、模型檢測技術(shù)和互模擬等價技術(shù)這三種。

首先要說的是模型檢測技術(shù)，它需要密碼協(xié)議被實現(xiàn)，也就是被轉(zhuǎn)換成有限的狀態(tài)轉(zhuǎn)換圖，以此同時密碼協(xié)議所滿足的性質(zhì)也需要被規(guī)范，通常是將性質(zhì)用某種時態(tài)邏輯來約束，而模型檢測技術(shù)也就是通過確定實現(xiàn)的狀態(tài)轉(zhuǎn)換圖是否和被規(guī)范的密碼協(xié)議性質(zhì)相符，用這個來驗證有限狀態(tài)系統(tǒng)的技術(shù)類型。

其次是程序分析技術(shù)，其被分為靜態(tài)分析和動態(tài)分析，在現(xiàn)在的發(fā)展情況中靜態(tài)分析要比動態(tài)分析更完善，其已經(jīng)具備自動分析系統(tǒng)性質(zhì)的方法和工具，動態(tài)分析雖然可以有效的保護(hù)密碼協(xié)議執(zhí)行過程中可能出現(xiàn)的分支，并且具有驗證空間小、實現(xiàn)效率高的優(yōu)勢，但是目前還沒有合適的自動化驗證工具出現(xiàn)。因此，由于動態(tài)分析的先天不足，程序分析技術(shù)也主要可以從靜態(tài)分析方面被分為數(shù)據(jù)流分析和控制流分析[2]。

最后，互模擬關(guān)系作為進(jìn)程演算領(lǐng)域的核心概念之一，使互模擬等價技術(shù)的成長促發(fā)了進(jìn)程演算被廣為運用在程序的驗證和并發(fā)系統(tǒng)建模，而目前，互模擬驗證技術(shù)也主要是以Spi演算為基礎(chǔ)的。所以其在利用測試等價關(guān)系的形式化分析過程中的應(yīng)用基本被分為四個方面：

（1）協(xié)議整體和協(xié)議參與主體要用Spi演算轉(zhuǎn)換成具體描述來進(jìn)行形式化展示。

（2）在滿足密碼協(xié)議安全目標(biāo)的基礎(chǔ)上運用Spi演算對其規(guī)范形式進(jìn)行判斷。

（3）可以用反應(yīng)關(guān)系對被任意第三封閉進(jìn)程R和Barbβ測試的規(guī)范形式進(jìn)行約簡[2]。

（4）對密碼協(xié)議和其規(guī)范協(xié)議滿足的測試等價關(guān)系實施驗證，以確認(rèn)滿足的具體安全協(xié)議的要求。

2 基于Spi演算的密碼協(xié)議自動分析器的實現(xiàn)

2.1分析器工作原理

在運用邏輯方法在現(xiàn)有條件下，對擴展Spi演算語法和Spi演算在密碼協(xié)議安全屬性定義的基礎(chǔ)上實現(xiàn)的自動分析器，其化簡后的工作原理如圖1：

圖1分析器工作原理圖

該分析器基于被廣泛采用的Dolev-Yao模型，是根據(jù)密碼協(xié)議自動默認(rèn)在攻擊者是在運行環(huán)境中的，而攻擊者在環(huán)境中可以獲取密碼協(xié)議在信道上擁有的所有信息，并且可產(chǎn)生自己的消息和偽裝成一般的用戶發(fā)送消息。對于密碼協(xié)議的加密和解密操作，只有擁有相應(yīng)解密密鑰的用戶才可以將加密信息解密。

在密碼協(xié)議自動化分析器中對密碼協(xié)議及其協(xié)議參與主體的形式化描述、用戶對協(xié)議運行的設(shè)置條件還有驗證所要達(dá)到的安全目標(biāo)是用戶需要輸入的三個部分，也就是分析器所需的輸入語法。而自動翻譯模塊是對用戶所輸入的文件和語句部分進(jìn)行解析和處理，邏輯推導(dǎo)模塊則是被用以判斷每位用戶提供的信息是否可以從相關(guān)的事實和規(guī)則中導(dǎo)出。下面根據(jù)上述內(nèi)容對基于Spi演算下的密碼協(xié)議自動化分析器的分析過程主要步驟進(jìn)行簡要介紹：

第一，將之前被驗證的協(xié)議整體和協(xié)議參與主體受Spi演算的形式化描述輸入到系統(tǒng)中，根據(jù)系統(tǒng)參數(shù)和協(xié)議所運行的環(huán)境安排設(shè)定，主要是針對攻擊者屬性、信道屬性還有密鑰威脅等來確定驗證目標(biāo)。第二，分析器會根據(jù)用戶的環(huán)境參數(shù)自動驗證內(nèi)容，將協(xié)議的形式化描述轉(zhuǎn)為特定的語言，例如霍恩字句等，對協(xié)議進(jìn)行抽象描述。第三，分析器在進(jìn)行一番邏輯推理算法之后，它會在已有的事實和規(guī)則的基礎(chǔ)上自動搜索既定的驗證目標(biāo)，根據(jù)最后的具體情況來分別處理，如果在目前環(huán)境下協(xié)議不存在潛在的漏洞，則對協(xié)議分析給出正確的結(jié)果，反之，則向協(xié)議分析提供導(dǎo)致攻擊或者漏洞產(chǎn)生的路徑。

2.2密碼協(xié)議分析相關(guān)內(nèi)容

在以事實和規(guī)則為基礎(chǔ)的邏輯程序設(shè)計技術(shù)中，事實既是邏輯推理的前提假設(shè)，又是規(guī)則的依據(jù)。在分析器中真正完整的協(xié)議分析首先需要攻擊者初始知識以及符合其條件的事實，其次是對攻擊者計算能力的規(guī)則還有對協(xié)議本身的規(guī)則描述這兩個部分。

2.3分析器對密碼協(xié)議安全屬性的分析

首先是密碼協(xié)議秘密性驗證的問題，要對事實和規(guī)則定義的基礎(chǔ)上證明基于Spi演算的類型系統(tǒng)和分析器在安全屬性的分析方法方面的一致性，然后再由此去根據(jù)對應(yīng)事件進(jìn)程的定義去解決模型中對單射一致性和非單射一致性的證明問題。而在分析密碼協(xié)議安全屬性的方法上除了邏輯方法，其實還有密碼學(xué)方法，其分析結(jié)果比起邏輯方法的可信度要更高一些，而邏輯方法的優(yōu)勢在于，如果是在加密算法完善的情況下，分析效率比密碼學(xué)更高且直接簡潔，則更加有利于自動化分析技術(shù)的進(jìn)行[3]。

另外，在現(xiàn)有的邏輯程序設(shè)計技術(shù)基礎(chǔ)上引進(jìn)新的認(rèn)證邏輯系統(tǒng)，對分析器的分析能力其實是一種很有效的完善方式，通過羅列一些常用的定理并引進(jìn)多種符號和公式和增加新的消息源公理以及改進(jìn)原本的消息生成、身份認(rèn)證、消息接收公理，令基于Spi演算的密碼協(xié)議的自動化分析器能夠?qū)Ω囝愋偷拿艽a協(xié)議進(jìn)行嚴(yán)謹(jǐn)?shù)姆治雠袛?。而且這種方式能夠更好的讓公鑰密碼體制在密碼協(xié)議中發(fā)揮效用，例如能夠證明一些協(xié)議的安全性、可以找出更多協(xié)議的安全漏洞以及讓分析器不止適用于單一類型的協(xié)議。

這些都為我們后期針對密碼協(xié)議的安全漏洞提出并進(jìn)行相關(guān)的改進(jìn)方案，保證用戶的身份不被泄露的網(wǎng)絡(luò)安全性問題提供了保障[4]。密碼協(xié)議的自動化技術(shù)發(fā)展現(xiàn)在來說尚未達(dá)到一個較為平穩(wěn)的狀態(tài)，頻現(xiàn)的網(wǎng)絡(luò)安全性問題的解決需要不斷地將理論融合于實踐中去，并針對其在整個密碼協(xié)議中的應(yīng)用優(yōu)勢和缺點進(jìn)行分析和揚長避短。邏輯方法擁有的優(yōu)勢是采用進(jìn)程演算的分析效率，短處卻是現(xiàn)有的簡單邏輯被實際應(yīng)用后的分析結(jié)果可信度有待加強。如何完善語句，如何在加強安全性的同時提高分析效率等等一系列的問題都有待我們進(jìn)一步思考?，F(xiàn)今對基于Spi演算的密碼協(xié)議自動化分析器還只是初步的對單一邏輯進(jìn)程的演算，今后的研究中則需要進(jìn)一步深入了解復(fù)合邏輯，以實現(xiàn)同時驗證多個安全目標(biāo)的復(fù)合密碼協(xié)議的安全性。

3 結(jié)束語

與之前所研究的密碼協(xié)議所不同的是，其對密碼協(xié)議的兩項屬性，即認(rèn)證性和秘密性進(jìn)行分析，首先在信道上輸出的信息可以作為秘密性的依據(jù)，其次事件發(fā)生的先后順序和次數(shù)又可以用來驗證協(xié)議是否滿足密碼協(xié)議的認(rèn)證性，并利用Spi演算的擴展語法構(gòu)造類型系統(tǒng)與密碼協(xié)議進(jìn)行匹配，假設(shè)其中的進(jìn)程被密碼協(xié)議佐證出是無誤的，則認(rèn)定該進(jìn)程不存在泄露秘密級別數(shù)據(jù)的可能性，最終在以上原理基礎(chǔ)上實現(xiàn)密碼協(xié)議的自動分析技術(shù)。通過詳細(xì)的Spi演算過程對各主體間的精準(zhǔn)把握，恰好可以提升密碼協(xié)議的安全性。

[1]楊芳.基于模型檢測的安全協(xié)議自動驗證方法研究[D].湖南大學(xué)，2015.

[2]鄭清雄.基于Spi演算的安全協(xié)議形式化分析[D].上海交通大學(xué)，2010.

[3]程華清.密碼協(xié)議安全性分析的邏輯方法及其哲學(xué)意蘊[D].華東師范大學(xué)，2015.

[4]袁亞飛.邏輯化方法的改進(jìn)及若干密碼協(xié)議安全性分析[D].中國人民解放軍信息工程大學(xué)，2005.