Abstract: This paper demonstrates a comprehensive analysis method using formal methods such as finite-state machine. First, we describe the modified version of our new protocol and briefly explain the encrypt-then-authenticate mechanism, which is regarded as more a secure mechanism than the one used in our protocol. Then, we use a finite-state verification to study the behaviour of each machine created for each phase of the protocol and examine their behaviours together. Modelling with finite-state machines shows that the modified protocol can function correctly and behave properly even with invalid input or time delay.

Dania Aljeaid, Xiaoqi Ma and Caroline Langensiepen, “Analysis of Security Protocols using Finite-State Machines” International Journal of Advanced Research in Artificial Intelligence(IJARAI), 4(4), 2015. http://dx.doi.org/10.14569/IJARAI.2015.040407

@article{Aljeaid2015,
title = {Analysis of Security Protocols using Finite-State Machines},
journal = {International Journal of Advanced Research in Artificial Intelligence},
doi = {10.14569/IJARAI.2015.040407},
url = {http://dx.doi.org/10.14569/IJARAI.2015.040407},
year = {2015},
publisher = {The Science and Information Organization},
volume = {4},
number = {4},
author = {Dania Aljeaid and Xiaoqi Ma and Caroline Langensiepen}
}