IEEE802.11中WEP认证协议的SPIN模型检测

用SPIN工具对WEP认证协议进行模型检测,不仅可以从状态空间上搜索出协议的漏洞,还可以各个角度分析WEP协议的运行逻辑.模型检测的方法先通过建立WEP认证协议的模型,转换成SPIN的输入语言Promela,然后通过建立WEP协议的性质转化成LTL语言,最后利用SPIN工具分析WEP认证协议.实验的结果说明WEP认证协议存在漏洞.     

802.11i的认证安全性分析

IEEE设计802.11i协议解决无线局域网的安全问题.802.11i协议的形式化分析,对于确保该协议的正确性至关重要.利用串空间理论对802.11i协议进行建模,在串空间模型中验证协议的认证属性.结果表明,802.11i协议能够安全实现它的认证功能.     

基于802.11i的WLAN安全认证机制研究与实现

WLAN标准IEEE802.11的安全机制存在严重的漏洞,论证了如何以最新的IEEE802.11i标准中的安全机制来改善WLAN的安全性。考虑安全性与效率,应侧重依靠认证机制来实施WLAN的安全防护,通过IEEE802.11i RSN中的安全措施来更新WLAN现有的安全体系。最后基于EAP-TLS认证机制,设计了一种WLAN安全认证系统模型,该模型改变了传统认证机制中的安全策略,使用四步握手以及增强的密钥颗粒度方法提高了认证过程的安全性,并给出了该安全认证系统相应认证模块的软件实现方案,同时对该认证系统的安全性和适用性进行了相关论证。     

基于SPIN的网络认证协议高效模型检测

为了有效地提高网络认证协议建模和验证的效率,基于模型检测方法提出一个通用的网络认证协议模型描述方法,结合模型检测工具SPIN可以方便地进行性质验证。通过一些模型的简化策略,不仅可以对不同协议进行高效建模,而且减小了模型的状态空间。与现有的文献相比,自动化程度较高,模型验证的效率较好。基于该方法,对PKM认证协议进行了模型检测,实验证明该模型分析验证方法的有效性,可用于其他网络认证协议的分析验证。     

基于密钥的RFID双向认证安全协议

随着RFID技术的日益普及,安全问题,特别是用户隐私问题变得日益严重.在现有RFID认证协议的基础上,将双向认证与密钥加密算法有机地结合,较好地解决了RFID的安全隐患问题.该协议具有抗重放、抗分析、防伪造、防跟踪等特性.对该协议的安全性和性能进行比较分析,结果表明该协议可以为RFID系统提供较好的安全性.     

一种适合于低成本标签的RFID双向认证协议

在分析现有一些RFID认证协议的基础上,提出了一种新的适合低成本标签的双向认证协议,并对其进行了SMV模型检测形式化证明和性能分析。结果表明该认证协议具有认证性、保密性和完整性,能够满足低成本标签的安全需求,并且在安全性能提高的同时仍具有较好的执行性能。     

无线认证协议的模型检验分析研究

模型检验作为一种有效的分析和验证手段,在对有线认证协议的形式化分析上已得到了成功的应用,但关于无线认证协议的相关工作目前还比较少。论文应用模型检验方法对D.S.Wong等提出的无线认证协议(Server-specificMAKEP)的安全性进行分析,在分析过程中充分考察了无线环境中移动装置和无线网络的特点,验证结果表明了该方法用于分析无线认证协议的有效性。     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析．应用自动机和Promela对协议进行建模。利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析.应用自动机和Promela对协议进行建模,利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

Web服务认证协议模型安全性的研究

通过对入侵者攻击网络协议消息交互能力描述的阐述,构建具有Web服务安全协议模型函数,该模型包括安全协议头与安全体的相关消息。详细介绍了该模型中消息的语法结构和消息内容遵守Web服务安全规范的XML机制。分析了该协议模型安全性机制,并且给出其防止类型漏洞入侵与协议冲突入侵解决方案的思想。     

身份认证协议的模型检测分析

