基于串空间理论的安全协议自动验证

方案，形成了以下三类成果。其一是应用认证测试方法分析各种协议，证明协议的认证安全性，或找出协议在认证属性上存在的问题并改进。研究人员使用认证测试方法分析了NeedhamSchroeder协议[6]、OtwayRees协议和X.509等常规协议，还成功对安全传输层（Transport Layer Security，TLS）握手协议[7]、ISO/IEC（International Organization for Standardization/ International Electrotechnical Commission）97983认证协议[8]，以及A.Perrig传感器网络协议[9]回答：不是指文献[9]作者为perrig，是文献[9]中作者对A.Perrig提出的协议（名为A.Perrig传感器网络协议）进行了分析。不需要更改。文献[9]的作者名字不是Perrig？是否为指代错误，请作相应调整。等新的特殊用途协议的认证属性进行了分析。其二是将认证测试方法作为协议设计的辅助手段，Guttman[10]在2002年首次将认证测试定理用于电子商务协议的辅助设计，设计了一个新的电子商务协议ATSPECT（an Authentication Testbased Secure Protocol for Electronic Commerce Transactions），为认证测试定理的应用开辟了一个新的空间[11]。国内也有研究人员借鉴这一思路，使用认证测试定理设计出了一种双向认证的密钥协商协议[12]。其三就是对认证测试理论本身进行的研究。国内学者针对传统认证测试无法分析含双重加密消息项协议的不足[13]，引入了攻击等价类、测试元素变换链的概念[14]，对认证测试理论进行了改进。文献[15]研究了协议主体密钥在测试元素构造上的性质，探讨了构造测试元素的形式化规则。国外相关的研究包括：斯坦福大学Doghmi等[16]提出了完全认证测试的概念，指出符合完全认证测试的协议即使遭受攻击仍能正确实现主体的身份认证。德国奥尔登堡大学Frschle[17]将Petri网中“分支”的概念引入串空间和认证测试，扩展出分支丛的概念，从而可以检测出相冲突的协议执行序列。认证测试理论创始人Guttman[18]关注着协议的“渐增”设计过程中协议目标能否保持的问题，并使用串空间和认证测试理论进行了分析，并于其最新研究中使用扩展后的理论对Wang文献19的作者名字也不是Wang，是否为指代错误？请作相应调整。回答：同上，是指文献[19]作者Guttman中分析了Wang公平交换协议。不需要更改公平交换协议进行了分析[19]。

推荐访问： 验证 协议 理论 空间

---