《電子技術(shù)應(yīng)用》
您所在的位置:首頁 > 通信與網(wǎng)絡(luò) > 設(shè)計應(yīng)用 > 數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計與實(shí)現(xiàn)[圖]
數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計與實(shí)現(xiàn)[圖]
CCTIME
CCTIME
摘要: CSP,數(shù)據(jù)獨(dú)立,進(jìn)程,映射,數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計與實(shí)現(xiàn)[圖],1996年,Lowe首先使用通信順序進(jìn)程CSP和模型檢測技術(shù)分析NSPK(Needham-Schro
Abstract:
Key words :

1996年,Lowe首先使用通信順序進(jìn)程CSP和模型檢測技術(shù)分析NSPK(Needham-Schroeder Public Key)協(xié)議,并成功發(fā)現(xiàn)了協(xié)議中的一個中間人攻擊行為。隨后,Roscoe對CSP和FDR(Fallures-Divergence Refinenent)的組合做了進(jìn)一步研究,認(rèn)為CSP方法是形式分析安全協(xié)議的一條新途徑。事實(shí)證明,CSP方法對于安全協(xié)議分析及發(fā)現(xiàn)安全協(xié)議攻擊非常有效。但是類似FDR的模型檢測通常受NONce、Key等新鮮值大小的限制,而在實(shí)際執(zhí)行中所需的數(shù)據(jù)值比這大得多。使用數(shù)據(jù)獨(dú)立技術(shù)使結(jié)點(diǎn)能夠調(diào)用無限的新鮮值以保證實(shí)例無限序列的運(yùn)行。本文將研究Roscoe這些理論,對CSP協(xié)議模型進(jìn)行設(shè)計與實(shí)現(xiàn),從而解決有限檢測的問題。

1 CSP協(xié)議模型

在CSP模型中,協(xié)議參與者被表示為CSP的進(jìn)程(process),消息被表示為事件(event),進(jìn)而協(xié)議被表示為一個通信順序進(jìn)程的集合。

CSP協(xié)議模型由一些可信的參與者進(jìn)程和入侵者進(jìn)程組成,進(jìn)程并行運(yùn)行且通過信道交互。以NSPK協(xié)議為例。該協(xié)議的CSP模型包括兩個代理(初始者a,響應(yīng)者b)和一個能執(zhí)行密鑰產(chǎn)生、傳送或認(rèn)證服務(wù)的服務(wù)器s,它們之間通過不可信的媒介(入侵者)通信,所以存在四個CSP進(jìn)程,如圖1所示。

 

數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計與實(shí)現(xiàn)

Initiator a的CSP進(jìn)程描述如下:

 

數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計與實(shí)現(xiàn)

響應(yīng)者b與服務(wù)器s也有著相似的描述。

攻擊者進(jìn)程被描述為:

 

數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計與實(shí)現(xiàn)

2 數(shù)據(jù)獨(dú)立技術(shù)

數(shù)據(jù)獨(dú)立技術(shù)是本論文的關(guān)鍵技術(shù).它起源于Lazic的數(shù)據(jù)獨(dú)立研究。

2.1 一般的數(shù)據(jù)獨(dú)立分析

如果一個進(jìn)程P對于類型T沒有任何限制,則P對于T類型是數(shù)據(jù)獨(dú)立的。此時,T可以被視為P的參數(shù)。

通常,數(shù)據(jù)獨(dú)立分析是為以類型T為參數(shù)的驗證問題發(fā)現(xiàn)有限閾值。如果對于T的閾值,可以驗證系統(tǒng)成立,則對于所有較大的T值也可以驗證系統(tǒng)成立。這點(diǎn)對于很多問題都是成立的。

安全協(xié)議模型中的許多特征都可以被視為數(shù)據(jù)獨(dú)立實(shí)體。常見的key、nonce可以作為模型中進(jìn)程的參數(shù)。

對依賴nonce和密鑰(和依賴協(xié)議的其他簡單數(shù)據(jù)對象)惟一性的安全協(xié)議進(jìn)行的閥值計算,主要是發(fā)現(xiàn)進(jìn)程存儲量的閾值,并不能直接解決驗證的局限性,也就不能直接應(yīng)用于安全協(xié)議模型。

2.2 Roscoe的數(shù)據(jù)獨(dú)立技術(shù)

此內(nèi)容為AET網(wǎng)站原創(chuàng),未經(jīng)授權(quán)禁止轉(zhuǎn)載。