模型检测是一种验证软硬件系统的强有力方法,它首先用形式化语言来描述待检验系统和系统需要满足的规范,然后使用DFS（Depth First Search）等算法遍历系统模型的状态空间,找出不满足规范的地方并返回反例以指导系统修改。但是现有的模型检测器都是基于单反例的,其在验证系统时往往需要人为的多次干预才能完成验证过程。另一方面,随着移动互联网时代下各种应用和平台的用户量爆发增长,人们将自己在某个平台的信息授权给第三方应用的场景越来越常见。OAuth 2.0（Open Authorization）协议作为一种开放授权协议,被国内外许多企业和应用如微信、Google、Facebook等用作其信息授权解决方案。然而,目前关于OAuth2.0协议安全性的研究工作还不够多,且存在建模不准确、分析效率不高等问题。本文使用多反例方法对模型检测工具SPIN（Simple Promela Interpreter）进行研究和改进,并利用模型学习方法和改进后的SPIN对OAuth 2.0协议进行分析验证。具体地,主要工作如下:（1）本文改进了模型检测器SPIN。SPIN是一个基于单反例的模型检测工具,在使用SPIN进行协议验证时,如果发现一个反例它就会自动中止,需要人为地对引发这个反例的错误进行修改,然后重新进行验证以生成下一个反例,这个过程较为繁琐。本文提出了对SPIN验证流程的修改方法,使其仅需一次验证就能搜索出所有反例。针对这些反例中可能存在相似反例的问题,本文借鉴字符串相似度的度量方法对相似反例进行了精简和消除。此工作简化了SPIN的验证过程,提高了它的工作效率,同时对于其它协议和程序的分析也具有积极作用。（2）本文使用模型学习方法对OAuth 2.0协议进行了建模。建模是模型检测方法的第一步,建模的准确性直接影响到验证结果。相比于传统的人为分析建模,模型学习是一种更高效的建模方法,具有自动化程度高、建模准确等优点。本文首次将模型学习方法引入OAuth 2.0协议的建模过程,建立了协议的模型。（3）本文使用多反例的SPIN对OAuth 2.0协议进行了验证。验证结果发现该协议存在一个漏洞,攻击者可以在未经用户授权的情况下获取访问令牌,然后窃取用户的受保护资源。针对这一漏洞本文提出了对OAuth 2.0协议流程的一种改进方法,该方法通过为重定向地址添加授权服务器身份信息来保证安全性,最后通过实验验证了改进方法的有效性。