In recent years, the number of studies conducted on the effectiveness of formal methods in analyzing and verifying security protocols has increased. The ProVerif model checker and the Tamarin theorem prover are widely used automatic tools for the formal verification of cryptographic security protocols. ProVerif sometimes hands over the decision of the attack detection process to the verifier because it cannot determine the “cannot be proved” verification result. In this case, there is a possibility to rigorously determine the security properties and weaknesses of a security protocol using the Tamarin prover for verification. In this study, the “cannot be proved” output by ProVerif is manually examined using the Tamarin prover, and the results output by these verification tools are compared. The detailed investigation of the verification results output by the above tools showed that in some cases, these results were different even for the same cryptographic protocol.