安全协议是以密码学为基础,在通信网络和分布式系统中提供各种安全服务的一种协议,在信息系统安全中占据重要的位置。然而对安全协议进行分析和验证是一项非常有挑战的工作,成为安全协议发展与应用的瓶颈。由于安全协议的发展已经超出了人们进行严格分析和验证的能力,因此有必要对安全协议自动化检测技术进行研究。　　 本文研究了基于SAT(Satisfaction)的安全协议自动化检测的关键技术,并指出现有检测工具在检测协议类型上的局限性,然后针对该问题,对检测协议类型进行扩展,提出了无类型消息和多协议中的候选辅助协议的概念,设计并实现了基于SAT的安全协议自动化检测系统SAT-ADS(Automatic Detection System ofSecurity Protocols Based SAT),使SAT-ADS可以检测类型缺陷攻击和多协议攻击,并经过实例验证检测的可行性。　　 最后,应用SAT-ADS检测系统对BAN modified Andrew Secure RPC协议进行检测,发现了一个尚未公开的中间人攻击。本文对此协议提出了一种改进方法,即在协议交互消息中加入一个身份标识,经验证,改进后的协议避免了中间人攻击的漏洞。