On the logical verification of key exchange protocols for mobile communications

T. Newe, T. Coffey

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationRecent Advances in Communications and Computer Science
PublisherWorld Scientific and Engineering Academy and Society
Pages76-81
Number of pages6
ISBN (Print)9608052866
Publication statusPublished - 2003

Keywords

  • 3G mobile
  • Formal methods
  • Modal logic
  • Security protocol
  • Verification
  • Wireless communications

Fingerprint

Dive into the research topics of 'On the logical verification of key exchange protocols for mobile communications'. Together they form a unique fingerprint.

Cite this