计算可靠且高效的群组密钥协商协议符号化分析方法

符号化分析方法将密码原语视为黑盒,且未研究其需要满足的具体安全属性,因而计算可靠性一直备受质疑.而且,这类方法在分析参与者数目较多的群组密钥协商协议时不具有高效性.针对上述两个问题,文中提出了一种计算可靠且高效的群组密钥协商协议符号化分析方法.该方法通过为符号化表达式设计一个Pattern函数,定义了模幂运算需要满足的具体安全属性,并基于此证明了符号化分析Burmester-Desmedt协议在通用可组合安全框架下是计算可靠的.进而通过数学归纳法,证明了Burmester-Desmedt协议的安全性与参与者数目无关,避免了参与者数目对符号化分析造成的影响,提高了符号化分析方法的效率.     

基于刚性与相似性概念的密码协议分析方法

如何融合计算密码学与形式演算模型两条途径以有效分析和证明复杂密码协议,是信息安全领域富有挑战性的问题之一.文中提出Dolev-Yao刚性和Dolev-Yao相似性概念,运用密码协议的语法骨架提取与语义赋值技术,建立起一个能涵盖除具有适应性入侵能力之外的任何主动攻击者和大部分有实际意义的非自由消息代数的理论分析框架.该框架内所证明的协议安全性质具有复合一稳定性,即所证明的安全性质在协议与环境复合时仍然保持成立.文中针对strand一图模型这一具体情形证明了Canetti的UC-相似性概念与这里所建立的Dolev-Yao相似性概念之间接近充分必要程度的对偶关系,从而对融合UC-理论/strand-图模型这一情形具体证明了该分析框架具有相容性和完备性.最后,根据以上理论结果讨论了如何建立一种对应的新的协议分析方法.     

群组密钥协商协议的安全性分析方法研究

群组密钥协商允许多个用户通过不安全的信道建立一个共享的会话密钥,设计安全的群组密钥协商协议是最基本的密码学任务之一。介绍了群组密钥协商协议的两类安全性分析方法:计算复杂性方法和形式化分析方法,详细讨论了计算复杂性方法中的关键技术,包括基于规约的证明技术及基于模拟的证明技术、基于规约的安全模型和基于模拟的安全模型,探讨了安全性分析方法的发展趋势。     

Relating symbolic and cryptographic secrecy

We investigate the relation between symbolic and cryptographic secrecy properties for cryptographic protocols. Symbolic secrecy of payload messages or exchanged keys is arguably the most important notion of secrecy shown with automated proof tools. It means that an adversary restricted to symbolic operations on terms can never get the entire considered object into its knowledge set. Cryptographic secrecy essentially means computational indistinguishability between the real object and a random one, given the view of a much more general adversary. In spite of recent advances in linking symbolic and computational models of cryptography, no relation for secrecy under active attacks is known yet. For exchanged keys, we show that a certain strict symbolic secrecy definition over a specific Dolev-Yao-style cryptographic library implies cryptographic key secrecy for a real implementation of this cryptographic library. For payload messages, we present the first general cryptographic secrecy definition for a reactive scenario. The main challenge is to separate secrecy violations by the protocol under consideration from secrecy violations by the protocol users in a general way. For this definition, we show a general secrecy preservation theorem under reactive simulatability, the cryptographic notion of secure implementation. This theorem is of independent cryptographic interest. We then show that symbolic secrecy implies cryptographic payload secrecy for the same cryptographic library as used in key secrecy. Our results thus enable formal proof techniques to establish cryptographically sound proofs of secrecy for payload messages and exchanged keys.     

One-round identity-based key exchange with Perfect Forward Security

Identity-based authenticated key exchange (IBAKE) protocol is one of the most important cryptographic primitives that enables two parties using their identities to establish their common secret keys without sending and verifying public key certificates. Recently, many works have been dedicated to design efficient and secure IBAKE protocols without bilinear pairings which need the heavy computational cost. Unfortunately, most of the proposed protocols cannot provide Perfect Forward Security (PFS) which is a major security goal of authenticated key exchange protocols. In this paper we present an efficient and provably secure IBAKE protocol with PFS. Our protocol relies on the technique known as the concatenated Schnorr signature and it could be viewed as a variant of the protocol proposed by Fiore et al. in 2010. By using the Canetti–Krawczyk security model, we prove that the protocol is secure with PFS under the Computational Diffie–Hellman assumption in the random oracle model. The protocol is of interest since it offers a remarkable combination of advanced security properties and efficiency and its security proof is succinct and intelligible.     

