Filters: Keyword is ProVerif  [Clear All Filters]
Iftikhar, Jawad, Hussain, Sajid, Mansoor, Khwaja, Ali, Zeeshan, Chaudhry, Shehzad Ashraf.  2019.  Symmetric-Key Multi-Factor Biometric Authentication Scheme. 2019 2nd International Conference on Communication, Computing and Digital systems (C-CODE). :288–292.
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.
Dewoprabowo, Ridhwan, Arzaki, Muhammad, Rusmawati, Yanti.  2018.  Formal Verification of Divide and Conquer Key Distribution Protocol Using ProVerif and TLA+. 2018 International Conference on Advanced Computer Science and Information Systems (ICACSIS). :451-458.

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.

Kobeissi, N., Bhargavan, K., Blanchet, B..  2017.  Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. 2017 IEEE European Symposium on Security and Privacy (EuroS P). :435–450.

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.