OAuth2.0协议形式化验证: 使用AVISPA

OAuth协议是一套用于在不同的服务中进行身份认证并且实现资源互访一套协议.由于关系到用户隐私,所以OAuth协议的安全性非常重要.这篇文章的主要贡献是研究OAuth2.0协议文本,对协议进行抽象,并且使用验证工具AVISPA对抽象后的协议进行建模与验证,找到协议中会导致隐私泄露的一种攻击模式.我们在建模过程中提出需将要验证的消息作为双方的对称密码这样一种创新思路.这种对协议的抽象和验证的方法可以推广到其他安全协议上,例如在线支付协议等等.     

A secure multifactor remote user authentication scheme for Internet of Multimedia Things environment

To attain ubiquitous connectivity of everything, Internet of Things (IoT) systems must include “multimedia things.” Internet of Multimedia Things (IoMT) is a heterogeneous network of smart multimedia things connected together and with other physical devices to the Internet so as to achieve globally available multimedia services and applications. Due to the ever increasing amount of multimedia data in IoT environments, securing these systems becomes crucial. This is because these systems are easily susceptible to attacks when information or any service is accessed by the users. In this paper, we propose a secure three‐factor remote user authentication scheme for IoMT systems using ECC. The formal security proof performed using ROR model and BAN logic confirms that an attacker will not be able to extract sensitive user information. Through informal security analysis, we justify the resistance of the scheme against several security attacks. The performance comparison shows that the scheme is efficient in terms of computational cost, security features, and attack resistance. Furthermore, simulation of the scheme using AVISPA and Proverif proves that the scheme is secure against all active and passive attacks.     

Privacy‐preserving authentication scheme for on‐road on‐demand refilling of pseudonym in VANET

Privacy in Vehicular Ad Hoc Networks (VANET) is fundamental because the user's safety may be threatened by the identity and the real‐time spatiotemporal data exchanged on the network. This issue is commonly addressed by the use of certified temporal pseudonyms and their updating strategies to ensure the user's unlinkability and anonymity. IEEE 1609.2 Standard specified the process of certifying pseudonym along with certificates structure. However, the communication procedure between the certifying authority and the requesting vehicle was not defined. In this paper, a new privacy‐preserving solution for pseudonym on‐road on‐demand refilling is proposed where the vehicle anonymously authenticates itself to the regional authority subsidiary of the central trusted authority to request a new pseudonyms pool. The authentication method has two phases, the first one uses anonymous tickets, and the second one is a challenge‐based authentication. The anonymous tickets are certificates that do not include the identity of the user. Instead, it contains a reference number and the certifying authority signature. The challenge authentication is identity‐less to preserve the privacy, yet it is used to prevent the misuse of tickets and the impersonation of its owner. Our proposed scheme is analyzed by the use of Burrows, Abadi and Needham (BAN) logic to demonstrate its correctness. It is also specified and checked by using the Security Protocol ANimator (SPAN) and the Automated Validation of Internet Security Protocols and Applications (AVISPA) tools. The logical demonstration proved that this privacy‐preserving authentication is assured. The SPAN and AVISPA tools illustrated that it is resilient to security attacks.     

Provably secure authenticated key agreement scheme for distributed mobile cloud computing services

With the rapid development of mobile cloud computing, the security becomes a crucial part of communication systems in a distributed mobile cloud computing environment. Recently, in 2015, Tsai and Lo proposed a privacy-aware authentication scheme for distributed mobile cloud computing services. In this paper, we first analyze the Tsai–Lo’s scheme and show that their scheme is vulnerable to server impersonation attack, and thus, their scheme fails to achieve the secure mutual authentication. In addition, we also show that Tsai–Lo’s scheme does not provide the session-key security (SK-security) and strong user credentials’ privacy when ephemeral secret is unexpectedly revealed to the adversary. In order to withstand these security pitfalls found in Tsai–Lo’s scheme, we propose a provably secure authentication scheme for distributed mobile cloud computing services. Through the rigorous security analysis, we show that our scheme achieves SK-security and strong credentials’ privacy and prevents all well-known attacks including the impersonation attack and ephemeral secrets leakage attack. Furthermore, we simulate our scheme for the formal security analysis using the widely-accepted AVISPA (Automated Validation of Internet Security Protocols and Applications) tool, and show that our scheme is secure against passive and active attacks including the replay and man-in-the-middle attacks. More security functionalities along with reduced computational costs for the mobile users make our scheme more appropriate for the practical applications as compared to Tsai–Lo’s scheme and other related schemes. Finally, to demonstrate the practicality of the scheme, we evaluate the proposed scheme using the broadly-accepted NS-2 network simulator.     

An extended ECC‐based anonymity‐preserving 3‐factor remote authentication scheme usable in TMIS

A telecare medicine information system (TMIS) helps in providing an efficient communication platform to patients from home to consult doctors at a clinical center. In TMIS, the patient's confidentiality, security, and mutual authentication are very crucial; so remote authentication plays a vital role for verifying the legitimacy of patients. Recently, Amin and Biswas have devised a remote authentication protocol for TMIS, claiming it to be secured from various malicious vulnerabilities. We examine this protocol and find that it is not able to withstand many attacks that include off‐line and online password‐guessing, identity‐guessing, user impersonation, privileged insider, and known session key temporary information attacks. We propose a 3‐factor–based authentication protocol for TMIS by overcoming these security shortcomings. We present its security verification in formal and informal ways, which assert its resistivity against various security threats. We use the Burrows‐Abadi‐Needham logic for validating it, and with the Automated Validation of Internet Security Protocols and Applications tool, it is simulated. Further, the performance evaluation and the security functionalities justify high degree of security with efficient complexity.     

主从区块链容错异构跨域身份认证方案

