期刊名称：Journal of Theoretical and Applied Information Technology
印刷版ISSN：1992-8645
电子版ISSN：1817-3195
出版年度：2021
卷号：99
期号：15
语种：English
出版社：Journal of Theoretical and Applied
摘要：The three-way handshake protocol is widely used especially as a part of complex communication and security systems. It is used to establish a connection between a client and a server under specific rules and constraints. In this research, we used the NuSMV model checker along with Computational Tree Logic (CTL) to verify the correctness of the three-way handshake protocol over specific correctness conditions and properties. The results showed that the proposed protocol satisfied all correctness conditions except δ_9, δ_11, and δ_1Furthermore, the proposed automated verification approach aims to verify the correctness of a finite number of clients each of them iterated infinitely often.
关键词：CTL;Model Checking;Nusmv;Three-Way Handshake Protocol;Correctness Conditions;Kripke Model
