We develop CNetVerifier, an automated control-plane protocol interaction verification method with domain-specific heuristics and model checking techniques to systematically explore possible problematic interactions in cellular networks. The main advantage of this methodology is the exploration of problems/issues in mobile networks is not restricted by unlimited use scenarios (time consuming) or the lack of full access to mobile device or network infrastructure. Its impact on the wireless/mobile networking technology and cybersecurity can be considered as far-reaching. It does not only capture the fundamental design issues of mobile networks span over multiple dimensions, but also discover the security loopholes> caused by improper designs of control-plane protocols of mobile networks. The lessons we learnt can be even applied to the next big things (e.g., 5G, Internet of Thing, Device-to-Device communication) in the networking area.