目前，安全协议的验证工作主要采用各种形式化方法，如逻辑证明和模型检测。基于逻辑证明的安全协议分析在发现协议是不安全的之后不能给出现实的攻击路径，且协议的理想化过程及主观性假设往往会影响分析的结果。基于模型检测的安全协议分析虽然在近些年才开始受到人们的关注，但是其发展非常迅猛。特别是有序二叉决策树(OBDD)等符号化技术的引入有效地解决了模型检测面临的状态爆炸问题，产生了符号化模型检测技术。现在，符号化模型检测技术已经开始广泛地应用的安全协议的验证工作中，各种符号化模型检测工具，如SMV等应运而生。 IBS (Internet Business Server) 协议是卡内基-梅隆大学开发的电子商务协议。到目前为止，还没有文献对IBS协议进行基于符号化模型检测的安全分析。为此，本文首先采用 SMV 符号化模型检测工具对比较简单的智力扑克协议(mental poker)的公平性进行了安全验证。接着对IBS协议的不可否认性、公平性等安全性能进行了验证。结果表明IBS协议不满足不可否认性和公平性。根据检测结果给出的现实攻击路径，我们对协议进行了相应的改进。随后，我们还在有第三方攻击者的安全模型下对IBS协议的安全验证。