安全协议通常描述了公共网络中两个或多个智能进程之间的消息交换行为,从而保证对交互过程中诸如认证、机密保持、密钥一致、隐私和匿名性等安全属性的支持。但是,设计一个安全可信的协议并不是一件容易的事情,而这些不安全的协议往往就系统攻击的入口点。从Lowe提出了形式化自动验证之后,该验证方法已经展示了其在协议安全性证明方面的强大优势并得到了广泛的应用。由于针对密码学原语具体算法的攻击往往难以分析,以自动化的形式证明攻击就更加困难,因此密码学操作原语在形式化验证中往往被看作是不带任何代数属性的函数符号,忽略其具体计算细节,这个假设被称为完美密码假设,也就是说加密后的消息除非使用相应的密钥解密打开,否则是不可能通过其他方式得到其对应明文的。基于这个假设,目前存在很多自动化验证工具,其中ProVerif以其高效的性能被公认为目前最优秀的验证工具之一。但是,ProVerif等工具没有涵盖那些利用密码学操作原语代数属性的攻击。因此,完美假设的限制需要适当放宽,从而将此类攻击有效的识别出来。位运算符XOR (exclusive or)广泛应用于最近几年流行的RFID协议中,再加上其简洁的格式,已经成为目前的研究热点。因此,为了能够更加有效的发现包含有XOR安全协议的攻击隐患,需要将对操作符代数属性的使用能力加入到入侵者的攻击能力中。特里尔大学的KUsters教授和Truderung最近提出了一个对包含有操作符XOR((?))安全协议的自动验证方法。在该方法中,包含有XOR的协议模型被自动转换为相应的可进行形式化验证的等价模型,其中已经包含了对XOR的代数属性运算的合理建模,该等价模型可以作为ProVerif的输入模型,由它自动验证。虽然该方法在验证机密性时表现出较高效率但是在认证属性的验证中往往效率不高,对某些协议甚至无法处理。本文中,针对KUsters和Truderung算法存在的缺陷,提出了两个改进方向：第一,为了扩展可验证认证属性的安全协议的范围,提出了有界验证的方法,使更多的XOR安全认证协议得到自动的有效证明；第二,为了提高该算法的效率,提出了一系列的优化方案,进一步减小转换后的协议模型的规模,缩短ProVerif的验证时间。通过设计实现测试模型,测试了常用的XOR协议标准和若干最新提出的RFID协议。实验结果表明本文提出的改进方案达到了预先的设想效果,并日.在实验中发现了在一个RFID协议上新的攻击过程。