微型电脑应用
微型電腦應用
미형전뇌응용
MICROCOMPUTER APPLICATIONS
2015年
8期
4-6
,共3页
自动验证%驱动模型%串空间模型%认证协议
自動驗證%驅動模型%串空間模型%認證協議
자동험증%구동모형%천공간모형%인증협의
@@
为了实现对认证协议的自动验证,首先,通过对认证协议的协议主体行为分析,给出了驱动模型(Driving Module,DM)的定义.然后,根据串空间模型中的常规者串和攻击者串分别构建了常规者DM和攻击者DM.最后,提出了基于常规者DM和攻击者DM的自动验证算法.实例分析和定理证明表明,该算法的搜索过程不仅是全面和正确的,而且能有效地避免状态空间爆炸问题.
為瞭實現對認證協議的自動驗證,首先,通過對認證協議的協議主體行為分析,給齣瞭驅動模型(Driving Module,DM)的定義.然後,根據串空間模型中的常規者串和攻擊者串分彆構建瞭常規者DM和攻擊者DM.最後,提齣瞭基于常規者DM和攻擊者DM的自動驗證算法.實例分析和定理證明錶明,該算法的搜索過程不僅是全麵和正確的,而且能有效地避免狀態空間爆炸問題.
위료실현대인증협의적자동험증,수선,통과대인증협의적협의주체행위분석,급출료구동모형(Driving Module,DM)적정의.연후,근거천공간모형중적상규자천화공격자천분별구건료상규자DM화공격자DM.최후,제출료기우상규자DM화공격자DM적자동험증산법.실례분석화정리증명표명,해산법적수색과정불부시전면화정학적,이차능유효지피면상태공간폭작문제.
