基于模型检测工具SPIN的安全协议分析和验证

摘要

随着Internet和分布式系统的广泛应用，安全协议逐渐发挥着越来越重要的作用。形式化的方法是分析安全协议的主要方法。目前已经有很多研究安全协议的理论和方法，其中比较著名的有可证明安全理论、BAN逻辑、串空间模型理论以及模型检测和定理证明的方法等。 模型检测作为形式化分析安全理论方法的一种，有着自动化和提供反例等诸多优点。并且近年在硬件验证中得到了广泛应用。模型检测器SPIN是由贝尔实验室开发的一种专门用于软件和协议验证的工具。 本文基于模型检测工具SPIN，对电子商务协议Netbill协议做形式化地分析和验证。 首先对此协议从行为属性和安全性两方面进行抽象。包括对协议主体建立状态和状态转移描述；然后对协议采用PROMELA语言建立模型。协议的安全属性描述采用LTL逻辑公式。最后运用SPIN对协议的模型进行行为模拟，对LTL描述的协议属性进行正确性及安全性验证。在验证和模拟的过程中，随时根据模型的状态数目和系统的消耗调整抽象模型的结构和行为。对协议中不满足属性的验证结果进行分析和改进。最后，将分析和验证结果和其他安全协议的验证方法比较，总结现有工作和尚需完善的工作。

目录

文摘

英文文摘

原创性声明及关于学位论文使用授权的声明

第一章绪论

第二章理论背景

第三章基于SPIN的安全协议形式化分析和验证

第四章结论及展望

参考文献

致谢

附录