Revisiting the BAN-modified Andrew Secure RPC protocol

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.