基于ProVerif的电子商务协议分析

采用应用pi演算来建模自动解决争端的公平电子商务协议,基于一致性给出了公平性的形式描述方法,利用应用pi演算的自动化分析工具--ProVerif分析了该协议,结果表明,利用一致性描述协议公平性是可行的,同时指出了基于ProVerif验证电子商务协议的优缺点:适用于分析"A事件发生以前,B事件是否曾经发生",但不适用于分析"A事件发生之后,B事件将来是否会必然(或可能)发生".     

Cryptanalysis and security enhancement of a robust two‐factor authentication and key agreement protocol

Two‐factor user authentication scheme allows a user to use a smart card and a password to achieve mutual authentication and establish a session key between a server and a user. In 2012, Chen et al. showed that the scheme of Sood et al. does not achieve mutual authentication and is vulnerable to off‐line password guessing and smart card stolen attacks. They also found that another scheme proposed by Song is vulnerable to similar off‐line password guessing and smart card stolen attacks. They further proposed an improved scheme. In this paper, we first show that the improved scheme of Chen et al. still suffers from off‐line password guessing and smart card stolen attacks, does not support perfect forward secrecy, and lacks the fairness of session key establishment. We then propose a new security‐enhanced scheme and show its security and authentication using the formal verification tool ProVerif, which is based on applied pi calculus. Copyright © 2014 John Wiley & Sons, Ltd.     

安全增强的智能电网轻量级匿名认证方案

现有的智能电网身份认证方案大多存在计算成本高和认证流程复杂的问题,不适用于智能电网中资源受限的智能设备。而一些轻量级的方案却存在各种安全漏洞,这些方案都无法在效率和安全性之间实现所需的权衡。针对上述问题,基于椭圆曲线加密算法设计了一个增强的可证明安全的智能电网轻量级匿名认证方案。引入辅助验证器,摆脱在认证阶段对于电力供应商的依赖,在保护智能电表真实身份的条件下实现网关和智能电表之间的相互认证。同时,可以通过伪身份对恶意智能电表进行身份的溯源和撤销。通过在随机预言模型下的安全性分析和仿真工具ProVerif证明了方案具备较高的安全属性。性能分析表明,所提方案能够满足智能电网环境下对于安全性和高效性的要求。     

Lattice-Based Authentication Scheme to Prevent Quantum Attack in Public Cloud Environment

Public cloud computing provides a variety of services to consumers via high-speed internet. The consumer can access these services anytime and anywhere on a balanced service cost. Many traditional authentication protocols are proposed to secure public cloud computing. However, the rapid development of high-speed internet and organizations’ race to develop quantum computers is a nightmare for existing authentication schemes. These traditional authentication protocols are based on factorization or discrete logarithm problems. As a result, traditional authentication protocols are vulnerable in the quantum computing era. Therefore, in this article, we have proposed an authentication protocol based on the lattice technique for public cloud computing to resist quantum attacks and prevent all known traditional security attacks. The proposed lattice-based authentication protocol is provably secure under the Real-Or-Random (ROR) model. At the same time, the result obtained during the experiments proved that our protocol is lightweight compared to the existing lattice-based authentication protocols, as listed in the performance analysis section. The comparative analysis shows that the protocol is suitable for practical implementation in a quantum-based environment.     

An efficient and authenticated key establishment scheme based on fog computing for healthcare system

Because of its closeness to users, fog computing responds faster than cloud computing. Thus, it has been deployed to various applications, such as healthcare system. Recently, to ensure the secure communication of the fog-based healthcare system, Jia et al. proposed an authenticated key agreement scheme. Moreover, in view of the high computation cost existing in Jia et al.’s scheme, Ma et al. presented an efficient one using elliptic curve cryptography. In this paper, we observe that both the two schemes may potentially risk ephemeral key compromise attacks and need improving. Therefore, to overcome this potential risk, we propose a new authenticated scheme based on Jia et al.’s scheme using elliptic curve computational Diffie-Hellman hypothesis and hash functions. Additionally, we provide provable security under the adopted adversarial model and ProVerif simulation, and also analyze the performance in terms of computation and communication costs by comparisons. The analysis results show that the improved scheme resists the common attacks, reduces computation overhead, and has a certain significance.     

Efficient design and hardware implementation of a secure communication scheme for smart grid

In smart grid, bidirectional communications between the smart meters and control center are subject to several security challenges. Since the smart meters have limited storage space and processing capability, the suggested communication scheme not only must consider the security requirements but also should put the least possible burden on the smart meters' resources. In 2014, an interesting communication scheme has been proposed for the secure consumption reports transmission of the smart meters to the neighbor gateways. In this paper, we first show that this scheme is vulnerable to the smart meter's memory modification, pollution, and denial of service attacks; then, we propose an authenticated communication scheme, which not only is secure against the aforementioned attacks, but also is much more efficient in terms of storage space, communication overhead, and computational complexity. Moreover, our scheme also presents the details of control messages transmission from the neighborhood gateways to the smart meters. Our comparative analysis with several recently published schemes indicates that the proposed scheme is more suitable than the previous ones. More significantly, our realistic implementation on ATmega2560, as a suitable candidate to be used for the smart meters, confirms our claim.     

基于ProVerif的可信平台模块安全分析

可信平台模块是可信计算技术的关键部件,其安全性直接影响可信评估的结果。使用演算对可信平台模块进行了形式化建模,并利用该模型对模块中的密钥签署命令进行安全性分析。最后,经模型自动化分析工具ProVerif的验证发现了该命令存在的安全漏洞。     

改进的OpenID Connect协议及其安全性分析

OpenID Connect协议是最新的单点登录协议之一,已经广泛应用于用户身份认证领域,其安全性受到了人们的重点关注。为增强OpenID Connect协议的安全性,首先引入数字签名及非对称加密技术,对其进行改进,重点关注改进后协议的秘密性和认证性;其次基于符号模型,应用应用PI演算对改进的OpenID Connect协议进行形式化建模;然后为验证改进后协议的认证性和秘密性,分别使用非单射性和query对认证性和秘密性进行建模;最后把改进的OpenID Connect协议的应用PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析。实验结果表明,改进后的OpenID Connect协议具有认证性和秘密性。     

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

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明,并通过对Kerbero...     

An improved and secure multiserver authentication scheme based on biometrics and smartcard

With the advancement in internet technologies, the number of servers has increased remarkably to provide more services to the end users. These services are provided over the public channels, which are insecure and susceptible to interception, modification, and deletion. To provide security, registered entities are authenticated and then a session key is established between them to communicate securely. The conventional schemes allow a user to access services only after their independent registration with each desired server in a multiserver system. Therefore, a user must possess multiple smartcards and memorize various identities and passwords for obtaining services from multiple servers. This has led to the adoption of multiserver authentication in which a user accesses services of multiple servers after registering himself at only one central authority. Recently, Kumar and Om discussed a scheme for multiserver environment by using smartcard. Since the user-memorized passwords are of low entropy, it is possible for an attacker to guess them. This paper uses biometric information of user to enhance the security of the scheme by Kumar and Om. Moreover, we conducted rigorous security analyses (informal and formal) in this study to prove the security of the proposed scheme against all known attacks. We also simulated our scheme by using the automated tool, ProVerif, to prove its secrecy and authentication properties. A comparative study of the proposed scheme with the existing related schemes shows its effectiveness.