运用SPIN对开放授权协议OAuth 2.0的分析与验证

OAuth 2.0协议是一种开放授权协议,主要用于解决用户账号关联与资源共享问题。但是,其弱安全性导致各网络公司海量用户信息泄露,且OAuth 2.0传输数据采用的https通道效率低下,成为黑客攻击对象。提出采用http通道传输OAuth 2.0协议数据,基于Promale语言及Dolev-Yao攻击者模型对OAuth 2.0协议建模,运用SPIN进行模型检测。形式化分析结果表明,采用公钥加密体系对OAuth 2.0协议进行加密不安全。上述建模方法对类似的授权协议形式化分析有重要借鉴意义。     

串空间模型对RPC协议机密性的验证

首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议的机密性进行了形式化分析与验证。     

一种理性安全协议的博弈逻辑描述模型

博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证。但在理性环境中,由于参与者对知识的自利性,ATL和ATEL都不能形式化分析与验证理性安全协议。因此在CEGS中引入效用函数和偏好关系知识,得到新的rCEGS,并在合作模态算子《Γ》中加入行为ACT参数,提出新的可形式化分析理性安全协议的交替时序认知逻辑rATEL-A。然后运用rATEL-A构建两方理性安全协议的形式化模型,并基于rCEGS的等价扩展式博弈,对具体的两方理性交换协议进行形式化分析,结果表明构建的形式化模型可以有效地形式化分析理性安全协议的正确性、理性安全性和理性公平性。     

基于模型检测的OpenFlow多交换机数据包转发协议的分析与验证

OpenFlow协议是SDN网络中控制平面与数据转发平面之间进行交互的规范与标准,其正确性将直接影响到整个网络功能的实现。通过模型检测技术实现一种验证OpenFlow协议正确性的形式化方法。首先提取OpenFlow协议的核心子协议,即OpenFlow多交换机数据包转发协议作为验证的实例;然后运用协议行为自动机对该子协议进行形式化建模,并且通过时态逻辑描述协议需要进行验证的性质;最后给出算法验证协议模型是否满足给定的性质要求,以此检测OpenFlow协议是否存在正确性漏洞,以便对其进行修正。     

基于串空间模型的Andrew安全RPC协议分析

在Andrew安全RPC协议模型的基础上,运用安全协议的形式化串空间模型分析方法,对Andrew安全RPC协议进行了分析,说明了该方法进行协议分析的过程,证明了该协议在机密性和认证性方面的正确性,并分析了该协议存在的安全缺陷。     

802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

基于串空间模型的Andrew RPC协议的分析与验证

本文首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议进行了形式化分析与验证,然后指出了安全缺陷。     

基于分段模型检测的云服务跨域认证协议的形式化分析与验证

针对多个云服务之间的跨域认证问题,提出一种基于SAML协议的云服务安全认证方案。阐明了该方案的关键技术机制,建立了云服务安全认证协议抽象模型;采用Casper和FDR软件的组合,通过模型检测法对云服务认证协议进行了形式化分析与验证;通过对安全认证协议进行分段模型检测,解决了安全协议形式化分析验证导致的状态空间爆炸问题。模型检测软件的实验结果验证了云服务跨域认证方案的有效性及安全性。     

基于CPN的RUDP建模与分析

目前可靠用户数据报协议(RUDP)有许多分析方式,但缺少形式化的模型.针对该问题,运用着色Petri网(CPN)对RUDP进行形式化建模,使用CPN Tools对模型进行仿真,通过生成的状态空间报告验证该协议模型的信息一致性、完整性和系统活性等性质.采用3次不同的实验对模型进行性能分析,实验结果显示,该模型的平均重传率为5％,能够模拟RUDP的行为,为研究RUDP提供一种形式化的方法.     

认证测试中协议主体串参数一致性研究

针对认证测试基础理论在协议主体串参数一致性分析方面,因形式化判定规则不足所产生的分析复杂度较高和自动化程度较低问题,通过对消息组件结构的形式化,以及认证测试结构的共性分析,基于认证测试基础理论对认证测试结构进行形式化建模;在认证测试结构模型上,运用协议主体密钥的认证测试构造规则,分析协议主体串在不同类型参数上满足一致性的条件,在明确参数一致性判定规则的同时,给出协议主体串参数一致性分析的形式化方法。协议分析实践表明,该方法较传统方法不仅具有简洁高效、易于自动化实现的优点,而且能够准确定位协议缺陷并给出相应的修正方案。     

基于Spin的SET协议模型检测研究

