随着网络多样化发展,以及移动支付、社交网络等新技术的不断涌现,信息安全领域中的认证与授权技术得到了长足的发展。其中,可信认证协议及授权协议由于近几年广泛应用受到越来越多人的关注,这些协议具有安全属性多样性、逻辑结构复杂性等特点,使得构造验证模型与精确地刻画协议的安全属性变得非常困难。因此有关可信认证协议及授权协议的安全性分析问题成了安全研究中的一个难点和关键点。形式化验证是专门针对安全协议的安全性分析所提出的一种自动化检验方法,其原理是将安全协议转换为某种数学模型,将协议满足的安全要求转换为某种数学公式,然后通过验证建立的模型是否满足数学公式来检验安全协议的安全性。这种基于严谨的数学逻辑推导来达到证明效果的方法被公认为证明协议安全性的有效方法。针对上述问题,本文以可信属性认证系统、授权协议动态客户端注册协议的形式化建模与验证为研究重点,首先提出面向可选择披露的属性认证系统的形式化模型框架;其次对复杂的可信属性认证协议U-Prove进行了形式化分析和安全性验证。最后,论文对授权协议中的客户端动态注册协议进行了形式化建模,在建模过程中发现了该协议在特定环境下具有安全隐患,随后对协议提出了改进措施,并通过形式化验证的方法对改进后的协议进行了安全性验证。具体研究内容如下:(1)针对可信认证系统形式化建模的需求,提出了一种面向可选择披露的属性认证系统的形式化模型框架。描述了可选择披露属性认证系统的抽象结构,刻画了系统中属性结构、实体结构和行为特征。对用户不同的属性添加了类型定义,给出分类函数及具体行为描述,对系统各个实体及实体之间的交互行为进行抽象,其执行条件、具体的行为均给出了进程描述。针对系统需要满足的签名不可伪造性、匿名性和属性的隐私性给出安全特性定义。模型对于系统的设计与安全性分析具有实际意义。(2)基于前一步工作,将模型检测方法应用于可信认证协议U-Prove的形式化验证中。U-Prove是一种新的复杂密码技术,其核心是一个嵌有属性的U-Prove令牌,用户通过该令牌可以实现身份的识别,且不会泄露任何隐私信息。论文首先利用上述模型框架完成对U-Prove协议的形式化建模,以及协议满足的有关安全属性的形式化建模,然后通过ProVerif工具完成了 U-Prove协议相关安全属性的验证工作。实验结果证明协议的模型能够满足相关的安全属性。(3)进一步,在对开放授权协议中的客户端动态注册协议的形式化分析中发现了其具有安全隐患,针对存在的安全隐患提出了相应的改进措施,并对改进后的客户端动态注册协议进行了形式化验证工作。原有的开放授权协议中,用户完全信任授权服务器,对于己注册的客户端注册信息的正确性与完整性缺乏检测机制。在客户端注册后,授权服务器一旦在应用层遭到攻击,则攻击者可以任意篡改或伪造客户端的注册信息,从而导致用户在授权时被重定向到某个恶意站点。本文针对该安全隐患提出了改进措施,引入安全注册中心对注册信息进行保护,使得用户在授权时可以对客户端的注册信息进行可靠性分析,从而避免了上述攻击。为了验证改进后的协议安全特性,论文对新方案进行了建模及形式化验证工作,实验结果表明改进后的协议可以避免原协议中存在的攻击,具有更高的安全性。