Automated verification of wireless security protocols using layered proving trees

Marian Ventuneac, Reiner Dojen, Tom Coffey

Research output: Contribution to journalArticlepeer-review

Abstract

Cryptographic protocols are designed to provide security services, such as key distribution, authentication and non-repudiation, over insecure networks. Formal verification of these protocols is an important step in their design. The manual verification of security protocols using logic-based formal methods is susceptible to human-factor errors in correctly applying logical postulates. Using automated systems, which apply the axioms of the logic as part of the proving process, has the potential to improve the verification process. This paper presents an empirical study of an automated proving system on the analysis of two wireless communication protocols. The automated system uses the CS modal logic implemented on a layered proving tree-based proving engine. The analysis demonstrates the accuracy of the automated systems in finding protocol flaws. Also the system is shown to be efficient both in terms of time and memory resources.

Original languageEnglish
Pages (from-to)252-258
Number of pages7
JournalWSEAS Transactions on Communications
Volume5
Issue number2
Publication statusPublished - Feb 2006

Keywords

  • Automated formal verification
  • Modal logics
  • Security protocol
  • Wireless communication

Fingerprint

Dive into the research topics of 'Automated verification of wireless security protocols using layered proving trees'. Together they form a unique fingerprint.

Cite this