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