计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2004年
8期
117-121
,共5页
刘学锋%石昊苏%薛锐%周径野
劉學鋒%石昊囌%薛銳%週徑野
류학봉%석호소%설예%주경야
形式化分析%串空间模型%模型检测%状态空间剪枝
形式化分析%串空間模型%模型檢測%狀態空間剪枝
형식화분석%천공간모형%모형검측%상태공간전지
串空间模型是分析安全协议的一种实用、直观和严格的形式化方法.概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构,提出一些剪枝规则对状态搜索空间进行剪枝.通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间,防止状态空间爆炸.
串空間模型是分析安全協議的一種實用、直觀和嚴格的形式化方法.概述基于該模型結閤使用定理證明和模型檢測技術開髮的安全協議驗證工具AVSP的體繫結構,提齣一些剪枝規則對狀態搜索空間進行剪枝.通過Needham-Schroeder安全協議的弱一緻性認證屬性驗證過程來錶明這些狀態搜索空間剪枝規則可有效縮小狀態搜索空間,防止狀態空間爆炸.
천공간모형시분석안전협의적일충실용、직관화엄격적형식화방법.개술기우해모형결합사용정리증명화모형검측기술개발적안전협의험증공구AVSP적체계결구,제출일사전지규칙대상태수색공간진행전지.통과Needham-Schroeder안전협의적약일치성인증속성험증과정래표명저사상태수색공간전지규칙가유효축소상태수색공간,방지상태공간폭작.
