در مورد تایید امنیت پروتکل سرویس پیام کوتاه On the Security Verification of a Short Message Service Protocol

I. INTRODUCTION Short Message Service (SMS) is playing a major role in present-day mobile networks. SMS services are widely used in many online services such as mobile banking, marketing, sales delivery and many more [1], [2]. Since SMS can deliver lots of vital information, SMS systems are becoming vulnerable to more and more attacks, such as deception, eavesdropping, messages tampering, spoofing and forgery [3]. In the technical specifications for SMS [4], the confidentiality and integrity mechanisms are only specified as optional security measures that can be made available, but they are not mandatory requirements for SMS system implementation. Hence, without these SMS security options, the SMS messages transmitted on a network are only protected by the communication network itself such as GSM network, shown to be prone to many errors [5]. Therefore, it is required to design a security mechanism that can provide user authentication, data confidentiality and integrity. To offer such security features, Wu and Tan proposed a high security SMS communication protocol called Message Security Communication Protocol (MSCP) [6]. Many cryptographic security protocols such as MSCP [6] are widely used/proposed in secure data exchange over both mobile and infrastructure networks. The design of correctnessprovable security protocols is highly complex and prone to errors. The main difficulty in the development of security protocols is to identify the vast possibilities of an adversary to gain information [7]. In such cases, informal and intuitive techniques are often used to analyze security protocols, resulting in insecure protocols to be widely used in public networks. On the other hand, formal verification techniques have been proven to be able to identify previously unknown flaws in security protocols through the means of protocol verification, providing confidence in the correctness of the protocols. In particular, the use of the automated logic-based technique with attack detection capability described in [7]–[12] has been shown to be an effective approach in detecting flaws in the design of security protocols. This paper is concern with logic-based formal verification and its use in the design of security protocols. We formally analyze MSCP by using an automated logic-based verification tool, which reveals that the protocol is susceptible to a denialof-service (DoS) attack and a parallel session attack. We analyze the issues in MSCP and propose an amended version of the protocol that counters the identified weaknesses. Then, a formal verification of the amended protocol is provided to verify the correctness and effectiveness of the proposed modifications. The rest of paper is organized as follows: Section II presents the logic-based verification process. Section III introduces Message Security Communication Protocol (MSCP). Section IV contains the formal verification of MSCP. Section V presents the amended protocol and Section VI presents its formal verification. Finally, Section VII concludes this paper.