协议形式化开发环境的规范语言

LOTOS（languageoftemporalorderingspecification）是一种基于进程代数CCS的协议规范语言，面向协议验证，但它不能描述协议的某些性质．本文提出了一种LOTOS的扩充语言ELOTOS（extendedLOTOS），它在LOTOS的基础上引入了异步通讯机制、时间描述、事件发生的随机性描述．

安全协议形式化分析研究

计算机网络中,安全协议为通信双方的信息交互提供安全保证,是计算机网络安全的基础.而当安全协议中存在安全漏洞时,会对信息安全产生重大威胁,造成数据泄露、身份被冒用等危害.因此,对于安全协议安全性的研究,历来都属于安全领域的重要研究方向.目前的安全性分析方法主要是通过协议形式化分析与验证来实现.形式化分析方法的理论体系大致可分为三类:模态逻辑技术、模型检测技术和定理证明技术.在不同类别的理论体系中,所使用的技术方法各有不同,对安全协议分析的侧重点也略有不同.对于每一种理论体系,研究者们也提出了不同的方法,以及针对经典方案的改进来提高形式化分析的准确性.对于复合协议,其主要问题是通过对多种现有可靠安全协议加以组合,构成新的协议并保持其安全性可靠.对于复合协议的安全性分析,也有异于普通的安全协议形式化分析.本文总结了各种类别中的主要分析方法,并比较了每种方法的优缺点,同时特别针对复合协议的安全性分析技术进行了概述.最后指出了形式化分析方法中需要解决的问题,以及下一步的研究方向.

基于FSM的协议形式化技术研究

本文主要讨论基于有限状态机(FSM)的协议形式化技术问题。文中论述了FSM形式描述与验证的技术特征,提出了一种增强FSM形式化方法,并给出了基于该方法的形式描述与验证的协议实例。

CSP和RSL应用于协议形式化描述的研究

文中用一种新的形式化描述语言RSL来描述网络协议,采用通信顺序进程CSP为模型。该模型基于进程代数,能用严密的代数演算方法验证协议性质。文中对CSP模型和RSL语言作了时间的扩充,并且给出了从CSP模型到RSL语言的转换步骤及规则。最后给出了一个TFTP的实例来说明RSL语言在协议描述上的适用性。

受限环境下委托握手DTLS协议的形式化分析与改进

物联网设备有着资源受限的特性,往往处于受限的网络环境中,在这之上又面临着安全的挑战。目前常见的受限网络协议栈为CoAP-DTLS/UDP-6LoWPAN,传输层使用UDP,其安全性由DTLS协议维持。但DTLS协议作为TLS在UDP上的扩展,基于PKI连接建立的方式使其在直接应用到受限环境下会产生诸多性能上的问题。针对DTLS协议在受限环境下的性能问题,国内外的研究学者提出了诸多解决方式,包括但不限于改进加密算法、使用特定硬件、优化证书链、委托可信三方进行密钥协商(即将DTLS握手委托给第三方)。因此,对委托握手的DTLS协议使用Scyther进行形式化分析,得出其交付密钥材料时使用长期预共享密钥存在的安全问题,并提出重用TLS/DTLS协议中PRF函数的改进方式,对改进后的方法进行分析,证明了该方法能有效降低交付密钥材料时存在的风险。

Casper/FDR和串空间在物联网通信协议中的形式化分析

通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析:用Casper/FDR对协议的有穷状态进行穷举验证,当发现协议漏洞时会自动给出攻击的迹,但是此方法会产生状态爆炸的问题;串空间方法正好可以解决状态爆炸问题,用串空间对协议的各种状态进行证明,但是如果发现了协议漏洞,该方法不能给出攻击者的迹。

通信协议测试的形式化技术

自然语言协议的自动形式化是通信协议自动测试的前提,从而也是数据链协议自动测试的重要研究方向。此问题出现已久,但尚无可靠解决方案。隐词形理论和格语法是排岐能力很强的自然语言处理方法。运用此套方法。通过分析协议文本,确定隐词形特征,可编写出隐词形词典、隐词形语法规则以及自动机生成规则。根据这些词典、规则,可生成自然语言协议文本对应的自动机。本方案有助于解决自然语言协议文本自动形式化,实现通信协议测试的全面自动化。

基于标号有限状态机的协议形式描述与验证

本文论述了协议的形式描述与验证的主要技术,讨论了基于标号有限状态机的形式描述与验证问题,给出了应用实例。

