网络支付协议的形式化安全需求及验证逻辑

从整个网络支付协议的安全角度出发，提出网络支付协议的多层安全需求模型，包括以认证和密钥分配为基础的基层需求、网络支付协议固有的中层需求(包括保密性、原子性、公平性、完整性、匿名性、不可否认性、可追究性等)、以及面向具体应用的高层需求。基于一阶逻辑和时序逻辑，提出一种适合描述网络支付协议的形式化安全需求的逻辑，描述了该逻辑的语法结构和推理规则，并用该安全需求逻辑对网络支付协议的多层安全需求进行了形式化描述。最后，以SET协议为例进行需求验证。     

An approach to sequential circuit diagnosis based on formal verification techniques

This article deals with the generation of exact diagnostic trees for real-size synchronous sequential circuits. Starting from existing detection-oriented test patterns, a modified fault simulator is used for assessing their diagnostic power, which, in general, is not satisfactory. A diagnostic procedure for improving it is described that successfully exploits symbolic FSM equivalence proof algorithms. In order to resort to costly techniques, such as product machine traversal, only when really needed, special checks are performed to verify combinational identity and identity on reachable states. As all faults are attributed to theirequivalence class, a complete and exact diagnostic tree can be built. Experimental results on ISCAS'89 circuits show the feasibility of the approach and support the claim that, for the first time, diagnosing real-world synchronous sequential circuits has become feasible.     

SoC interconnection protection through formal verification

The wide adoption of third-party hardware Intellectual Property (IP) cores including those from untrusted vendors have raised security concerns for system designers and end-users. Existing approaches to ensure the trustworthiness of individual IPs rarely consider the entire SoC design, especially the IP interactions through SoC bus. These methods can hardly identify malicious logic (or design flaws) distributed in multiple IPs whereas individual IPs fulfill security properties and can pass the security testing/verification. One possible solution is to treat the SoC as one IP core and try to verify security properties of the entire design. This method, however, suffers from scalability issues due to the large size of SoC designs with multiple IP cores integrated. In this paper, we present a scalable SoC bus verification framework trying to verify the security properties of SoC bus implementation where the bus protocol plays the role of the golden reference. More specifically, finite state machine (FSM) models will be constructed from the bus implementation and the trustworthiness will be verified based on the property set derived from the bus protocol and potential security threats. Along with IP level formal verification solutions, the proposed framework can help ensure the security of large-scale SoCs. Experimental results on ARM AMBA Bus demonstrate that our approach is applicable and scalable to prevent information leakage and denial-of-service (DoS) attack by verifying security properties.     

基于SAT的安全协议惰性形式化分析方法

提出了一种基于布尔可满足性问题的安全协议形式化分析方法SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率。另一方面,通过在消息类型上定义偏序关系,SAT-LMC能够检测出更丰富的类型缺陷攻击。基于此方法实现了一个安全协议分析工具,针对Otway-Rees协议检测出了一种类型缺陷攻击;针对OAuth2.0协议,检测结果显示对现实中存在的一些应用场景,存在一种利用授权码截取的中间人攻击。     

A lightweight and secure NFC‐base mobile payment protocol ensuring fair exchange based on a hybrid encryption algorithm with formal verification

During the past few years, many near‐field communication (NFC) mobile payment protocols have been widely used and received more and more attentions. This could be an essential factor for the growth of the world economy and leads to the improvement of the quality of life for human beings. The NFC mobile payment is one prominent approach in allowing m‐commerce to conduct a sales transaction. However, fair exchange and information security are significant concerns in creating trust among the parties participating in the transaction. Many NFC mobile payment protocols have been introduced by researchers. But, most of them still lack some crucial properties of information security and fair exchange, and this can be an obstacle to their uses. In this article, we propose an NFC mobile payment protocol that possesses comprehensive properties of both information security and fair exchange for sales transaction processing. The protocol employs both symmetric and asymmetric encryptions, hash function, and the technique of offline session key generation, in order to improve the security while maintaining the lightweight property. The fairness analysis shows that the proposed protocol is more competent and effective than others. It can resolve any dispute in case one party misbehaves. Finally, the proposed protocol's security has been successfully verified using both Burrows, Abadi and Needham (BAN logic) and the Scyther tool.     

家庭网络技术及相关协议

家庭网络技术是当前信息应用领域发展最为迅速的领域之一.罗列了目前8大典型的家庭网络联盟及主要研究状况,并列出了家庭网络核心技术--家庭网关的三类产品,最后提出了基于NGN的家庭网关的框架图.     

自动信任协商的形式化描述与验证研究

首先提出了自动信任协商的通用形式化框架,并将典型的信任协商策略规约到上述框架内;其次,基于上述形式化框架对自动信任协商的形式化验证问题进行了定义,确定了形式化验证的目标以及一般流程;再次,研究了典型信任协商策略的形式化验证问题,讨论了相关问题的计算复杂性并得到系列结论;最后,利用逻辑编程方法和模型检测方法实现了自动信任协商的形式化验证。实验结果表明,规则数是影响形式化验证系统运行时间的关键因素,逻辑编程方法和模型检测方法在规则较少时效率较高,但逻辑编程方法的可扩展性不及模型检测方法。     

通信顺序进程的扩充及其在协议形式化技术中的应用

讨论了为进行协议形式化描述而进行的CSP扩充问题。向CSP中引入了可终止进程的概念，并给出了可终止进程的判定方法：针对CSP只能进行同步通信描述的缺陷，提出了用CSP来描述异步通信的手段：最后给出了AB协议的CSP描述，并在此基础上初步讨论了协议规范的正确性及测试用例的生成。     

