Analysis and improvement of cross-realm client-to-client password authenticated key exchange protocols

Because cross-realm C2C-PAKE （client-to-client password authenticated key exchange） protocols can not resist some attacks, this paper writes up new attacks on two representative protocols, then designs a new cross-realm C2C-PAKE protocol with signature and optimal number of rounds for a client （only 2-rounds between a client and a server）. Finally, it is proved that the new protocol can be resistant to all known attacks through heuristic analysis and that it brings more security through the comparisons of security properties with other protocols.     

A protocol for fair electronic purchase based on concurrent signatures

E-commerce protocols for the electronic purchase of goods are difficult to design and implement due to their complexity and high security demands. Fairness of such protocols in literature highly depends on an additional TTP（trusted third party）. However, it is difficult to find such a TTP in some situations. In addition, fairness for customers has been neither fully considered nor well satisfied in existing electronic purchasing protocols. In this paper, a new protocol FEP （fair electronic purchase） without a special TTP but an online bank is presented based on a concurrent digital signature scheme. The FEP protocol guarantees fair electronic purchase of goods via electronic payment between consumers, merchants and their online banks. The protocol is practical and the analysis based on the game logics shows that it achieves the properties of viability, fairness, and timeliness.     

A New Watermarking Protocol against Conspiracy

A trusted third party introduced in watermarking protocols would decrease the security and affect the implementation of the protocols. In this paper, a new watermarking protocol with an un-trusted third party （UTTP） was proposed. Based on the idea of all-or-nothing disclosure of secret （ANDOS）, all of the buyer, the seller and the third party didn＇t know the exact watermark, which was embedded in a digital content for tracing piracy. The proposed protocol provided mechanisms to trace piracy and protect customer＇s right. In addition, the problem that a seller colluded with UTTP to frame the buyer, namely, the conspiracy problem, could be avoided.     

分析和设计安全协议的新逻辑的语义

文献[1]中提出了一种分析和设计安全协议的新逻辑.协议分析者可以用该逻辑来对安全协议进行分析,而协议设计者可以使用该逻辑用一种系统的方法来构造安全协议.文献[1]没有给出该逻辑的形式化语义,因为串空间模型具有良好的语义,现将新逻辑和串空间模型结合起来,给出新逻辑的串空间语义,并运用该语义证明了新逻辑的推理规则是正确的.     

Formal analysis on an extended security model for database systems

In order to develop highly secure database systems to meet the requirements for class B2, the BLP （Bell-LaPudula） model is extended according to the features of database systems. A method for verifying security model for database systems is pro- posed. According to this method, an analysis by using Coq proof assistant to ensure the correctness and security of the extended model is introduced. Our formal security model has been verified secure. This work demonstrates that our verification method is effective and sufficient.     

安全协议抗DoS攻击的形式化分析研究

随着拒绝服务攻击给协议的可用性带来的危害越来越大,需要行之有效的方法对安全协议的抗DoS性进行分析.但是目前对安全协议的抗DoS性进行分析的方法模型都存在一些缺陷,有的只能分析部分的DoS攻击,有的只关注协议各方计算资源的消耗,而忽略了存储资源消耗.针对以上不足,本文对基本的串空间模型进行扩展,引入消息相关度集合和代价函数,提出了一种分析安全协议抗DoS性的新方法,并利用该方法,对JFK协议的抗DoS性进行了详细分析.     

Breaking and repairing the certificateless key agreement protocol from ASIAN 2006

The certificateless authenticated key agreement protocol proposed by Mandt et al does not haVE the property of key-compromise impersonation （K-CI） resilience. An improved protocol with a simple modification of their protocol is proposed in this paper. In particular, our improved protocol is proved to be immune to the K-CI attack and at the same time possess other security properties.     

MANET路由协议的正确性分析

移动自组网(MANET)是当前网络研究的一个热点,但是由于安全问题致使其未能广泛应用.在安全问题中,路由协议的正确性尤为重要.采用形式验证方法分析了MANET非安全路由协议和安全路由协议的正确性.首先给出了协议正确性的形式描述以及攻击者的形式定义,将协议的正确性分为安全性(Safety property)和活性(Liveness property),前者指协议所发现的路由具有某些良好的性质,后者指协议能够发现路由而且能够顺利地传输数据;然后提出了两个活性证明规则--响应性证明规则和反应性证明规则,并用所提出的活性证明规则在Isabelle/HOL中证明了DSR协议和SRP协议的正确性.     

一种安全协议的形式化验证方法

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的安全协议。介绍BAN逻辑的产生、成分和分析步骤，指出BAN逻辑的缺陷，由此而产生的改进BAN逻辑和现状，并对BAN类逻辑作全面的回顾与展望，得出：BAN类逻辑仍然是密码协议分析和设计的主要工具，但理想化步骤是BAN类逻辑的致命缺陷的结论。展望了BAN类逻辑研究。对未来协议的形式化分析工作具有指导意义。     