一种具有前向安全的TLS协议0-RTT握手方案

针对传输层安全(TLS)协议1.3版本在握手消息的第1个flight中传输应用数据的0-RTT握手方案,传输的早期数据由于不存在身份认证,容易遭受重放、伪造以及中间人的攻击,并且不满足前向安全的问题,提出一种具有前向安全的0-RTT优化握手方案,使用Tamarin安全协议形式化分析工具对改进前、后的协议进行形式化验证,结果表明:改进方案的早期数据在原方案之上具有了前向保密的安全性质。

认证测试方法对X.509认证协议的分析

采用认证测试方法对X.509协议的认证正确性进行了分析,该方法比BAN逻辑分析得到的结论更具体,比传统串空间理论构造集合寻找M-minimal元素的方法更为简单直观。然后针对分析结论提出了改进协议,并使用认证测试方法证明了改进协议在保持数据保密性完整性的同时,也能实现认证的正确性。

两个认证密钥协商协议的前向安全性分析

目前,网络安全及隐私受到广泛关注。前向安全性是Günther在1989年提出的一种认证密钥协商协议(AKA)的安全属性(doi:10.1007/3-540-46885-4_5),该性质经过30年的蓬勃发展已经成为研究领域的热点之一。该文主要分析了MZK20和VSR20两个AKA协议。首先在启发式分析的基础上,利用BAN逻辑分析了MZK20协议不具有弱前向安全性;其次利用启发式分析和Scyther工具证明了VSR20协议不具备前向安全性。最后,在分析VSR20协议设计缺陷的基础上,提出了改进方案,并在eCK模型下证明了改进后协议的安全性;并且,结合Scyther软件证明了改进VSR20协议与VSR20协议相比明显提高了安全性。

认证协议的有向图模型及其安全性分析

认证协议的形式化描述及其安全性分析是安全协议形式化分析的关键问题之一.为了解决以往分析方法中协议规范形式化描述存在的问题,提出了一种协议规范有向图描述方法,并在此基础上提出了协议消息构造的逆向搜索算法.用该算法分析Woo-Lam认证协议,找到了该协议一种新的攻击方法及其攻击路径.

用BAN逻辑方法分析TLS协议

密码协议的形式化正在成为国际上研究的热点,通过形式化分析密码协议来判断密码协议是否安全可靠。BAN逻辑是最早提出、最为重要的一种安全协议分析方法,被广泛地用于密码协议的安全性证明。文章介绍了BAN逻辑和TLS协议,用BAN逻辑分析TLS协议,从而证明TLS协议的双方认证协议是完整的、没有漏洞的。

SDL在空间通信协议开发中的应用

针对空间通信协议开发难度大、代价大的问题,提出了基于协议工程思想利用SDL(规范与描述语言)对SCPS-TP(空间通信协议规范-传输协议)进行开发的方法,包括SDL建模、仿真和验证。首先对SCPS-TP进行了功能分析,确定功能点和状态机,并据此利用SDL建模;接着对模型进行实时仿真,测试其正确性,通过调试保证所有功能通过仿真;最后对模型进行了验证。验证结果表明,SCPS-TP不存在死锁、活锁等逻辑错误,为其在空间通信中的应用提供了有力支持,同时也说明了SDL在空间通信协议开发中的重要应用。

基于第三方的安全移动支付方案

在现有移动支付方案研究的基础上,提出一种新的基于第三方的安全移动支付方案。该方案以第三方支付平台为基础,在交易过程中采用"一次一密"的密钥分配机制,改善了现有移动支付方案的缺陷,在安全性上实现交易信息的保密性、不可伪造性及不可否认性等特性,并利用串空间模型的形式化分析方法对相关协议进行安全性证明。

无线局域网WPS安全性分析

介绍了Wi-Fi联盟的WPS标准并给出了对应的攻击方法——暴力破解攻击,使用CPN对WPS协议及改进协议进行形式化分析并证明AP限制重新发起连接认证的次数为3次时,原协议可完全被攻破而给出的改进协议成功概率仅约为3/108。

通用Web跨域认证构架研究与实现

分析了目前主要的Web跨域认证技术特点和不足,设计了一种新的基于URL重定向的Web跨域认证构架,给出了典型协议实现并进行了安全性分析。它对信息系统改动极少,且不易受NAT网关和防火墙的限制,具有良好的应用前景。