Design of a new efficient and secure multi-secret images sharing scheme

We propose a new (n,n) multi-secret images sharing scheme that provides high level of provable security with fast sharing and reconstruction procedures. It uses simple Boolean operations conjointly with a secure stream cipher and a cryptographic hash function in order to enable an efficient sharing of n secret images among a set of n different participants. This approach overcomes the security weakness detected in existing similar schemes, and provides additional advantages such as high sensitivity to alterations and ability to share heterogeneous images having diverse resolutions. Obtained experimental results show the effectiveness and robustness of the method compared to existing schemes, particularly its ability to ensure higher security level with competitive computational performances.     

Semantic relation based personalized ranking approach for engineering document retrieval

Since engineering design is heavily informational, engineers want to retrieve existing engineering documents accurately during the product development process. However, engineers have difficulties searching for documents because of low retrieval accuracy. One of the reasons for this is the limitation of existing document ranking approaches, in which relationships between terms in documents are not considered to assess the relevance of the retrieved documents. Therefore, we propose a new ranking approach that provides more correct evaluation of document relevance to a given query. Our approach exploits domain ontology to consider relationships among terms in the relevance scoring process. Based on domain ontology, the semantics of a document are represented by a graph (called Document Semantic Network) and, then, proposed relation-based weighting schemes are used to evaluate the graph to calculate the document relevance score. In our ranking approach, user interests and searching intent are also considered in order to provide personalized services. The experimental results show that the proposed approach outperforms existing ranking approaches. A precisely represented semantics of a document as a graph and multiple relation-based weighting schemes are important factors underlying the notable improvement.     

User-friendly and certificate-free grid security infrastructure

Certificate-based public key infrastructures are currently widely used in computational grids to support security services. From a user’s perspective, however, certificate acquisition is time-consuming and public/private key management is non-trivial. In this paper, we propose a security infrastructure for grid applications, in which users are authenticated using passwords. Our infrastructure allows a user to perform single sign-on based only on a password, without requiring a public key infrastructure. Moreover, hosting servers in our infrastructure are not required to have public key certificates. Nevertheless, our infrastructure supports essential grid security services, such as mutual authentication and delegation, using public key cryptographic techniques without incurring significant additional overheads in comparison with existing approaches.     

Towards scalable synthesis of stochastic control systems

Formal synthesis approaches over stochastic systems have received significant attention in the past few years, in view of their ability to provide provably correct controllers for complex logical specifications in an automated fashion. Examples of complex specifications include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. A general methodology to synthesize controllers for such properties resorts to symbolic models of the given stochastic systems. Symbolic models are finite abstractions of the given concrete systems with the property that a controller designed on the abstraction can be refined (or implemented) into a controller on the original system. Although the recent development of techniques for the construction of symbolic models has been quite encouraging, the general goal of formal synthesis over stochastic control systems is by no means solved. A fundamental issue with the existing techniques is the known “curse of dimensionality,” which is due to the need to discretize state and input sets. Such discretization generally results in an exponential complexity over the number of state and input variables in the concrete system. In this work we propose a novel abstraction technique for incrementally stable stochastic control systems, which does not require state-space discretization but only input set discretization, and that can be potentially more efficient (and thus scalable) than existing approaches. We elucidate the effectiveness of the proposed approach by synthesizing a schedule for the coordination of two traffic lights under some safety and fairness requirements for a road traffic model. Further we argue that this 5-dimensional linear stochastic control system cannot be studied with existing approaches based on state-space discretization due to the very large number of generated discrete states.     

VCSE: Verifiable conjunctive keywords search over encrypted data without secure-channel

Data outsourcing service has gained remarkable popularity with considerable amount of enterprises and individuals, as it can relief heavy computation and management burden locally. While in most existing models, honest-but-curious cloud service provider (CSP) may return incorrect results and inevitably give rise to serious security breaches, thus the results verification mechanism should be raised to guarantee data accuracy. Furthermore, the construction of secure-channel incurs heavy cryptographic operations and single keyword search returns many irrelevant results. Along these directions, we further design a significantly more effective and secure cryptographic primitive called as verifiable conjunctive keywords search over encrypted data without secure-channel scheme to assure data integrity and availability. Formal security analysis proves that it can effectively stand against outside keyword-guessing attack. As a further contribution, our actual experiments show that it can admit wide applicability in practice.     

