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

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

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

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

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