Formal Verification of Authentication and Confidentiality for TACACS plus Security Protocol using Scyther

Designing a perfect security protocol is a difficult task and requires a good effort and knowledge of Cryptography which is an art of secret writing. In order to achieve high reliability of security protocols, the testing technique is not suitable, because the testing technique has got many drawbacks. To achieve high reliability of security protocols, proving the correctness of security protocols is very much essential. To prove and verify the correctness of security protocols the Formal Verification technique is the best solution because it provides the mathematical proof for the correctness of security protocols. TACACS+ (Terminal Access Controller Access-Control System Plus) [6] is one the important security protocol used by most of the Cisco network communication devices to provide Authentication, Authorization, and Accountability (popularly known as AAA services) services to the host devices. In the proposed work, the TACACS+ security protocol is formally verified using the Model Checking technique. Using the Scyther [12] model checker the Confidentiality and Authentication security properties of TACACS+ security protocol is successfully verified.