计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2014年
z2期
85-90
,共6页
安全协议%形式化验证%Spin模型检测%Promela语义模型%LTL公式%密钥分配中心协议
安全協議%形式化驗證%Spin模型檢測%Promela語義模型%LTL公式%密鑰分配中心協議
안전협의%형식화험증%Spin모형검측%Promela어의모형%LTL공식%밀약분배중심협의
security protocol%formal verification%Spin model checking%Promela semantic model%Linear Timing Logic ( LTL) formula%key contribution center protocol
针对安全协议的形式化验证问题，运用模型检测方法，以一种改进的入侵者Promela语义模型，对双方密钥分配中心协议进行Spin模型检测，验证发现其不满足线性时序逻辑（ LTL）公式描述的安全性，得到了原协议的安全漏洞。针对该漏洞，提出了一种协议改进方案，并针对改进后的协议，给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法：模型检测过程中的存储状态数减少，使模型复杂度降低约40'；迁移状态数减少，使验证效率提升约44'。
針對安全協議的形式化驗證問題，運用模型檢測方法，以一種改進的入侵者Promela語義模型，對雙方密鑰分配中心協議進行Spin模型檢測，驗證髮現其不滿足線性時序邏輯（ LTL）公式描述的安全性，得到瞭原協議的安全漏洞。針對該漏洞，提齣瞭一種協議改進方案，併針對改進後的協議，給齣新的Promela語義模型的建模方法。改進的入侵者模型建模方法比起原方法：模型檢測過程中的存儲狀態數減少，使模型複雜度降低約40'；遷移狀態數減少，使驗證效率提升約44'。
침대안전협의적형식화험증문제，운용모형검측방법，이일충개진적입침자Promela어의모형，대쌍방밀약분배중심협의진행Spin모형검측，험증발현기불만족선성시서라집（ LTL）공식묘술적안전성，득도료원협의적안전루동。침대해루동，제출료일충협의개진방안，병침대개진후적협의，급출신적Promela어의모형적건모방법。개진적입침자모형건모방법비기원방법：모형검측과정중적존저상태수감소，사모형복잡도강저약40'；천이상태수감소，사험증효솔제승약44'。
Aiming at the formal verification problem in security protocols, an improved Promela semantic intruder model was used to complete the model checking for key distribution center protocol, to find that it does' t meet the security property described by LTL ( Linear Temporal Logic) formula, and to get a protocol vulnerability. An improvement program against vulnerability was proposed. A new Promela semantic modeling was put forward for the improved protocol. The improved intruder modeling method reduces the number of states stored in the model checking, thus the model complexity reduces about 40'; and reduces the number of transiations, thus the verification efficiency increases about 44' .
