A Security Formal Model for Multiple Channels Communication

Recent heterogeneous networks, such as LTE-A and 5G, support roaming of mobilities between multiple domains and may require communications on different channels, which brought new challenges to network security. However, existed Formal Security Methods usually abstract the communications in networking systems with one public channel, which makes the modeling of heterogeneous networks become difficult. In this article, based on the basic syntax of Applied Pi Calculus, we define a multiple channel syntax and the corresponding semantic rules for the security analysis of heterogeneous networks. We applied the proposed methods on a typical 3GPP and Non 3GPP heterogeneous structure, and the results present that the method can support the formal security evaluation of heterogeneous networks.