计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2008年
17期
130-132
,共3页
庄庆%蔡小娟%董笑菊%戚正伟
莊慶%蔡小娟%董笑菊%慼正偉
장경%채소연%동소국%척정위
线性时序逻辑%安全协议%保密性%认证性
線性時序邏輯%安全協議%保密性%認證性
선성시서라집%안전협의%보밀성%인증성
介绍一个基于GSPM的安全协议验证的图形化工具.验证工具以GSPM模型为基础形式化地描述了安全协议,并引进线性时序逻辑刻画了安全协议的性质,用基于状态搜索的模型检测方法在安全协议的验证过程中找出漏洞.以简化的NSPK协议为例,描述了该工具如何验证安全协议,表明GSPM模型和验证算法的有效性和正确性.
介紹一箇基于GSPM的安全協議驗證的圖形化工具.驗證工具以GSPM模型為基礎形式化地描述瞭安全協議,併引進線性時序邏輯刻畫瞭安全協議的性質,用基于狀態搜索的模型檢測方法在安全協議的驗證過程中找齣漏洞.以簡化的NSPK協議為例,描述瞭該工具如何驗證安全協議,錶明GSPM模型和驗證算法的有效性和正確性.
개소일개기우GSPM적안전협의험증적도형화공구.험증공구이GSPM모형위기출형식화지묘술료안전협의,병인진선성시서라집각화료안전협의적성질,용기우상태수색적모형검측방법재안전협의적험증과정중조출루동.이간화적NSPK협의위례,묘술료해공구여하험증안전협의,표명GSPM모형화험증산법적유효성화정학성.
