Abstract
As the multimedia social network develops rapidly, protocols protecting the security of realtime multimedia are becoming very significant. The ZRTP protocol, one of Real-time Transport Protocols (RTPs) for real-time multimedia applications, has many advantages compared with others. Though the calculation cost is relatively high, the ZRTP protocol provides perfect forward secrecy and authentication against man-in-the-middle attack. As so many formal verification tools were proposed recently, formal method has become one of the main methods of security protocol analysis. However, the formal verification tools are rarely used for the Real-time Transport Protocols. In this paper, we innovatively utilize the formal verification tool Scyther- Compromise and Tamarin to analyse the ZRTP protocol. According to the results, we find that the ZRTP protocol is insecure under the eCK model though it provides the perfect forward secrecy property. The adversary can impersonate the endpoint when the shared secrets are revealed. Besides, the experiments of this paper show that the formal method can perform perfectly and play an important role in protocol analysis.
Keywords: Formal analysis, real-time transport protocol, scyther, tamarin, ZRTP protocol.
Graphical Abstract
Call for Papers in Thematic Issues
Advancements in Brain Tumor Detection and Treatment using Machine Learning, Deep Learning, and Blockchain Technology
Brain tumors are among the most challenging diseases to diagnose and treat, requiring specialized expertise and advanced technology for accurate detection and effective treatment. In recent years, machine learning and deep learning algorithms have shown promise in improving the accuracy and efficiency of brain tumor detection through medical imaging analysis. ...read more
Advances of Biometric Data Analysis to Boost Intelligent Applications
With the rapid development of artificial intelligence (AI) technology, more and more intelligent devices and applications are appearing in our daily lives, such as smart home, smart agriculture, health diagnosis, educational support, and environmental monitoring. Interaction with these devices or applications has become a pressing issue that can greatly improve ...read more
Attainment of SDGs through the Advancement in Solar Energy Systems
With less than a decade until we reach 2030, it is crucial to address the deep inequalities affecting not only our health but also our quality of life, and the economy of countries worldwide. Few of the UN's Sustainable Development Goals (SDGs) can be directly and indirectly achieved through the ...read more
Computational Intelligence theory and practices
Computational intelligence represents the extraordinary capacity of the human intellect to assert and understand in an environment of uncertainty and imprecision. Computational intelligence is new-age multidisciplinary branch of artificial intelligence which can reduce the human work. The main goal of computational intelligence is to develop intelligent systems to solve real-world ...read more
Related Journals
Recent Patents on Engineering
23
4