浅谈加密技术的方法及应用

当今在互联网上进行文件传输、电子邮件商务往来存在许多不安全因素。特别是对于一些大公司和一些机密文件在网络上传输，只好选择了数据加密和基于加密技术的数字签名。加密在网络上的作用就是防止有用或私有化信息在网络上被拦截和窃取。     

Enhanced protocols for hierarchical encryption key management forsecure communication in internet environments

Two enhancements to a recently published hierarchical encryption key management protocol for end-to-end secure communication in internet environments are outlined. The first one concerns a more reliable authentication of the principals which can be realized by a modification of the message structures being exchanged, while the second one concerns a modified protocol that permits the implementation of the hierarchical key management approach in the widely employed TCP/IP-based network interconnections     

On automating the verification of secure ad-hoc network routing protocols

Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for ad-hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a fully automatic verification method for secure ad-hoc network routing protocols that helps increasing the confidence in a protocol by providing an analysis framework that is more systematic, and hence, less error-prone than the informal analysis. Our method is based on a deductive proof technique and a backward reachability approach. The main novelty of this approach compared to the prior works is that beside providing expressive semantics and syntax for modelling and specifying secure routing protocols, it assumes an arbitrary topology, and a strong attacker model.     

Toward efficient protocol design through protocol profiling and performance assessment: using formal verification in a different context

The most common use of formal verification methods so far has been in identifying whether livelock and/or deadlock situations can occur during protocol execution, process, or system operation. In this work, we aim to show that an additional equally important and useful application of formal verification methods can be in protocol design in terms of performance‐related metrics. This can be achieved by using the methods in a rather different context compared with their traditional use, that is, not only as model checking tools to assess the correctness of a protocol in terms of lack of livelock and deadlock situations but rather as tools capable of building profiles of protocol operations, assessing their performance, and identifying operational patterns and possible bottleneck operations. This process can provide protocol designers with an insight about the protocols’ behavior and guide them toward further optimizations. It can also assist network operators and service providers to assess the protocols’ relative performance and select the most suitable protocol for specific deployment scenarios. We illustrate these principles by showing how formal verification tools can be applied in this protocol profiling and performance assessment context using some existing protocol implementations in mobile and wireless environments as case studies. Copyright © 2011 John Wiley & Sons, Ltd.     

智能化电视网络安全协议的验证方法综述

在有线电视网络领域,安全的网络通信协议是安全的信息传输的保障,那么研究出有效的协议安全性验证方法显得至关重要。当前,随着互联网的普及数字电视的双向化、智能化趋势日益明显,处于互联网中的数字电视将面临严峻的信息安全威胁,必须通过通信协议的安全性验证法选择出安全性更高的通信协议,才能确保双向数字电视传输网络的安全性。目前,关于验证通信协议的方法主要分为逻辑推理分析法、模型模拟检测法、定理归纳证明法以及其它衍生验证法。本文在前期研究的基础上,对近五年提出的典型的协议验证方法进行总结比较,分析各验证方法的优缺点。最后,对协议验证领域存在的问题及未来的发展趋势做以阐述。     

Security architectures using formal methods

A model describing secure communications architectures is developed using the formal language Z. The model is based on fundamental cryptographic properties. Some basic constraints are derived for the design of secure architectures which allow problems to be identified prior to the design of security protocols. A simple criterion is derived for ensuring that all pairs of users can set up secure communications channels     

Privacy‐preserving authentication protocols with efficient verification in VANETs

As an important component of intelligent transportation systems, vehicular ad hoc networks can provide safer and more comfortable driving circumstance for the drivers. However, communication security and privacy issues present practical concerns to the deployment of vehicular ad hoc networks. Although recent related studies have already addressed most of these issues, most of them have only considered a posteriori countermeasures or a priori countermeasures to prevent the attacks of an adversary. To the best of our knowledge, up to now, only two privacy‐preserving authentication schemes can provide a posteriori countermeasures and a priori countermeasures. But, the computational cost of verifying a signature is relatively high or security proof of the scheme is loose in the two schemes. In this paper, we propose two novel privacy‐preserving authentication schemes. The first one cannot only provide a posteriori and a priori countermeasures, but also has low computational cost in the verification phase and tight security proof. The second one can achieve batch verification on multiple messages. Comparison with Wu et al.'s scheme and Chen et al's scheme, our scheme shows higher efficiency in terms of the computational cost of verifying signature.Copyright © 2013 John Wiley & Sons, Ltd.     

Automated verification of a key management architecture for hierarchical group protocols

Emerging applications require secure group communications involving hierarchical architecture protocols. Designing such secure hierarchical protocols is not straightforward, and their verification becomes a major issue in order to avoid any possible security attack and vulnerability. Several attempts have been made to deal with formal verification of group protocols, but to our knowledge, none of them did address the security of hierarchical ones. In this paper, we present the specific challenges and security issues of hierarchical secure group communications, and the work we did for their verification. We show how the AtSe back-end of the avispa tool was used to verify one of these protocols.     

SSMCI:verification mechanism for security protocols centered on the attacker

A automatic verification mechanism for security protocols analysis was proposed.The attacker model was proposed and the concept of ‘need’ was defined,a knowledge set which was necessary for the attacker to compose a target message term but unknown to the attacker.The attacker model was established as needed.The mechanism centered on the attacker was designed,in which whether add a protocol session was determined by the attacker.This might cause contradiction in time sequence,so some back-track algorithm was adopted to solve this contradiction.Experiments show that the system can verify the security of the protocol,and the number of state space is slightly better than the Scyther tool.