Analysis and Evaluation of the TETRA Network Security Protocols Using Automated Analysis Tools

In this paper, the structure of the various versions of the TETRA security protocol is investigated in the “formal model” using Proverif and Scyther automatic analysis tools. The TETRA's network security protocol is a key-exchange one, in which two parties also establish a session key while authenticating each other. This protocol also uses pre-distributed secret keys which are based on the symmetric-encryption schemes. The security analysis of the protocol has been done in the “formal model”, using the Proverif and Scyther automatic analysis tools. Firstly, eight security features including Confidentiality, Authentication, Forward Secrecy, Unknown Key-Share security, Identical Session Key, Unknown Key Security, Anonymity, and Integrity are modeled in these frameworks, and then using both of the two tools, the security of the protocol is investigated regarding the mentioned features. Comparing the results of the formal analysis of these features with the informal analysis resulted from the open sources indicates that there are new security flows in the structure of the protocol respect to “Forward Secrecy” and “integrity”. Finally, several solutions are suggested to overcome these weaknesses.