BAN类逻辑的由来与发展

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的密码协议。该文介绍了 BAN逻辑的产生、成分和分析步骤 ,进而全面指出了 BAN逻辑的缺陷 ,由此而产生的改进的 BAN逻辑和现状 ,从而对 BAN类逻辑作了全面的回顾与展望 ,并得出结论 :BAN类逻辑仍然是密码协议分析和设计的主要工具 ,但理想化步骤是 BAN类逻辑的致命缺陷。指出了 BAN类逻辑研究工作的展望。这些结论对未来协议的形式化分析工作具有指导意义     

用串空间分析路由协议SGSR

用形式化方法分析安全协议是协议分析的有效手段,近年来,出现了众多的研究方法.串空间模型是一种新兴的形式化分析工具,其中,"理想"和"诚实"两个概念简化了分析协议的步骤.首次利用串空间理论对由徐兰芳提出的一种安全的Ad Hoc网络路由协议SGSR进行分析,并分析了它的认证性和机密性,结果证明此协议能够达到协议的目标。     

Analysis and Application of Covert Channels of Internet Control Message Protocol

Based on the analysis of the covert channel＇s working mechanism of the internet control message protocol （ICMP） in internet protocol version 4 （IPv4） and Internet Protocol version 6 （IPv6）, the ICMP covert channd＇s algorithms of the IPv4 and IPv6 are presented, which enable automatic channeling upon IPv4/v6 nodes with non-IPv4-compatible address, and the key transmission is achieved by using this channel in the embedded Internet terminal. The result shows that the covert channel＇s algorithm, which we implemented if, set correct, the messages of this covert channel might go through the gateway and enter the local area network.     

A Scalable Intrusion Detection System for IPv6

0 IntroductionIPv6 ,as a new, widely available version of Internet proto-col , contains numerous features that make it attractivefroma securitystandpoint[1].IPv6is not a panaceafor securi-ty,though, because the basic mechanisms for transportingpackets across the network stay mostly unchanged,and theupper-layer protocols that transport the actual application dataare mostly unaffected.IPv6 is usually deployed without cryp-tographic protections of any kind in real environment[2].So,IPv6 securi…     

多播水印协议MAMWP的BAN逻辑分析

 用形式化的方法分析密码协议可以检测出协议中的漏洞和证明协议的安全性,BAN类逻辑是目前使用最广泛的一种形式化分析密码协议的方法.文章介绍了基于移动代理的多播水印协议MAMWP和BAN逻辑,并给出了用BAN逻辑分析MAMWP协议的详细过程.     

A Lightweight Mobile RSVP for Unicast

This paper presents a lighter protocol, and it removes the multicast burdens from RSVP to adapt to unicast applications. At the same time, when RSVP is used in wireless networks, some issues about mobility raise popular concerns. The proposed protocol a lightweight mobile RSVP protocol, solves the problems by the following mechanisms： changeless flow identifier, a new state management and ＂refresh＂ mechanism.     

Fault Tolerant Approach for Data Encryption and Digital Signature Based on ECC System

An integrated fault tolerant approach for data encryption and digital signature based on elliptic curve cryptography is proposed. This approach allows the receiver to verify the sender‘s identity and can simultaneously deal with error detection and data correction. Up to three errors in our approach can be detected and corrected. This approach has atleast the same security as that based on RSA system, but smaller keys to achieve the same level of security. Our approach is more efficient than the known ones and more suited for limited environments like personal digital assistants (PDAs), mobile phones and smart cards without RSA coprocessors.     

A Novel Digital Audio Watermarking Scheme in the Wavelet Domain

We present a novel quantization-based digital audio watermarking scheme in wavelet domain. By quantizing a host audio‘s wavelet coefficients (Integer Lifting Wavelet Transform ) and utilizing the characteristics of human auditory system ( HAS), the gray image is embedded using our watermarking method. Experimental results show that the proposed watermarking scheme is inaudible and robust against various signal processing such as noising adding, lossy compression, low pass filtering, re-sampling, and re-quantifying.     

A New ID-Based Proxy Multi-Signature Scheme from Bilinear Pairings

ID-based public key cryptosystem can be a good alternative for certifieate-based public key setting. This paper provides an efficient ID-based proxy multi signature scheme from pairings. In the random oracle model, we prove that our new scheme is secure against existential delegation forgery with the assumption that Hess＇s scheme-1 is existential unforgeable, and that our new scheme is secure against existential proxy multi-signature forgery under the hardness assumption of the computational Diffie-Hellman problem.     

An Image Encryption Method Based on Bit Plane Hiding Technology

A novel image hiding method based on the correlation analysis of bit plane is described in this paper. Firstly, based on the correlation analysis, different bit plane of a secret image is hided in different bit plane of several different open images. And then a new hiding image is acquired by a nesting ＂Exclusive-OR＂ operation on those images obtained from the first step. At last, by employing image fusion technique, the final hiding result is achieved. The experimental result shows that the method proposed in this paper is effec rive.