基于ProVerif的TVP迁移协议安全性分析*

针对可信虚拟平台TVP(Trusted Virtual Platform)迁移协议缺乏有效的安全性验证的问题,引入应用pi演算对协议流程及安全属性进行形式化建模,并基于其自动化工具ProVerif对协议的弱机密性、强机密性及实体可认证性进行了分析,结果表明,该协议能够满足TVP迁移应用的安全要求。     

改进的OAuth2.0协议及其安全性分析

随着OAuth2．0协议的广泛应用,其安全性受到了人们的重点关注．为了增强OAuth2．0协议的安全性,本文首先引入数字签名技术,提出一个改进的OAuth2．0协议．它支持授权服务器对资源拥有者和客户端的身份认证．并且在计算模型下基于Blanchet演算,应用一致性对授权服务器认证资源拥有者和客户端进行建模,最后使用自动化工具CryptoVerif分析和证明了其认证性．     

一种改进的密码协议形式化模型

多重集重写MSR(multiset rewriting)模型是一种基于多重集重写的协议形式化建模方法.从目前的研究成果来看,该模型并不完善.针对其攻击者模型验证协议存在的不足,对MSR模型进行了改进,并给出了基于MSR模型的秘密性和认证性描述.实践表明,对模型的改进进一步完善了原模型.     

移动自组网中跨域两方认证密钥协商协议研究

针对基于身份的移动自组网认证密钥协商协议中,会话两方属于不同私钥生成中心（PKG）的情况,利用双线性对的性质和椭圆曲线离散对数问题,提出了一种跨域两方认证密钥协商协议,并采用应用pi演算和ProVerif自动化验证工具对其安全属性进行形式化分析。分析结果表明,提出的协议实现了保密性、身份认证性以及密钥一致性确认,同时又具有较好的性能,非常适用于资源有限的移动自组网。     

无双线性对的无证书两方认证密钥协商协议

鉴于双线性对运算复杂度较高,不适用于移动通信环境,提出新的无双线性对的基于无证书的两方认证密钥协商协议。新协议解决了基于身份的公钥密码方案中固有的密钥托管问题,实现了对通信双方的身份认证,采用非双线性对运算,极大地降低了计算开销。通过分析协议的正确性,采用Applied Pi演算对协议进行形式化分析,借助ProVerif工具验证了协议的安全性和认证性。与其他两方密钥协商协议相比,新方案具有更好的安全性和效率。     

基于扩展Spi演算的IKEv2协议形式化分析与改进

安全性是新一代密钥交换协议的关键,而Spi演算是研究协议安全性的一种形式化方法,文中采用Spi演算研究了IKEv2协议的安全属性。针对Spi演算不能形式化定义Diffie-Hellman密钥交换和密钥生成的问题,扩展了Spi演算的语法和语义。基于扩展的Spi演算形式化分析了IKEv2协议,分析结果表明协议满足认证性和私密性,但不能保护相对重要的发起方身份。针对IKEv2协议的不足,提出了一种基于Weil对签名算法的改进方案。改进后的协议解决了发起方身份保护问题,具有更好的安全性。     

安全协议的CSP描述技术

基于进程代数的CSP方法是一种重要的形式化协议分析验证方法。本文首先简单介绍了CSP相关理论,并以NSPK协议为例系统概述了安全协议的CSP建模方法。为更好的查明协议的安全缺陷,重点研究如何在CSP的体系结构中对协议的安全属性进行形式化描述。并最终提出秘密性、认证性、不可否认性、匿名性的形式化提炼检测目标,为进一步使用模型检测器进行协议验证奠定了理论和技术基础。     

光纤工程中基于OpenID的统一认证系统设计与实现

从OpenID入手分析了在当今企业云计算中统一认证的重要性,对原有的OpenID协议进行扩展和改进,设计了一种基于OpenID的企业用户身份统一认证模型,能够就企业用户进行分级认证和多重身份登录,旨在实现商业领域云服务系统统一认证的安全性和高效性,同时,减轻用户的操作负担,通过一个实际的光纤工程项目结果来说明该模型能够提升云服务统一认证的效率,是一种可行且实用的认证模型,可以投入实际应用中.     

关于秘密共享方案在应用Pi演算中的实现

针对秘密共享方案的自动化验证问题,提出一种基于等值理论的秘密共享方案自动化验证方法。首先通过等值理论在应用Pi演算中对可验证的多秘密共享方案的密码学语义进行了形式化定义。在此基础上,进一步提出了一种用于将所提出等值理论转化为自动化协议验证器ProVerif中重写机制的编码方法,在ProVerif中实现了关于可验证的多秘密共享方案的自动化验证。通过证明给出了关于可验证的多秘密共享方案形式化分析结果的健壮性结论：如果自动化协议验证器ProVerif中可验证的多秘密共享方案的形式化分析结果满足特定安全属性,则其能够归约证明应用Pi演算模型中针对可验证的多秘密共享方案所建立的现实敌手可以“模拟”ProVerif验证器中的理想敌手,其意味着现实敌手与理想敌手是不可区分的。     

无线认证协议Linear MAKEP的模型检验

模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验。对检验结果进行分析发现：在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性。给出了协议的一种改进,使其满足认证性。     

OpenID身份认证系统的认证等级模型研究

以OpenID为现有的切入点,分析了现代分布式认证体系中,依赖站点和用户对认证协议安全性方面的需求,提出了对OpenID协议的扩展,根据不同的认证需求定义了4种不同的认证等级,从匿名性、完整性和不可伪造性3个特性上对认证等级进行了研究,并给出了解决方法和密码学算法。同时,协议能够通过满足完整性和不可伪造性,提高用户对依赖站点的信任度。这一认证等级的提出,可以为各类网络服务的定位提供参考,也为用户在选择依赖站点的判断上,提供了安全性方面的衡量标准。     