异构跨域身份认证是对不同体制信任域内的节点进行身份确认和安全信息交互的技术,现有的认证方案主要存在单点攻击风险和认证复杂等问题。为此,设计了主从区块链身份认证模型和匹配使用的分层拜占庭容错算法,通过主从链分步、分阶段共识,减少了共识参与节点数量,并将PKI体制与CL-PKC体制的特有功能节点与主从链节点相对应,在不改变原有信任域节点功能的前提下,使用区块链证书的哈希值高效传递信任,优化了认证流程,实现了双向异构跨域身份认证。最后通过仿真实验验证以及安全性和性能分析,表明该方案与相关方案对比,在实现安全通信的同时,提高了共识效率和容错性,降低了认证过程的通信开销。     

A secure user anonymity-preserving biometric-based multi-server authenticated key agreement scheme using smart cards

Advancement in communication technology provides a scalable platform for various services, where a remote user can access the server from anywhere without moving from its place. It provides a unique opportunity for online services such that a user does not need to be physically present at the service center. These services adopt authentication and key agreement protocols in order to ensure authorized and secure access to the resources. Most of the authentication schemes proposed in the literature support a single-server environment, where the user has to register with each server. If a user wishes to access multiple application servers, he/she requires to register with each server. The multi-server authentication introduces a scalable platform such that a user can interact with any server using single registration. Recently, Chuang and Chen proposed an efficient multi-server authenticated key agreement scheme based on a user’s password and biometrics (Chuang and Chen, 2014). Their scheme is a lightweight, which requires the computation of only hash functions. In this paper, we first analyze Chuang and Chen’s scheme and then identify that their scheme does not resist stolen smart card attack which causes the user’s impersonation attack and server spoofing attack. We also show that their scheme fails to protect denial-of-service attack. We aim to propose an efficient improvement on Chuang and Chen’s scheme to overcome the weaknesses of their scheme, while also retaining the original merits of their scheme. Through the rigorous informal and formal security analysis, we show that our scheme is secure against various known attacks including the attacks found in Chuang and Chen’s scheme. Furthermore, we simulate our scheme for the formal security verification using the widely-accepted AVISPA (Automated Validation of Internet Security Protocols and Applications) tool and show that our scheme is secure against the replay and man-in-the-middle attacks. In addition, our scheme is comparable in terms of the communication and computational overheads with Chuang and Chen’s scheme and other related existing schemes.     

An anonymous and robust multi‐server authentication protocol using multiple registration servers

The concept of multi‐server authentication includes multiple numbers of application servers. The registration/control server is the central point in such environment to provide smooth services to a limited number of legitimate users. However, this type of environment is inappropriate to handle unlimited users since the number of users may grow, and thus, the response time may be very high. To eliminate these shortcomings, we have modified the existing multi‐server authentication architecture and then designed a new scheme by including multiregistration server technique that can provide a smooth environment to support unlimited number of users. The main aspect of our design is to provide a secure authentication environment for multi‐server application using password and smartcard so that the participants can securely communicate with each other. The simulation results are obtained by executing our protocol using AVISPA tool. The results provide concrete evidence about the security safety against active and passive attacks. Furthermore, the justification of correctness of the freshness of the session key negotiation and the mutual authentication between the participants has done been evaluated with the BAN logic model. The comprehensive comparative analysis justifies our argument that our protocol has better applicability in multi‐server environments compared to other protocols with similar nature.     

Improved IPSec tunnel establishment for 3GPP–WLAN interworking

Interworking between wireless local area network (WLAN) and the 3rd Generation Partnership Project (3GPP) such as Long Term Evolution (LTE) is facing more and more problems linked to security threats. Securing this interworking is a major challenge because of the vastly different architectures used within each network. Therefore, security is one of the major technical concerns in wireless networks that include measures such as authentication and encryption. Among the major challenges in the interworking security is the securing of the network layer. The goal of this article is twofold. First, we propose a new scheme to secure 3GPP LTE–WLAN interworking by the establishment of an improved IP Security tunnel between them. The proposed solution combines the Internet Key Exchange (IKEv2) with the Host Identity Protocol (HIP) to set up a security association based on two parameters, which are location and identity. Our novel scheme, which is called HIP_IKEv2, guarantees better security properties than each protocol used alone. Second, we benefit from Mobile Internet Key Exchange protocol (MOBIKE) in case of mobility events (handover). And we extend HIP_IKEv2 to HIP_MOBIKEv2 protocol in order to reduce the authentication signaling traffic. The proposed solution reinforces authentication, eliminates man‐in‐the‐middle attack, reduces denial‐of‐service attack, assures the integrity of messages, and secures against reply attack. Finally, our proposed solution has been modeled and verified using the Automated Validation of Internet Security Protocols and Applications and the Security Protocol Animator, which has proved its security when an intruder is present. Copyright © 2014 John Wiley & Sons, Ltd.     

A secure end‐to‐end SMS‐based mobile banking protocol

Short message service (SMS) provides a wide channel of communication for banking in mobile commerce and mobile payment. The transmission of SMS is not secure in the network using global system for mobile communications or general packet radio service. Security threats in SMS restricted the use of SMS in mobile banking within certain limits. This paper proposed a model to address the security of SMS using elliptic curve cryptography. The proposed model provides end‐to‐end SMS communication between the customer and the bank through the mobile application. The main objective of the proposed model is to design and develop a security framework for SMS banking. Further, the protocol is verified for its correctness and security properties because most of the protocols are not having the facility to be verified by using the formal methods. Our proposed framework is experimentally validated by formal methods using model checking tool called automated validation of internet security protocols and Scyther tools. Security analysis shows that the proposed mechanism works better compared to existing SMS payment protocols for real‐world applications.