Biannual Journal Monadi for Cyberspace Security (AFTA)

fa مروری بر روش های تحلیل و اثبات امنیت پروتکل های امنیتی Methods of analyzing and proving the security of security protocols رمز و امنیت اطلاعات Cryptology and Information Security مروری Review Article ارائه تمامی خدمات از راه دور مستلزم احراز اصالت متقابل طرفین شرکت‌کننده است. چارچوبی که این احراز اصالت به وسیله آن انجام‌ می‌شود، پروتکل‌های احراز اصالت نام دارد. به‌عبارتی، پروتکل‌ رمزنگاری یا رمزنگاشتی یک الگوریتم رمزنگاری توزیع ‌شده است که بین حداقل دو یا چند هستار با یک هدف مشخص تعاملاتی را برقرار می‌نماید. درواقع، این پروتکل‌ها کانال‌های امن و ناامنی برای ارتباط بین طرفین شرکت‌کننده در پروتکل فراهم‌‌ نموده‌اند. معمولاً از کانال‌های امن جهت ثبت‌نام و از کانال‌های ناامن جهت احراز اصالت متقابل استفاده‌ می‌شود. کاربر بعد از ثبت‌نام در سرور و تأیید اصالت آن توسط سرور می‌تواند از خدماتی که سرور ارائه می‌دهد بهره‌مند شود. پروتکل‌های احراز اصالت بسیاری در زمینه‌هایی مانند مراقبت ‌پزشکی ‌الکترونیکی، اینترنت ‌اشیاء، محاسبات ابری و غیره ارائه ‌شده‌ است. حریم‌ خصوصی و گمنامی کاربران در این طرح‌ها، بزرگ‌ترین چالش در پیاده‌سازی بستر جهت بهره‌مندی خدمات از ‌راه‌ دور است. به ‌دلیل اینکه احراز اصالت کاربران در بستر ناامن اینترنت اتفاق ‌می‌افتد، پس نسبت به تمامی حملات اینترنتی موجود می‌تواند آسیب‌پذیر باشد. به ‌طور ‌کلی دو روش جهت تحلیل و اثبات امنیت پروتکل‌های احراز اصالت وجود دارد. روش صوری و روش غیرصوری. روش غیرصوری که مبتنی بر استدلال‌های شهودی، خلاقیت تحلیلگر و مفاهیم ریاضی است، سعی و تلاش در جهت یافتن خطاها و اثبات ‌امنیت دارد. درحالی‌که روش صوری که به دو صورت دستی و خودکار انجام‌ می‌شود، از انواع منطق‌های ریاضی و ابزارهای تحلیل امنیت خودکار استفاده نموده است. روش دستی با استفاده از مدل‌های ریاضی مانند مدل پیشگوی تصادفی و منطق‌های ریاضی مانند منطق BAN، منطق <m:r><m:rpr><m:scr m:val="roman"><m:sty m:val="p"></m:sty></m:scr></m:rpr>GNY</m:r> <img alt="" id="_x0000_i1025" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAACgAAAAXCAIAAAD2sJpCAAAAAXNSR0IArs4c6QAAAAlwSFlzAAAdhwAAHYcBj+XxZQAAAc1JREFUSEvtVr1uwjAQNt3DS6SiC0t5gWSLxFp1ZWFMGBirzIgRCbOysCLWKnmJTCyg+CV4gdRnn4kvCYiAVBZuCGB/d993PznRKYqCPcPenkEKnC/if6s8KbVII9/vns33I86FQC2Cn6+i1NZnXfgSXsK6XfnbIO1z5S+nWlm+9BzH8cIkNwdJKA+cMDEI+amPqqfo7C3RNUcYcTXeBoXEDSSIJN6gzvNAIRWkFFlInUUFo5yNuEIRY7bnQytH+hWAYaJVljEuSSQYSiuXRxtepRASq1FXMga5tIg1AAxXfsjks99zbxrp/VGwYLUdMZbFCzJl1D2YzgaMbeYwX4LPN6PtKrAQ9y4QDPtNB5xQu5MfrY7zccxmU5v2gc3lTtYqo2vUqC6WtOtJpZ6XMk6j8n2+kJXOCIvZ3CWEDL6GtTYC8fuHlM6gd6UFqxO0kbHR9kR6YzOYVo/58abxsEFA7Pb68pntfm1mo+d6REO927dlVqXWvagx3xQLfeG9aGW6x3pSsvjT5ymmLdJFXIumXzxqOGXNrOIIpcgOef26XE1yxeptqMwLl0mC+8Ja5o2rWi+L6mrGvWkCVq47r78+rSbkAfC9K/MBSu36Bz5TKWBG4IPZAAAAAElFTkSuQmCC" style="width:15pt; height:8.65pt" >  و غیره و روش خودکار با استفاده از ابزارهای اویسپا، سایتر، پرووریف، تامارین و غیره انجام ‌شده است. در واقع روش‌های اثبات و تحلیل امنیت پروتکل‌های امنیتی به دو دسته کلی مبتنی بر اثبات قضیه و وارسی ‌مدل تقسیم ‌شده‌اند، که در این مقاله جزئیات هرکدام از این روش‌های اثبات و تحلیل امنیت، تحلیل امنیت پروتکل <m:r><m:rpr><m:scr m:val="roman"><m:sty m:val="p"></m:sty></m:scr></m:rpr>ECCPWS </m:r> <img alt="" id="_x0000_i1025" src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAFMAAAAXCAIAAAD4GeQtAAAAAXNSR0IArs4c6QAAAAlwSFlzAAAdhwAAHYcBj+XxZQAAAuFJREFUWEftWD1uKjEQdl4fLrFR0qSBC+x2K0VKFdHSvHKhSJ2a+knACbZFVEjR0u0JoElDtHsJLrDP9thmxtiOEylNNtPh/eyZb/485qrrOtZL+dNL1oL0L/P+hb6/MWdd1yzSa6+ki4b3QCRNVaQIn6bForIgnR/j1oUOoYCiQpqrQljpWALj9Qeq3GmfPJQzF+I4tamERwhzMCstNFWhxDbmY4yti58iTdeqFHnb59onhLqOm16UR5mdQIE6y7hSMYdjrUOFP5B+h3dAMdoWg3HoUtyJ/ZY1Jhksj4itxGf0u2UfSqEgc5LlEG87+WklRGDsKLlyTuUN1iWW0sVlfGBdlRuNOK3Si1++DrebDqY71PDb182esdHTQ+K/BWIwUXdI8vA0Ymy/eW0NvDnuuXK5Xm7PhgmVllFkW0Cdm3m725Z0E9fMF+5vA8RZDMZtCqibPObqs6J+bDScAwTB5Paer7y9a49YxPPnufDYyzCb7s5O87AnzMvxAGQ4tohHheproHa3zIS60fxZE2cMKJroKuKM5Y8TlAwXEU9m9WE+GbF9OR4OsjB/wnyyPoEc1lzB9wry8oZN5utDPcP5JCnq6IqUUOl2cyeiCsngSHXus9mqPnD7OX3B38/ene0JKP5OMV4+nep6NcvtMgKKstTb9zdTCVAHMt+dxKXJSZKvah4+nvuc/d+lM/N9HS5fnVbn5GNMGoIqzOWUGEy0M8+lLhiiFiDqQHoEmp6/8ST5rBa5u3/5h3u1tiA4vbbLLFMOg8IL980YTDRzBtTL7ZIQ16V+bEzth46EYDglxBxuKSWqb+KbRtbaMjtffzGYT1CHRr7h99bdDdom2ZTjsez2+DhiC/pAt5sPgemVTIIcZ8bKwPQagYGBLTwTYasuoJ7xVtmXmndEcHgVc/tnXiwXbxH+YFk09MUSwlBdH7L3DGW+WY1TLfB7yv9c4Z69+v03Kr7+fgiyv/9M9Jf5f7848wKXIFnHAAAAAElFTkSuQmCC" style="width:31.15pt; height:8.65pt" >  با برخی از این روش‌ها و در نهایت مقایسه این روش‌ها با یکدیگر از لحاظ نقاط قوت، نقاط ضعف و غیره بیان ‌‌‌شده ‌‌است. در این مقاله، روش‌های مبتنی ‌بر وارسی ‌مدل و سپس روش‌های مبتنی بر اثبات قضیه شرح ‌داده ‌می‌شود. <div>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.</div>   پروتکل‌های احراز اصالت, ابزار تحلیل امنیت پرووریف, ابزار تحلیل امنیت تامارین, ابزار تحلیل امنیت اویسپا, ابزار تحلیل امنیت سایتر ,منطق BAN, منطق GNY Authentication protocols, ProVerif, TAMARIN,AVISPA, Scyther security analysis tools, BAN logic, GNY logic 112 136 http://monadi.isc.org.ir/browse.php?a_code=A-10-430-1&slc_lang=fa&sid=1 MOhammad Dakhilalian سیدمحمد دخیل علیان mdalian@iut.ac.ir 10031947532846001720 10031947532846001720 Yes Isfahan University of Technology دانشکده مهندسی برق و کامپیوتر، دانشگاه صنعتی اصفهان، اصفهان، ایران Masomeh Safkhani معصومه صفخانی Safkhani@sru.ac.ir 10031947532846001721 10031947532846001721 No Shahid Rajaee Teacher Training University دانشکده مهندسی کامپیوتر، دانشگاه تربیت دبیر شهید رجائی، تهران، ایران Fatemeh Pirmoradian فاطمه پیرمرادیان f.pirmoradian@ec.iut.ac.ir 10031947532846001722 10031947532846001722 No Isfahan University of Technology دانشکده مهندسی برق و کامپیوتر، دانشگاه صنعتی اصفهان، اصفهان، ایران