一种云计算中的多重身份认证与授权方案

OpenID是一种广泛应用于云计算中的去中心化的身份认证技术。OpenID为用户以一个身份在多个云服务中通行提供了一种方式,也解决了因遗失在云提供商处注册的云身份凭证而不能登录的问题。但用户以OpenID身份登录云服务后,却不能访问该用户的云身份拥有的资源,且OpenID技术也没有对请求身份信息的云服务进行认证与细粒度授权。因此文章在OpenID技术和OAuth技术的基础上,设计了一种多重身份认证与授权方案来解决上述同一用户不同身份的资源不可访问问题,以及身份信息等资源访问流程中的细粒度授权问题。     

基于SM9盲签名的OpenID协议

OpenID是一个以用户为中心的数字身份识别框架,同时又是一个去中心化的网上身份认证系统,它具有开放、分散、自由等特性。但是,当前已有的一些OpenID协议在有效保护用户隐私方面仍存在诸多不足,如身份提供商可以通过每次使用了解用户登录的依赖方信息。针对上述问题,本文提出一种基于盲签名的OpenID协议设计思路,将OpenID依赖方的网站标识符进行盲化。首先基于国密算法SM9设计一个身份基盲签名方案,并证明该方案的安全性依赖于SM9签名方案;随后基于上述盲签名方案,设计一个OpenID协议;最后通过仿真实验和理论分析论证所提出的OpenID协议的高效性和安全性。     

改进的抵抗离线字典攻击的口令更新协议

口令认证是最简单,方便和应用最广泛的一种用户认证方式。最近,Tsaur等人指出了Chang等人的口令更新协议存在拒绝服务攻击并且不能提供口令的后向安全。随后,他们给出了一种改进的口令更新协议,并声称该协议是安全的。文中,分析了Tsaur等人的口令更新协议,指出了其方案是易受离线字典攻击的,且不能提供口令的前向和后向安全性。最后,提出一种改进的口令更新协议,并分析其安全性。     

Analysis of privacy vulnerabilities in single sign-on mechanisms for multimedia websites

This paper studies the privacy risks for the users of two popular single sign-on platforms for web-based content access: OpenID and Facebook Connect. In particular we describe in detail a privacy vulnerability of the OpenID Authentication Protocol that leads to the exposure of the OpenID user identifier to third parties. We illustrate how OpenID agents leak the (potentially unique) OpenID identifiers of their users to third parties, like advertisement and traffic analysis corporations. This vulnerability is a real and widespread privacy risk for OpenID users. This paper also analyzes the privacy of Facebook Connect --the proprietary single sign-on platform that is gaining a lot of popularity recently-- and, we conclude that it is not affected by the same vulnerability but other important privacy issues remain. Finally, this paper studies the solution space of these problems and defines a number of possible countermeasures. In the case of the OpenID vulnerability, we propose three solutions to this problem: one for the long term to avoid the root cause of the vulnerability, and another two short-term mitigations.     

基于OpenID的可兼容身份认证系统设计与实现

研究提供数字认证基础服务的OpenID协议认证机制,设计并实现了基于OpenID的身份认证系统.该系统兼容OpenID 1.1和OpenID 2.0规范,实现三个扩展协议,并且通过具体应用分析了其安全性.使用该标准认证系统可以整合其他的登录认证系统,实现单点登录.     

New semantic model for authentication protocols in ASMs

A new semantic model in Abstract State Model (ASM) for authentication protocols is presented. It highlights the Woo-Lam's ideas for authentication, which is the strongest one in Lowe's definition hierarchy for entity authentication. Apart from the flexible and natural features in forming and analyzing protocols inherited from ASM, the model defines both authentication and secrecy properties explicitly in first order sentences as invariants. The process of proving security properties with respect to an authentication protocol blends the correctness and secrecy properties together to avoid the potential flaws which may happen when treated separately. The security of revised Helsinki protocol is shown as a case study. The new model is different from the previous ones in ASMs.     

Towards the integration of reputation management in OpenID

OpenID is an open standard providing a decentralized authentication mechanism to end users. It is based on a unique URL (Uniform Resource Locator) or XRI (Extensible Resource Identifier) as identifier of the user. This fact of using a single identifier confers this approach an interesting added-value when users want to get access to different services in the Internet, since users do not need to create a new account on every website they are visiting. However, OpenID providers are normally used as a point to store certain personal attributes of the end users too, which might be of interest for any service provider willing to make profit from collecting that personal information. The definition of a reputation management solution integrated as part of the OpenID protocol can help users to determine whether a given service provider is more or less reliable before interacting with it and transferring their private information. This paper is providing the definition of a reputation framework that can be applied to the OpenID SSO (Single Sign-On) standard solution. It also defines how the protocol itself can be enhanced so OpenID providers can collect (and provide) recommendations from (to) users regarding different service providers and thus enhancing the users' experience when using OpenID. Besides the definition, a set of tests has been performed validating the feasibility of the framework.     

云计算中身份认证技术研究

对于云平台中用户之间的安全性认证问题,在分析openstack云平台的平台架构、安全认证组件keystone、云计算中身份认证的主要安全性问题及当前云环境中主流的身份认证技术的基础之上,针对云平台下的统一身份认证机制及统一身份认证技术的漏洞,着重分析了OpenID身份认证的工作原理,提出了OpenID当前存在的安全性问题,并得出了一些改进方案。最后以OpenID改进技术为基础,在openstack平台上实现了身份认证技术。