|
Methods of analyzing and proving the security of security protocols
|
MOhammad Dakhilalian *   , Masomeh Safkhani , Fatemeh Pirmoradian |
| Isfahan University of Technology |
|
|
Abstract: (1004 Views) |
Providing all remote services requires mutual authentication of participating parties. The framework by which this authentication is done is called authentication protocols. In other words, cryptographic or cryptographic protocol is a distributed cryptographic algorithm that establishes interactions between at least two or more hosts with a specific purpose. In fact, these protocols have provided secure and insecure channels for communication between the parties participating in the protocol. Usually, secure channels are used for registration and insecure channels for mutual authentication. After registering on the server and verifying its identity by the server, the user can benefit from the services provided by the server. Many authentication protocols have been proposed in fields such as e-medical care, Internet of Things, cloud computing, etc. The privacy and anonymity of users in these plans is the biggest challenge in implementing a platform to benefit from remote services. Due to the fact that authentication of users takes place on the insecure platform of the Internet, it can be vulnerable to all existing Internet attacks. In general, there are two methods to analyze and prove the security of authentication protocols. Formal method and In-formal method. The In-formal method, which is based on intuitive arguments, analyst's creativity and mathematical concepts, tries to find errors and prove security. While the formal method, which is done both manually and automatically, has used a variety of mathematical logics and automatic security analysis tools. Manual method using mathematical models such as Real Or Random and mathematical logics such as BAN logic, GNY logic, etc., and automatic method using AVISPA, Scyther, ProVerif, TAMARIN, etc. tools. In fact, the methods of proving and analyzing the security of security protocols are divided into two general categories based on proof of theorem and model verification, and in this article, the details of each of these methods of proving security are explained. It should be noted that most of the security protocol verification tools are based on model verification. The methods based on model checking and then the methods based on proving the theorem are described.
|
|
| Keywords: Authentication protocols, ProVerif, TAMARIN, AVISPA, Scyther security analysis tools, BAN logic, GNY logic |
|
|
Full-Text [PDF 2147 kb]
(818 Downloads)
|
Type of Study: Review Article |
Subject:
Special
Received: 2023/12/18 | Accepted: 2024/03/11 | Published: 2024/03/26
|
|
|
|
|
|
|
| Send email to the article author |
|
|
|
| Add your comments about this article |
|
|
|
