Secure communications are paramount in today's environment, where mobile and fixed networks are trusted with highly sensitive information. Cryptographic protocols are used to provide security services, such as confidentiality, authentication and non-repudiation. Beller, Chang and Yacobi (BCY) proposed three communication protocols capable of providing mobile link security services. These protocols use a combination of asymmetric and symmetric cryptographic algorithms. In this paper the original BCY basic Modular Square Root (MSR) protocol and the Boyd-Mathuria modified Improved Modular Square Root (IMSR) protocol are discussed. A formal verification of these protocols using the Coffey-Saidha-Newe (CSN) modal logic is given. This verification demonstrates that protocol weaknesses can be readily detected by the use of formal verification methods.