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