基于Strand空間模型的安全協(xié)議分析方法研究.pdf

1、該文通過對基于Strand空間模型的安全協(xié)議分析方法的研究,提出了用于提高安全協(xié)議分析效率的改進(jìn)的狀態(tài)空間簡化技術(shù).在協(xié)議分析過程中,將一般的狀態(tài)空間簡化技術(shù)與剪枝定理相結(jié)合,不但刪除了協(xié)議運行的冗余狀態(tài),而且刪除了協(xié)議運行的不可達(dá)狀態(tài),從而有效地簡化了狀態(tài)空間,大大減少了協(xié)議分析的工作量.也就是說,在協(xié)議分析過程中,令入侵者總是截獲誠實主體發(fā)送的消息,并以該消息豐富其知識集合,以便增強(qiáng)其攻擊能力;同時,入侵者總是等待誠實主體沒有消息發(fā)

2、送的時候才重發(fā)或偽造消息給協(xié)議主體,從而使入侵者每次發(fā)送消息前,其知識集合都盡可能完備,以便形成最有效的攻擊.以上兩種簡化技術(shù)的應(yīng)用刪除了協(xié)議運行的大量冗余狀態(tài),并且不會遺漏導(dǎo)致攻擊的狀態(tài).為了刪除協(xié)議運行的不可達(dá)狀態(tài),在協(xié)議分析時,可根據(jù)協(xié)議特點,設(shè)計適用于該協(xié)議的剪枝定理.對于協(xié)議分析中的每個狀態(tài),首先以剪枝定理判斷該狀態(tài)的可達(dá)性,再確定是否需要對該狀態(tài)進(jìn)行進(jìn)一步擴(kuò)展.剪枝定理的應(yīng)用刪除了協(xié)議運行的不可達(dá)狀態(tài),進(jìn)一步簡化了狀態(tài)空間.

3、在Strand空間模型的基礎(chǔ)上,通過在安全協(xié)議分析算法的設(shè)計中選擇合理的狀態(tài)結(jié)構(gòu)記錄協(xié)議的運行情況,使該改進(jìn)的狀態(tài)空間簡化技術(shù)易于實現(xiàn).即通過使入侵者知識集合盡量完備,并且隨著其知識的增加,刪除其中的冗余信息,有利于入侵者生成攻擊時所需要的消息;通過優(yōu)先綁定發(fā)送消息的節(jié)點,并使入侵者總是截獲誠實主體發(fā)送的消息,有效刪除了協(xié)議分析中的冗余狀態(tài),并將誠實主體發(fā)送的消息用于豐富入侵者知識集合,從而增強(qiáng)了入侵者的能力;通過在狀態(tài)轉(zhuǎn)換前檢查狀態(tài)的

4、可達(dá)性,刪除了協(xié)議分析中的不可達(dá)狀態(tài)以及以這些狀態(tài)為根的狀態(tài)轉(zhuǎn)換子樹.作為利用該技術(shù)簡化安全協(xié)議分析的實例,在對Needhan-Schroeder-Lowe協(xié)議的分析過程中,以認(rèn)證定理作為剪枝定理,將其與一般的簡化技術(shù)相結(jié)合,簡化了該協(xié)議的分析過程.并且根據(jù)該設(shè)計思想,通過VB下的程序設(shè)計,實現(xiàn)了對Needhan-Schroeder協(xié)議的認(rèn)證性質(zhì)分析.總之,在Strand空間模型的基礎(chǔ)上,在協(xié)議的認(rèn)證性質(zhì)分析過程中,通過將狀態(tài)空間簡化技