基于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.     

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.     

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.