تحليل و ارزيابي صوري پروتكل هاي امنيتي شبكه تترا با استفاده از ابزارهاي تحليل خودكار

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.