软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2009年
10期
2799-2809
,共11页
安全协议%形式化方法%串空间%认证测试
安全協議%形式化方法%串空間%認證測試
안전협의%형식화방법%천공간%인증측시
security protocol%formal analysis method%strand space%authentication test
认证测试是一种用于证明安全协议认证属性的新方法,该方法能够简化协议认证属性的证明过程,但其局限性是无法应用于认证测试元素被多重加密的情况.指出Perrig和Song提出的认证测试改进方案在多个方面所存在的问题.在此基础上提出新的改进方案,并进行了形式化证明.新的认证测试定理突破了认证测试元素在整个协议消息中不能被加密的限制,扩展了认证测试理论的应用范围.
認證測試是一種用于證明安全協議認證屬性的新方法,該方法能夠簡化協議認證屬性的證明過程,但其跼限性是無法應用于認證測試元素被多重加密的情況.指齣Perrig和Song提齣的認證測試改進方案在多箇方麵所存在的問題.在此基礎上提齣新的改進方案,併進行瞭形式化證明.新的認證測試定理突破瞭認證測試元素在整箇協議消息中不能被加密的限製,擴展瞭認證測試理論的應用範圍.
인증측시시일충용우증명안전협의인증속성적신방법,해방법능구간화협의인증속성적증명과정,단기국한성시무법응용우인증측시원소피다중가밀적정황.지출Perrig화Song제출적인증측시개진방안재다개방면소존재적문제.재차기출상제출신적개진방안,병진행료형식화증명.신적인증측시정리돌파료인증측시원소재정개협의소식중불능피가밀적한제,확전료인증측시이론적응용범위.
Authentication test is a newly presented method that testifies protocols' authentication properties. Its proving process is simple and precise; unfortunately it can not analyze protocols with test components multi-encrypted. This paper analyzes the authentication test scheme improved by Perrig and Song and points out its deficiency. Then it proposes an Enhanced Authentication Test theory and proves its soundness in formal. The enhanced authentication test lifts the restriction that test component can not be multi-encrypted in protocol messages, also repairs the inaccuracies in Perrig's scheme.