Revisiting the BAN-Modified Andrew Secure RPC Protocol

Alberto Gugel¹, Benjamin Aziz¹⁺, and Geoff Hamilton²

¹University of Portsmouth, Portsmouth, United Kingdom
alberto.gugel@port.ac.uk, benjamin.aziz@port.ac.uk

²Dublin City University, Dublin, Ireland

geoff.hamilton@computing.dcu.ie

Abstract

We have analysed the well-known BAN modified Andrew Secure RPC authentication protocol by means of the AVISPA Web tool considering all the available back-ends and with the basic configurations of sessions. The protocol has been found vulnerable to a replay/mutation attack based on homomorphism by one of the back-ends. In order to fix it, we integrated into the protocol a common solution, including a new addition to the original protocol and the solution proposed by Liu, Ma and Yang, who earlier found a man-in-the-middle attack by means of a different model checker instantiated with different session compositions. When we tested this solution in AVISPA, under both conditions, we discovered that AVISPA considers it safe, while it can be demonstrated that it suffers from the same mutation attack as in the original protocol.

Keywords: protocol verification, internet protocols, static analysis, internet security

+: Corresponding author: Benjamin Aziz
School of Computing, University of Portsmouth, Portsmouth PO1 3HE, Tel: +44-(0)23-9284-2265,

Web: http://azizb.myweb.port.ac.uk/

Journal of Internet Services and Information Security (JISIS), 4(3): 82-96, August 2014 [pdf]