ANODR匿名路由协议的安全性验证

匿名路由协议的目的是保证移动自主网中节点在通信时不会泄露参与通信的节点身份以及通信路径不被发现,其目标可分为发送匿名、接收匿名和路由匿名。将该协议分解为3个组件,分别实现3个目标。利用扩展后的Cord逻辑对实现路由匿名的组件进行验证,结果证明其不能满足路由匿名规范,破坏了协议作为一个整体提供的匿名服务。     

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.     

一个安全、原子的电子商务协议及其形式化验证

电子商务的普及与接受主要取决于下述属性的解决：安全、原子、隐私与匿名,形式化描述和分析是描述电子商务协议并验证它各性的有效方法,面向物理商品交易的电子商务协议需要具备３个属性：安全、原子和隐私,介绍了一个安全、可靠的电子商务协议ＢＥＡＲＣＡＴ及其形式化描述,并龙有人侵者的情况下,通过用ＢＡＮ类型的逻辑证明所期望的属性的方式对协议的强度和正确性作形式化分析。     

移动支付协议PCMS的形式化分析和验证

移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。     

Kaman协议的形式化验证

Kaman协议是移动Ad Hoc网络安全认证机制,然而,协议设计者未对该协议的安全性作严格的形式化分析。协议复合逻辑PCL是验证协议安全属性的形式化方法,PCL逻辑能够简化协议安全分析过程。本文在协议复合逻辑PCL中描述Kaman协议并分析Kaman协议的安全属性,证明Kaman协议能够实现其安全目标。     

电子商务的安全和原子：模型、协议和验证

电子商务的流行与接受主要取决于下述属性：安全、原子、隐私与匿名．对于需要安全、原子和隐私等3个属性的物理商品的电子交易还没有合适的电子商务协议．基于此,提出了一个称为ELC的电子商务模型,ELC模型模拟了国际贸易中的电子信用证．然后提出了一个安全、原子的电子商务协议．最后,在有一个入侵者的情况下,通过使用BAN风格的逻辑证明所期望的属性分析了协议的强度和正确性     

基于完整性度量的端到端可信匿名认证协议

针对目前端到端认证协议只认证平台身份,缺乏对平台可信性的验证,存在安全性的问题。通过改进的ELGamal签名方案,利用可信计算技术,提出了一种基于完整性度量的端到端可信匿名认证协议ETAAP(End-to-end Trusted Anonymous Authentication Protocol)。协议的首轮交互中实现了可信平台真实性验证,在此基础上通过IMC/IMV交互完成对平台完整性验证和平台安全属性的可信性评估,并采用通用可组合安全模型对协议的安全性进行了分析,证明协议是安全的。最后通过实验表明该协议具有较好的性能,可实现基于完整性的端到端可信匿名认证。     

一种分析电子商务安全协议的新逻辑

针对典型电子商务安全协议逻辑分析方法存在的问题,如安全属性分析存在局限性、缺乏形式化语义、对混合密码原语的处理能力不强等,提出了一种新的逻辑分析方法。新逻辑能够分析电子商务安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。以匿名电子现金支付协议ISI作为分析实例,证明了新逻辑方法的有效性。分析找出了该协议的安全漏洞和缺陷:不满足商家的非否认性、密钥保密性、可追究性、公平性以及原子性,客户面临商家恶意欺骗的潜在威胁。     

匿名通信协议MACP概率模型检验

匿名通信技术是保护互联网用户隐私的最有力手段之一,但匿名通信协议的形式化验证仍是亟待解决的难题。对P2P匿名通信协议MACP进行了形式化验证与分析,将MACP协议的匿名路径建立过程模型化为一个离散时间马尔可夫链;然后利用概率计算树逻辑PCTL描述MACP协议的匿名性质,并采用概率模型检验器对MACP协议的匿名性进行检验。检验结果表明,通过增加匿名通道数,提高了MACP协议的匿名等级和抗攻击能力;MACP协议的匿名性随着规模的增大而增强,并没有因控制匿名路径的长度而降低。     

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

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

马尔科夫逻辑网在信息安全风险管理中的应用

针对现有的企业安全风险管理中,风险处理方案的制定和管理措施的选择缺乏量化手段、手动风险分析方式耗时过长等问题,提出了一种基于马尔科夫逻辑网的信息安全风险管理方法。首先利用马尔科夫逻辑网对被评估系统组件及服务间依赖关系进行描述,进而利用马尔科夫逻辑网的边际推理模型来预估不同安全管理措施情况下的系统可用性值,从而为管理措施的选择提供了量化依据。案例研究表明,该方法能够为企业信息系统安全风险管理措施的选择提供可靠的量化依据,且方法实施简单易行。     