提出一个直观、易用的模型来模拟和验证身份认证协议，并给出基于Spin(模型检测工具）的实现，它不仅可以模拟多对参与者同时进行会话，而且还有效缩减了状态空间，从而避免了以前文献中提到的状态爆炸现象，同时该文用Needham-Schroeder公钥协议和TMN协议来说明如何应用该模型。     

无线认证协议Linear MAKEP的模型检验

模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验。对检验结果进行分析发现：在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性。给出了协议的一种改进,使其满足认证性。     

对一种身份认证协议的改进及其形式化分析①

基于口令的远程身份认证协议是目前认证协议研究的热点。2005年,Sung-Woon Lee等人提出了一个低开销的基于随机数的远程身份认证协议即Lee-Kim-Yoo协议,首先分析了此协议中所存在的安全性缺陷,随后构造了一个基于随机数和Hash函数,并使用智能卡的远程身份认证协议,最后用BAN逻辑对修改后的协议进行了形式化的分析,结果表明修改后的协议能够达到协议的安全目标。     

对一种身份认证协议的改进及其形式化分析①

基于口令的远程身份认证协议是目前认证协议研究的热点。2005年,Sung-WoonLee等人提出了一个低开销的基于随机数的远程身份认证协议即Lee—Kim—Yoo协议,首先分析了此协议中所存在的安全性缺陷。随后构造了一个基于随机数和Hash函数,并使用智能卡的远程身份认证协议,最后用BAN逻辑对修改后的协议进行了形式化的分析,结果表明修改后的协议能够达到协议的安全目标。     

基于符号模型检测的SDG故障诊断解形式化验证

由于定量信息和非线性因果关系的丢失,SDG的故障诊断解需要进一步的进行校核与验证。创新地将SDG故障诊断解的验证置于符号模型检测框架中进行研究,提出了基于符号模型检测的SDG故障诊断形式化验证方法。首先扩展、转换了SDG模型的有限状态变迁系统形式化描述,建立了SMV模型;其次引入故障传播时间建立了模型观测变量的动态验证信息,并基于步进式监控分析了动态验证策略,将SDG正向推理扩展建模为动态推理验证;然后面向符号模型检测扩展了动态推理验证过程的SMV模型,提出了验证算法SSDGFD_ SMC;最后,通过一个实例验证了算法的有效性。     

Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

This paper introduces a new methodology for epistemic logic, to analyze communication protocols that uses knowledge structures, a specific form of Kripke semantics over hostile networks. The paper particularly focuses on automatic verification of authentication protocols. Our approach is based on the actual definitions of a protocol, not on some difficultto-establish justifications. The proposed methodology is different from many previous approaches to automatic verification of security protocols in that it is justification-oriented instead of falsification-oriented, i.e., finding bugs in a protocol. The main idea is based on observations： separating a principal executing a run of protocol from the role in the protocol, and inferring a principal＇s knowledge from the local observations of the principal. And we show analytically and empirically that this model can be easily reduced to Satisfiability （SAT） problem and efficiently implemented by a modern SAT solver.     

Bytecode Verification by Model Checking

Java bytecode verification is traditionally performed by using dataflow analysis. We investigate an alternative based on reducing bytecode verification to model checking. First, we analyze the complexity and scalability of this approach. We show experimentally that, despite an exponential worst-case time complexity, model checking type-correct bytecode using an explicit-state on-the-fly model checker is feasible in practice, and we give a theoretical account why this is the case. Second, we formalize our approach using Isabelle/HOL and prove its correctness. In doing so we build on the formalization of the Java Virtual Machine and dataflow analysis framework of Pusch and Nipkow and extend it to a more general framework for reasoning about model-checking-based analysis. Overall, our work constitutes the first comprehensive investigation of the theory and practice of bytecode verification by model checking. This revised version was published online in August 2006 with corrections to the Cover Date.     

RPKI增量同步Delta协议的形式化检测与实现

现有RPKI体系中,RPKI资料库与RP服务器之间的数据同步使用开源工具Rsync,但由于RPKI体系中证书数据结构的特殊性,使用Rsync进行数据的同步不仅效率低下,而且Rsync会消耗过多的系统资源,从而使整个RPKI体系遭遇潜在的安全风险.因此,IETF针对RPKI资料库数据特征,提出增量同步Delta协议以替代Rsync在RPKI中的作用.本文详细介绍了Delta协议的工作逻辑和机制,从安全性和高效性两方面将之与Rsync进行全面对比,并使用Promela语言构建Delta协议模型,借助形式化验证工具SPIN对该模型进行验证,从而证明该协议具备较高的协议安全性和稳定性.最后,本文给出Delta协议的实现结构.     

共识协议的形式化验证研究现状与展望

分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.