Biblio

The mechanism of Fog computing is a distributed infrastructure to provide the computations as same as cloud computing. The fog computing environment provides the storage and processing of data in a distributed manner based on the locality. Fog servicing is better than cloud service for working with smart devices and users in a same locale. However the fog computing will inherit the features of the cloud, it also suffers from many security issues as cloud. One such security issue is authentication with efficient key management between the communicating entities. In this paper, we propose a secured two-way authentication scheme with efficient management of keys between the user mobile device and smart devices under the control of the fog server. We made use of operations such as one-way hash (SHA-512) functions, bitwise XOR, and fuzzy extractor function to make the authentication system to be better. We have verified the proposed scheme for its security effectiveness by using a well-used analysis tool ProVerif. We also proved that it can resist multiple attacks and the security overhead is reduced in terms of computation and communication cost as compared to the existing methods.

The advent of 5G, one of the most recent and promising technologies currently under deployment, fulfills the emerging needs of mobile subscribers by introducing several new technological advancements. However, this may lead to numerous attacks in the emerging 5G networks. Thus, to guarantee the secure transmission of user data, 5G Authentication protocols such as Extensible Authentication Protocol - Authenticated Key Agreement Protocol (EAP-AKA) were developed. These protocols play an important role in ensuring security to the users as well as their data. However, there exists no guarantees about the security of the protocols. Thus formal verification is necessary to ensure that the authentication protocols are devoid of vulnerabilities or security loopholes. Towards this goal, we formally verify the security of the 5G EAP-AKA protocol using an automated verification tool called ProVerif. ProVerif identifies traces of attacks and checks for security loopholes that can be accessed by the attackers. In addition, we model the complete architecture of the 5G EAP-AKA protocol using the language called typed pi-calculus and analyze the protocol architecture through symbolic model checking. Our analysis shows that some cryptographic parameters in the architecture can be accessed by the attackers which cause the corresponding security properties to be violated.

Supply chain management systems (SCM) are the most intensive and statistical RFID application for object tracking. A lot of research has been carried out to overcome security issues in the field of online/offline object tracking as well as authentication protocols involving RFID technology. Due to advancements with the Internet of Things (IoT) and embedded systems in object tracking schemes the latest research manages to deliver information about the object’s location as well as provide particulars about the state of an object. Recent research presented a proposal for an authentication and online object tracking protocol focusing on solutions for privacy issues for device identification, end-to-end authentication, and secure online object tracking. However, recent schemes have been found to be vulnerable to traceability attacks. This paper presents an enhanced end-to-end authentication scheme where the identity of the user is kept anonymous so that its actions can not be tracked, eliminating attacks related to traceability. The security of the proposed protocol is formally analyzed using the attack model of the automated security testing tool, ProVerif. The proposed scheme outperforms competing schemes based on security.

The extensive use of the internet and web-based applications spot the multiserver authentication as a significant component. The users can get their services after authenticating with the service provider by using similar registration records. Various protocol schemes are developed for multiserver authentication, but the existing schemes are not secure and often lead towards various vulnerabilities and different security issues. Recently, Zhao et al. put forward a proposal for smart card and user's password-based authentication protocol for the multiserver environment and showed that their proposed protocol is efficient and secure against various security attacks. This paper points out that Zhao et al.'s authentication scheme is susceptive to traceability as well as anonymity attacks. Thus, it is not feasible for the multiserver environment. Furthermore, in their scheme, it is observed that a user while authenticating does not send any information with any mention of specific server identity. Therefore, this paper proposes an enhanced, efficient and secure user authentication scheme for use in any multiserver environment. The formal security analysis and verification of the protocol is performed using state-of-the-art tool “ProVerif” yielding that the proposed scheme provides higher levels of security.

Owing to the advancements in communication media and devices all over the globe, there has arisen a dire need for to limit the alarming number of attacks targeting these and to enhance their security. Multiple techniques have been incorporated in different researches and various protocols and schemes have been put forward to cater security issues of session initiation protocol (SIP). In 2008, Qiu et al. presented a proposal for SIP authentication which while effective than many existing schemes, was still found vulnerable to many security attacks. To overcome those issues, Zhang et al. proposed an authentication protocol. This paper presents the analysis of Zhang et al. authentication scheme and concludes that their proposed scheme is susceptible to user traceablity. It also presents an improved SIP authentication scheme that eliminates the possibility of traceability of user's activities. The proposed scheme is also verified by contemporary verification tool, ProVerif and it is found to be more secure, efficient and practical than many similar SIP authetication scheme.

Authentication is achieved by using different techniques, like using smart-card, identity password and biometric techniques. Some of the proposed schemes use a single factor for authentication while others combine multiple ways to provide multi-factor authentication for better security. lately, a new scheme for multi-factor authentication was presented by Cao and Ge and claimed that their scheme is highly secure and can withstand against all known attacks. In this paper, it is revealed that their scheme is still vulnerable and have some loopholes in term of reflection attack. Therefore, an improved scheme is proposed to overcome the security weaknesses of Cao and Ge's scheme. The proposed scheme resists security attacks and secure. Formal testing is carried out under a broadly-accepted simulated tool ProVerif which demonstrates that the proposed scheme is well secure.

We conduct formal verification of the divide and conquer key distribution scheme (DC DHKE)-a contributory group key agreement that uses a quasilinear amount of exponentiations with respect to the number of communicating parties. The verification is conducted using both ProVerif and TLA+ as tools. ProVerif is used to verify the protocol correctness as well as its security against passive attacker; while TLA+ is utilized to verify whether all participants in the protocol retrieve the mutual key simultaneously. We also verify the ING and GDH.3 protocol for comparative purposes. The verification results show that the ING, GDH.3, and DC DHKE protocols satisfy the pre-meditated correctness, security, and liveness properties. However, the GDH.3 protocol does not satisfy the liveness property stating that all participants obtain the mutual key at the same time.

Many popular web applications incorporate end-toend secure messaging protocols, which seek to ensure that messages sent between users are kept confidential and authenticated, even if the web application's servers are broken into or otherwise compelled into releasing all their data. Protocols that promise such strong security guarantees should be held up to rigorous analysis, since protocol flaws and implementations bugs can easily lead to real-world attacks. We propose a novel methodology that allows protocol designers, implementers, and security analysts to collaboratively verify a protocol using automated tools. The protocol is implemented in ProScript, a new domain-specific language that is designed for writing cryptographic protocol code that can both be executed within JavaScript programs and automatically translated to a readable model in the applied pi calculus. This model can then be analyzed symbolically using ProVerif to find attacks in a variety of threat models. The model can also be used as the basis of a computational proof using CryptoVerif, which reduces the security of the protocol to standard cryptographic assumptions. If ProVerif finds an attack, or if the CryptoVerif proof reveals a weakness, the protocol designer modifies the ProScript protocol code and regenerates the model to enable a new analysis. We demonstrate our methodology by implementing and analyzing a variant of the popular Signal Protocol with only minor differences. We use ProVerif and CryptoVerif to find new and previously-known weaknesses in the protocol and suggest practical countermeasures. Our ProScript protocol code is incorporated within the current release of Cryptocat, a desktop secure messenger application written in JavaScript. Our results indicate that, with disciplined programming and some verification expertise, the systematic analysis of complex cryptographic web applications is now becoming practical.