A Fast Method for Security Protocols Verification

摘要

Internet communication is essential for everyone. Algorithms that decide about the correctness of this communication are protocols, and the central part of it that keeps all in safety are security protocols. Because every such program must be implemented and applied, errors are probable. That is why we need verification methods based on mathematical models, and we also need tools checking the new protocols, looking for undiscovered gaps. Existing verification tools and languages describing the protocols are not free of errors or imperfections. Sometimes they neglect some dependencies, and sometimes they are utterly redundant. We present in the article a formal model that we have recently developed. It describes the different behaviours and properties of security protocols. On the base of it, we implemented the tool that verifies many types of protocol, first of all, if they work and then if they meet the security requirements. At the end of the article, we provided a summary of our results with the results obtained from popular tool.