Verification of Security Protocols Using Formal Methods


Abstract in English

There are many of Formal Methods for testing security protocols detecting being safe or not. Including Avispa, Casper, ProVerif, Scyther. Previously a comparisons using two of mentioned methods (ProVerif, Scyther). In this, research a comparison between the four mentioned methods in terms of the same used parameters in the previous comparison: working style, the modeling language, user interface, input, and output. As a result, the user provided with options to choose the appropriate method depending on the desired parameter. Six different of security protocols have been tested and finally the results have been compared; these protocols are Kao Chow Authentication Protocol, 3-D Secure Protocol, Needham-Schroeder Public Key Protocol, Diffie–Hellman key exchange, Andrew Secure RPC Protocol, and Challenge Handshake Authentication Protocol

References used

ALSHEHRI, A. A. NFC mobile coupon protocols: developing, formal security modelling and analysis, and addressing relay attack (Doctoral dissertation, University of Surrey). (2015)
BIONDI, F., & LEGAY, A. Security and Privacy of Protocols and Software with Formal Methods. In International Symposium on Leveraging Applications of Formal Methods (pp. 883-892). Springer International Publishing. (2016)
BLANCHET, B., SMYTH, B., & CHEVAL, V. (2015). ProVerif 1.90: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. URL: http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf online last accessed on 22-7-2016

Download