Friendly-jamming schemes to secure ultra-reliable and low-latency communications in 5G and beyond communications

The security vulnerabilities are becoming the major obstacle to prevent the wide adoption of ultra-reliable and low latency communications (URLLC) in 5G and beyond communications. Current security countermeasures based on cryptographic algorithms have a stringent requirement on the centralized key management as well as computational capabilities of end devices while it may not be feasible for URLLC in 5G and beyond communications. In contrast to cryptographic approaches, friendly jamming (FJ) as a promising physical layer security method can enhance wireless communications security while it has less resource requirement on end devices and it can be applied to the full distribution environment. In order to protect wireless communications, FJ signals are introduced to degrade the decoding ability of eavesdroppers who maliciously wiretap confidential information. This article presents a state-of-the-art survey on FJ schemes to enhance network security for IoT networks with consideration of various emerging wireless technologies and different types of networks. First, we present various secrecy performance metrics and introduce the FJ method. The interference caused by FJ signals on legitimate communication is the major challenge of using FJ schemes. In order to overcome this challenge, we next introduce the integration of FJ schemes with various communication technologies, including beamforming, multiple-input multiple-output, full duplex, and relay selection. In addition, we also integrate FJ schemes with different types of communication networks. Finally, a case study of FJ schemes is illustrated and future research directions of FJ schemes have been outlined.     

基于国密SM9的可搜索加密方案

为满足密文数据安全级别的要求,现有基于身份的可搜索加密方案多次使用安全参数较大的对称双线性对运算,导致计算效率降低,且其密钥形式难以与国家商用密码算法SM9相结合。针对该问题,设计一种基于SM9密码算法的可搜索加密方案。在离散椭圆曲线的两个子群中分别生成用户的公私钥对,使方案的密钥形式与SM9密码算法保持一致,解决经SM9密码算法加密后数据的检索问题,同时结合SM9密码算法,基于非对称双线性特性在确保方案安全性的同时提高检索效率。根据双线性对的性质分析该方案的正确性和安全性,并验证其满足在随机谕言模型下的适应性密文不可区分性和陷门不可区分性。仿真结果表明,与EdIBEKS、PEAKS、dIBAEKS方案相比,该方案在索引生成算法、陷门生成算法和检索匹配算法上的计算效率分别平均提高了77%、16.67%、28%以上。     

基于SM9的公钥可搜索加密方案

云存储技术因其使用便捷、性价比高等优势得以迅速发展,越来越多用户将个人数据外包至第三方云服务器存储。虽然数据加密存储可有效保护数据安全和用户隐私,但传统的对称/非对称加密技术会影响数据检索和使用。可搜索加密是一种特殊的加密技术,一经提出便备受关注,在保障数据机密性的同时可提供数据检索功能。目前,国内外学者提出了大量可搜索加密方案,但现有方案都基于国外密码算法设计,尚未见基于国产商用密码算法的可搜索加密方案在国内外刊物上公开发表,不符合我国密码核心技术自主可控的要求。为了丰富国产商用密码算法在可搜索加密方面的研究,满足云存储领域的数据安全检索需求,本文以SM9标识加密算法为基础,构造了一种公钥可搜索加密方案(SM9-PEKS)。在q-ABDHE安全假设和随机谕言模型下,本文首先证明SM9标识加密算法的匿名性,进而证明SM9-PEKS方案的安全性。理论分析和编程实现结果表明,与常用经典的公钥可搜索加密方案相比,本文方案在增加64字节通信代价的情况下,可至少降低31.31%的计算开销。最后,提出了未来可能的研究方向。     

Symbolic planning and control of robot motion [Grand Challenges of Robotics]

In this paper, different research trends that use symbolic techniques for robot motion planning and control are illustrated. As it often happens in new research areas, contributions to this topic started at about the same time by different groups with different emphasis, approaches, and notation. This article tries to describe a framework in which many of the current methods and ideas can be placed and to provide a coherent picture of what the authors want to do, what have they got so far, and what the main missing pieces are. Generally speaking, the aim of symbolic control as is envisioned in this article is to enable the usage of methods of formal logic, languages, and automata theory for solving effectively complex planning problems for robots and teams of robots. The results presented in this article can be divided in two groups: top-down approaches, whereby formal logic tools are employed on rather abstract models of robots; and bottom up approaches, whose aim is to provide means by which such abstractions are possible and effective. The two ends do not quite tie as yet, and much work remains to be done in both directions to obtain generally applicable methods. However, the prospects of symbolic control of robots are definitely promising, and the challenging nature of problems to be solved warrants for the interest of a wide community of researchers     

