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 language | English |
---|---|
Pages (from-to) | 252-258 |
Number of pages | 7 |
Journal | WSEAS Transactions on Communications |
Volume | 5 |
Issue number | 2 |
Publication status | Published - Feb 2006 |
Keywords
- Automated formal verification
- Modal logics
- Security protocol
- Wireless communication