J2EE模式下基于角色访问控制的应用

利用J2EE基于容器的安全机制，将基于角色的访问控制（Role-Based Access Control，RBAC）融入J2EE安全之中，用RBAC来管理J2EE组件安全而不需修改各组件的代码。RBAC的实现只需通过容器部署描述符配置既可，系统运行时，容器从部署描述符中读取出相应的RBAC安全策略，然后根据安全策略执行安全验证，实现RBAC对系统资源的保护。这样，组件开发和系统安全相分离，开发人员可不关心系统安全，集中精力投入组件的业务逻辑开发，安全问题由组件组装人员、部署者和系统管理员来完成。因此，降低了对编程人员的要求和系统开发成本开发成本，也提高了系统组件的可移植性。     

Linux进程语义安全性检测的稳定模型

现有进程检测方法,检测的目标是系统调用的序列的排列关联,忽略了语义中潜在的异常。稳定模型是逻辑程序的语义模型,可以用以发现并修改逻辑程序的异常问题。该文以系统调用为基本检测点,采用逻辑程序描述进程的基本语义逻辑,用稳定模型表达进程的检测语义。系统定义进程的一系列安全语义规则,在进程执行中,计算安全语义规则与进程逻辑之间的稳定模型,得到安全语义的可计算性结论。论文最后,给出了一个Linux系统中的进程语义安全性检测的基本框架。     

可重构安全系统建模与配置生成方法研究

以安全重构元为基础,能够提供高灵活性、适应性和可扩展性安全服务的可重构安全计算系统已成为当前安全研究领域的热点问题.目前,关于重构机理的研究主要采取基于功能候选集的静态重构配置生成方法,可重构安全系统作为一种主动安全防御手段,应具有动态自动重构的能力,避免人工介入导致的脆弱性.针对动态自动可重构安全系统的建模以及配置生成过程的描述问题,提出了一种基于直觉主义逻辑扩展的动态自动可重构安全系统逻辑模型SSPE,给出了逻辑模型SSPE上的语法和推理规则,设计了基于SSPE的等级化安全重构元和安全需求建模和表达方法,并给出了基于映射关系的安全重构元描述向逻辑语言的转换规则.最后,以IPSec协议为例,阐述了可重构安全系统重构配置的动态自动推理生成过程.基于直觉主义逻辑的可重构安全系统建模和配置生成方法,为研究可重构安全系统的重构机理提供了新的思路和方法,具有重要的意义.     

A security and authentication layer for SCADA/DCS applications

Mid 2010, a sophisticated malicious computer worm called Stuxnet targeted major ICS systems around the world causing severe damages to Siemens automation products. Stuxnet proved its ability to infect air-gapped-segregated critical computers control system. After this attack, the whole ICS industry security was thrust into spotlight. Automation suppliers have already started to re-think their business approach to cyber security. The OPC foundation have made also significant changes and improvements on its new design OPC-UA to increase security of automation applications but, what is still missing and seems to be not resolved any time soon is having security in depth for industrial automation applications. In this paper, we propose a simple but strong security control solution to be implemented as a logic level security on SCADA and DCS systems. The method presented in this work enforces message integrity to build trusts between DCS system components, but it should not be viewed as the main nor the only protection layer implemented on an industrial automation system. The proposed solution can be viewed as a low-level security procedure to avoid malicious attacks such as Stuxnet.     

模型学习与符号执行结合的安全协议代码分析技术

符号执行技术从理论上可以全面分析程序执行空间,但对安全协议这样的大型程序,路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点,提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路;同时,通过将协议代码中的密码学逻辑与协议交互逻辑相分离,避免了因密码逻辑的复杂性导致路径约束无法求解的问题。在SSH协议开源项目Dropbear上的成功实践表明了所提方法的可行性;通过与 Dropbear 自带的模糊测试套件对比,验证了所提方法在代码覆盖率与错误点发现上均具有一定优势。     

源程序语义检测的稳定模型分析方法

基于逻辑程序及其稳定模型的理论，提出一种源程序语义检测的稳定模型分析方法。该方法从源程序中提取关键语句图，将安全知识规则转换为一个逻辑程序，再用关键语句图去实例化该逻辑程序，最后求解其稳定模型得到源程序的安全性评价。该方法体现了源程序丰富的语义，具有较好的可扩展性。     

用BAN逻辑方法分析TLS协议

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