模型检测技术已成功地运用于验证复杂系统的性质。本文提出运用Promela语言对电子商务协议进行建模的方法,对比分析了有无入侵者时简化的SET协议的运行情况。运用Spin模型检测工具,对SET协议的Promela模型进行了检测,对电子商务协议中的关键性质认证性和保密性进行了分析与检测,发现了协议中的缺陷。     

SET中持卡人隐私保护分析及改进

本文简单介绍了SET协议，分析了它的隐私保护，并进行了改进扩展，提出了一种能够实行假名支付的新的模型。     

SSL/SET协议比较与改进模型

本文对SSL、SET两个电子商务安全协议作一比较，并针对不同的安全需要，构造一个分级安全控制模型，较好地改进了SET协议。     

SET协议形式化分析与模型检测

随着移动网络技术的快速发展,电子商务的大量普及,电子商务不在单单只是局限于有线网络,商家们开始将商机延续到移动网络。移动网络用户群体中手机移动上网用户占绝大部分,在这样的商机驱动下,移动电子商务得到快速发展。移动电子商务中最为核心的技术是移动电子支付协议SET,它直接决定了移动电子商务的安全性、高效性。本文就在这样的背景下采用AVISPA工具研究SET协议,通过形式化分析与模型检测,发现了SET协议的支付密钥的不安全性,并给出了攻击路径。     

改进SET对持卡人的隐私保护

SET是一个用于信用卡在线支付的安全规范，其交易模型由持卡人、商家、收单行、发卡行等各方组成。持卡人的个人信息(如卡号、密码、订单信息)可能被有关的参与方记录、收集、分析和滥用，因此对持卡人的隐私保护是十分重要的。本文分析了SET对持卡人隐私保护的不足，并提出了SET的改进方案，减少了个人隐私被泄露的风险。     

Secure Electronic Payments Based on Mobile Agents

The SET protocol for secure electronic payments, in particular its purchasing phase, is intended for users connected to the Internet during the entire transaction. This requirement cannot be easily met in high communication costs and/or low bandwidth settings, typically found in mobile computing environments.In this paper we describe SET/A, a system that works according to the SET rules for purchasing operations without forcing the user to be connected during the entire transaction. This is achieved by sending an agent to the merchant's server carrying all the data necessary to order and pay the goods (products, services or information). The paper shows that this can be achieved safely and efficiently, providing an alternative way for Internet payments using the SET protocol. We give our first impressions on SET/A usage by describing a prototype implementation based on a mobile agent system called AgentSpace, as well as a detailed example of what we consider a realistic application of the system.     

基于动态口令的SET改进及移动支付应用

在互联网和移动互联网支付领域,SET协议起着至关重要的作用。它通过对用户、商家、支付网关、收单行、发卡行关系的合理处理,为整个网络支付过程提供了安全、可靠的保障。但是,SET协议自身由于设计时代的局限,存在一定的效率和应用障碍的问题。文中对SET协议在移动支付中的安全性进行了研究,在保证原SET协议安全性的基础上,提出了一个改进方案。该方案的最大特点在于,通过将动态口令技术应用于SET协议的流程中,改进了SET协议的执行状况。通过分析,改进后的方案不仅是安全的,同时也是高效的,从而更好地保证了网上支付的安全性。     

SET协议分析及其改进

电子商务是目前经济发展的巨大推动力之一.而安全协议是电子商务发展能否取得长足发展的决定性因素.安全电子交易协议SET协议是目前电子商务系统中一种安全性比较高的协议.但是在交易的便捷性和交易纠纷处理方面还有一定的缺陷.在对SET协议流程进行分析的基础上,提出相应的改进措施,弥补了其在便捷性和交易纠纷处理方面的缺陷.     

一个公平、有效的安全电子交易协议

SET（安全电子交易）协议是由MasterCard和VISA制定的，基于信用卡的安全支付协议。在SET协议基础上提出了一种有效公平的安全电子交易协议（SET－1），该协议不仅保持了SET原有安全和有效的特性，而且实现了交易有效证据的生成和保存，从而保证了交易的公平性，同时还引入交易状态机制。最后，讨论该协议的安全性、有效性和公平性。     

椭圆曲线密码体制在SET协议中的应用

分析了电子商务中SET协议的运作方式,针对SET交易每个阶段要用加密和数字签名保证其安全进行的要求,设计了一套椭圆曲线密码体制在SET协议中的应用方案,其中包括ECC的密钥生成、数字签名和数字信封的实现算法。给出了一个SET交易的安全实现模型,它保证了交易的有效性、机密性、完整性和不可抵赖性。