抗量子可信计算安全支撑平台技术

随着科技的发展,量子计算机大规模部署逐渐变为可能,基于部分计算困难问题的公钥密码算法将被量子算法有效求解.传统的可信硬件芯片如TCM/TPM等由于广泛使用了RSA、SM3、ECC等公钥密码体制,其安全性将受到严重影响;而绝大部分具有抗量子能力的密码算法并不适配现有TCM/TPM芯片有限的计算能力,因此需要对抗量子可信计...     

Model‐based security testing: a taxonomy and systematic classification

Model‐based security testing relies on models to test whether a software system meets its security requirements. It is an active research field of high relevance for industrial applications, with many approaches and notable results published in recent years. This article provides a taxonomy for model‐based security testing approaches. It comprises filter criteria (i.e. model of system security, security model of the environment and explicit test selection criteria) as well as evidence criteria (i.e. maturity of evaluated system, evidence measures and evidence level). The taxonomy is based on a comprehensive analysis of existing classification schemes for model‐based testing and security testing. To demonstrate its adequacy, 119 publications on model‐based security testing are systematically extracted from the five most relevant digital libraries by three researchers and classified according to the defined filter and evidence criteria. On the basis of the classified publications, the article provides an overview of the state of the art in model‐based security testing and discusses promising research directions with regard to security properties, coverage criteria and the feasibility and return on investment of model‐based security testing. Copyright © 2015 John Wiley & Sons, Ltd.     

How to obtain full privacy in auctions

Privacy has become a factor of increasing importance in auction design. We propose general techniques for cryptographic first-price and (M+1)st-price auction protocols that only yield the winners' identities and the selling price. Moreover, if desired, losing bidders learn no information at all, except that they lost. Our security model is merely based on computational intractability. In particular, our approach does not rely on trusted third parties, e.g., auctioneers. We present an efficient implementation of the proposed techniques based on El Gamal encryption whose security only relies on the intractability of the decisional Diffie—Hellman problem. The resulting protocols require just three rounds of bidder broadcasting in the random oracle model. Communication complexity is linear in the number of possible bids.     

对一种白盒SM4方案的差分计算分析

传统密码算法的安全性建立在黑盒攻击模型下. 在这种攻击模型下, 攻击者只能获取密码算法的输入输出, 而无法得知密码算法运行时的内部细节. 近年来白盒攻击模型的概念被提出. 在白盒攻击模型下, 攻击者既可以获取密码算法的输入输出, 也可以直接观测或更改密码算法运行时的内部数据. 为保证已有密码算法在白盒攻击环境下的安全性, 在不改变其功能的基础上通过白盒密码技术对其进行重新设计被称为已有密码算法的白盒实现. 研究白盒实现方案的设计与分析对于解决数字版权管理问题具有重要意义. 近年来, 出现了一类针对白盒实现方案的旁信道分析方法. 这类分析手段只需要知道很少白盒实现方案的内部细节, 却可以提取到密钥, 因此是一类对现有白盒实现方案具有实际威胁的分析手段. 对现有白盒实现方案进行此类分析对于确保方案安全性具有重要现实意义. 此类分析方法中的典型代表是基于差分功耗分析原理的差分计算分析. 基于差分计算分析, 对白-武白盒SM4方案进行了安全性分析. 基于对GF(2)上n阶均匀随机可逆矩阵统计特征的研究结果, 提出了一种改进型差分计算分析(IDCA), 可以在分析成功率几乎不变的前提下显著提升分析效率. 结果表明, 白-武白盒SM4方案在面对差分计算分析时不能保证安全性, 必须对其进行进一步改进使之满足实际应用场景下的安全性需求.     

Computationally sound implementations of equational theories against passive adversaries

In this paper we study the link between formal and cryptographic models for security protocols in the presence of passive adversaries. In contrast to other works, we do not consider a fixed set of primitives but aim at results for arbitrary equational theories. We define a framework for comparing a cryptographic implementation and its idealization with respect to various security notions. In particular, we concentrate on the computational soundness of static equivalence, a standard tool in cryptographic pi calculi. We present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, to illustrate our framework, we establish the soundness of static equivalence for the exclusive OR and a theory of ciphers and lists.