فهرست مطالب
فصلنامه پدافند الکترونیکی و سایبری
سال پنجم شماره 4 (پیاپی 20، زمستان 1396)
- 149 صفحه، بهای روی جلد: 100,000ريال
- تاریخ انتشار: 1396/11/03
- تعداد عناوین: 9
-
- مقالات علمی - پژوهشی
-
صفحات 1-15«شبکه بات» شبکه ای از رایانه های آلوده متصل به اینترنت است که تحت مدیریت سرور فرماندهی و کنترل قرار دارد و برای حملات انکار سرویس، فرستادن هرزنامه و عملیات مخرب دیگر مورداستفاده قرار می گیرد. باوجود ویژگی های خاص هر شبکه بات، بات ها در داخل شبکه رفتارهای همسانی از خود نشان می دهند و این می تواند نقطه آغاز شناسایی یک بات در داخل شبکه باشد و با شناسایی این رفتار همگون می توان ترافیک تولیدی بات ها را از ترافیک عادی شبکه تفکیک کرد و از مشکلاتی مانند یافتن الگوریتم های رمزگشایی کانال های ارتباطی رمزنگاری شده در امان بود.
رفتار همسان بات ها در داخل شبکه بات می تواند منجر به تولید ویژگی ها و خصیصه هایی شود که بتوان با تحلیل این ویژگی ها، جریان بدخواه را از جریان سالم تشخیص داد. منطق اصلی روش استفاده شده در این پژوهش بر این پایه استوار است که شبکه های بات، الگو های ترافیکی قابل تشخیصی از خود به جای می گذارند که به کمک روش های یادگیری ماشین قابل شناسایی بوده و می توان ترافیک تولیدی توسط آن ها را از ترافیک عادی شبکه جدا کرد. در این مقاله ویژگی ها و رفتار شبکه های بات مشهور همچون Weasel در جهت تولید خصیصه ها مطالعه شد. سپس بعد از تهیه مجموعه داده های واقعی که ترکیبی از ترافیک سالم و ترافیک تولیدی توسط چندین شبکه بات مشهور است، جریان بسته ها در پنجره های زمانی 300 ثانیه ای تحلیل شده و با توجه به الگو های ترافیکی قابل تشخیص، خصیصه های مختلفی استخراج (تولید) شد. این خصیصه ها در ابزار وکا و به کمک الگوریتم های یادگیری ماشین داده کاوی شده و نتایج طبقه بندی به عنوان خروجی ارائه می شود. نتایج خروجی ها نشان دهنده نرخ تشخیص بالاتر در مقایسه باکارهای مشابه و در حدود 99 درصد می باشد. درنهایت نیز روشی برای شناسایی بلادرنگ شبکه های بات ارائه خواهد شد.کلیدواژگان: شبکه بات، تشخیص شبکه بات، سرور فرماندهی و کنترل، پنجره زمانی، یادگیری ماشین -
صفحات 17-27در این مقاله، یک روش جدید به منظور سنکرون سازی آشوب با استفاده از کنترل غیرخطی ارائه شده است. در اکثر کنترل-کننده های موجود فرض می شود مدل ریاضی سیستم های آشوبی فرستنده و گیرنده کاملا یکسان هستند. با توجه به یکسان نبودن شرایط محیطی فرستنده و گیرنده و تاثیر درجه حرارت و سایر عوامل بر پارامترهای سیستم آشوبی از قبیل مقادیر مقاومت ها و سایر المان ها، یکسان درنظرگرفتن مدل های فرستنده و گیرنده معقول نیست. در این مقاله، روش جدیدی برای تخمین عدم قطعیت ها ارائه شده است که در آن عدم قطعیت ها با یک معادله دیفرانسیل خطی با ضرایب نامعلوم ثابت مدل سازی می شود. به عبارت دیگر، عدم قطعیت ها را می توان به صورت پاسخ این معادله دیفرانسیل نمایش داد. با توجه به این که این تابع (پاسخ معادله دیفرانسیل) شرایط قضیه تقریب عمومی را دارد، می توان هر تابع غیرخطی را با دقت دلخواه تخمین زد، اما با توجه به این که ضرایب معادله دیفرانسیل نامعلوم می باشند، پارامترهای این تابع نیز نامعلوم بوده و باید تخمین زده شوند. این کار با استفاده از قوانین تطبیق به دست آمده از تحلیل همگرایی خطای سنکرون سازی انجام می گردد. نتایج شبیه سازی بیانگر عملکرد مناسب تخمین گر ارائه شده بوده و در مقایسه با کنترل کننده فازی مد لغزشی سرعت پاسخ کنترل کننده پیشنهادی بهتر می باشد. همچنین، کاربرد آن در مخابرات امن و رمزنگاری مورد بررسی قرار گرفته است.کلیدواژگان: سنکرون سازی آشوب، مخابرات امن، رمزنگاری، معادلات دیفرانسیل، قضیه تقریب عمومی
-
صفحات 29-41شبکه های نرم افزار محور برای ایجاد تغییر در معماری شبکه های سنتی با عملکرد اختصاصی جهت رسیدن به شبکه های هوشمند به وجود آمدهاند. اخیرا این نوع شبکه ها، به دلیل انعطاف پذیری در مدیریت سرویس های شبکه و کاهش هزینه های عملیاتی در بین سازمان ها محبوبیت خاصی پیدا کرده اند. در معماری این شبکه ها، سیستم عامل و برنامه های کاربردی از سطح سوئیچ های شبکه جدا شده و در یک لایه مجازی تحت عنوان کنترل کننده، متمرکز شده است. این معماری به دلیل تصمیم گیری متمرکز و محدودیت منابع کنترل کننده در معرض انواع تهدیدات ازجمله حملات منع خدمت توزیع شده قرار دارد. ما در این مقاله، معماری شبکه های نرم افزار محور و حملات منع خدمت توزیع شده در این معماری را بررسی کرده و با بهرهگیری از امکانات منحصربه فرد کنترل کننده، الگوریتم جدیدی برای تشخیص و کاهش اثر این حملات ارائه دادهایم. ما در این الگوریتم پیشنهادی از رابطه آماری فاصله هلینگر و روش تطبیق متحرک میانگین وزنی به منظور شناسایی حملات منع خدمت توزیع شده در شبکه های نرم افزار محور استفاده کرده ایم. در این مقاله، حملات منع خدمت توزیع شده در شبکه نرم افزارمحور توسط مقلد مینی نت به همراه کنترل کننده Pox شبیه سازی شده است. آزمایش ها و ارزیابی های انجام شده در این محیط، کارآیی الگوریتم پیشنهادی و برتری آن نسبت به روش های قبلی را نشان می دهند.کلیدواژگان: شبکه های نرم افزار محور، حملات منع خدمت توزیع شده، فاصله هلینگر، بخش کنترل، بخش داده
-
صفحات 43-53نهان نگاری یکی از حوزه های پرکاربرد مخفی سازی اطلاعات است که به جاسازی غیرمحسوس پیام محرمانه داخل یک پوشانه می پردازد. در این مقاله یک روش بهبودیافته برای جاسازی پیام محرمانه داخل پوشانه تصویر در حوزه مکان، براساس نظریه کدگذاری معرفی می کنیم، به طوری که فرستنده پیام محرمانه را با توجه به ماتریس کنترل مشابهت (H) کد توافقی با گیرنده، در پوشانه با کم ترین تغییر جاسازی نموده و آن را برای گیرنده ارسال می کند. حال گیرنده تنها با همان ماتریس توافقی به راحتی می تواند پیام را از پوشانه استخراج کند. در این روش جدید، ضمن برخورداری از مزایای حوزه مکان و تشخیص و تصحیح خطای رشته بیت دریافتی توسط گیرنده، می توان مقاومت را بین 94 % الی 100 %، شفافیت (PSNR) را تا 71/84 % و مشابهت (SSIM) را تا 99/9999 % افزایش داد.کلیدواژگان: نهان نگاری، پوشانه تصویری، کد خطی، ماتریس کنترل مشابهت
-
صفحات 55-67در یک طرح امضاء با تاییدکننده مشخص قوی، امضاءکننده قادر می شود تا امضاء را برای یک گیرنده خاص صادر نماید؛ یعنی تنها گیرنده مشخصی که مدنظر امضاءکننده است می تواند اعتبار امضای صادرشده را بررسی نماید. البته باید طرح امضاء به گونه ای باشد که هیچ بخش سومی قادر به بررسی اعتبار امضاء نباشد یا به عبارت دیگر، تاییدکننده مشخص نتواند امضاء را به بخش سومی منتقل کند. در این مقاله، یک طرح امضای مبتنی بر شناسه جدید با تاییدکننده مشخص جدید ارائه می کنیم که در مدل سروش تصادفی و براساس فرض BDH دارای اثبات امنیتی است. طرح ارائه شده تمامی ملزومات امنیتی یک طرح امضای با تاییدکننده مشخص را برآورده می نماید. علاوه بر آن، طرح ارائه شده ویژگی محافظت از حریم خصوصی کاربر را برآورده ساخته و همچنین به لحاظ کارآمدی از حیث اندازه امضای خروجی و محاسبات لازم برای فازهای صادرشدن امضاء و تایید آن با دیگر طرح های موجود قابل مقایسه بوده و جزو طرح های سبک وزن محسوب می شود. در نهایت نیز برخی از سناریوهای کاربردی طرح ارائه شده را در فضای اینترنت اشیاء معرفی می کنیم.کلیدواژگان: طرح امضای مبتنی بر شناسه، امضا با تاییدکننده مشخص، اینترنت اشیاء خانه هوشمند، رایانش ابری، اثبات امنیتی، زوج سازی دوخطی
-
صفحات 69-80شبکه های موردی از تعدادی گره بی سیم بدون نیاز به هیچ یک از زیرساخت های شبکه ای پیشین تشکیل می شوند. این گره ها بدون هیچ گونه زیرساختی با یکدیگر ارتباط برقرار می کنند. به دلیل ویژگی هایی مانند تغییر پویای ساختار شبکه، اعتماد پیش فرض گره ها به یکدیگر و نادیده گرفتن عملکرد گره ها، شبکه های موردی در مقابل حملات گره های مخرب محافظت شده نیستند. در این مقاله روش جدیدی با استفاده از ترکیب یک روش تشخیص مسیر امن و یک روش مقابله با گره های خرابکار در حمله سیاه چاله برای پروتکل مسیریابی AODV ارائه شده است. در مرحله اول، گره مبدا با پیداکردن بیش از یک مسیر به مقصد، اعتبار گره ای که بسته پاسخ مسیر را فرستاده است تایید می کند. هنگامی که یک بسته پاسخ مسیر به گره مبدا برسد، آن گره، مسیرهای کامل به مقصد را استخراج کرده و در انتظار یک بسته پاسخ مسیر دیگر می ماند. ایده این راه حل انتظار برای دریافت بسته پاسخ مسیر از بیش از دو گره است. در مرحله بعدی با توجه به رفتار گره ها در شبکه، رای گیری از گره های همسایه انجام شده و با استفاده از قوانین تعریف شده در مبدا به منظور تشخیص گره خرابکار، گره های خرابکار شناسایی و حذف می شوند. نتایج شبیه سازی با استفاده از نرم افزار OMNet نشان دهنده بهبود قابل توجه الگوریتم پیشنهادی نسبت به نسخه اصلی پروتکل AODV که دچار حمله شده است، می باشد.کلیدواژگان: شبکه موردی، پروتکل مسیریابی بردار فاصله مبتنی بر تقاضا، حمله سیاه چاله، مسیر امن
-
صفحات 81-93موتورهای جستجو را می توان بهترین ابزار کارآمد برای مدیریت، بازیابی و استخراج اطلاعات مهم از مجموعه عظیم داده های وب معرفی کرد. این موتورها پهنه وسیع وب را به طور زمان بندی شده پیمایش می کنند و به جمع آوری صفحات بی شمار ذخیره شده در گوشه کنار وب می پردازند. ارائه دهندگان موتورهای جستجو همواره به دنبال بهبود ارتباط نتایج و کاهش زمان پاسخ به کاربران هستند، اما هر دو این موارد می تواند تحت تاثیر ترافیک خودکار ارسال شده از سوی ربات ها قرار گیرد. در این مقاله ابتدا به تعریف ربات ها و چالش تشخیص آن ها پرداخته شده است. سپس، روشی با نام بوف برای تشخیص ربات های جستجو ارائه شده است. در روش بوف برای دستیابی به دقتی بالا در تشخیص ربات های ناهنجار، از پارامترهای مختلف و نسبتا زیادی برای مدل کردن رفتار کاربران استفاده شده است. پس از تعیین اولویت پارامترها در تشخیص ماهیت کاربران، درخت تصمیمی ساخته شده و اقدام به دسته بندی کاربران در گروه-های انسان، ربات مخرب، ربات مجاز و نامشخص می کند. ربات های تشخیص داده شده در درخت تصمیم، بخش دیگری از سامانه تشخیص ربات را فعال می کند که قادر است با توجه به الگوی رفتاری شبکه های رباتی، حتی ربات هایی با نرخ درخواست پایین را نیز شناسایی کند. ارزیابی روش پیشنهادی بر روی داد های آزمون، صحت 97/7درصدی را در تشخیص ماهیت کاربران نشان می دهد که حداقل بهبود دقت 9/9 درصدی را نسبت به روش های بررسی شده در این حوزه نشان می دهد. رقم قابل توجهی که در هر روز تصمیم گیری در مورد 2230 کاربر را تحت تاثیر قرار می دهد.کلیدواژگان: موتور جستجو، ربات جستجو، تحلیل لاگ، تشخیص ربات، درخت تصمیم
-
صفحات 95-108یکی از حوزه های امنیتی که در شرایط جدید جهانی بسیار مورد اهمیت قرار گرفته است، امنیت سایبری است. در این تحقیق برای مطالعه بر روی حملات ناشناخته در شبکه های کامپیوتری، دو هانی نت آزمایشگاهی مجازی در دو مکان مختلف طراحی شده و همچنین از سایر مجموعه داده های علمی استفاده گردیده است. در داده های شبکه ای، مشکل داده های نامتوازن اغلب اتفاق می افتد و موجب کاهش کارایی در پیش بینی برای رده هایی که در اقلیت هستند، می گردد. در این مقاله برای حل این مشکل، از روش های یادگیری جمعی استفاده گردیده است تا بتوان مدلی اتوماتیک ارائه نمود که با استفاده از تکنیک های مختلف و با استفاده از یادگیری مدل، حملات شبکه به ویژه حملات ناشناخته را شناسایی نماید. روش های جمعی، برای توصیف مشکلات امنیت کامپیوتر بسیار مناسب می باشند زیرا هر فعالیتی که در چنین سیستم هایی انجام می گیرد را در سطوح چند انتزاعی می توان مشاهده کرد و اطلاعات مرتبط را نیز می توان از منابع اطلاعاتی چندگانه جمع آوری نمود. روش تحقیق بر اساس تحلیل های آماری جهت برسی میزان صحت و درستی نتایج و میزان اتکاپذیری آن ها صورت گرفته است. در این مرحله به کمک تکنیک ها و آزمایش های آماری نشان داده ایم که عملکرد الگوریتم طراحی شده با رای گیری وزنی پیشنهادی براساس الگوریتم ژنتیک نسبت به دوازده طبقه بند دیگر بهتر می باشد.کلیدواژگان: حملات ناشناخته، یادگیری جمعی، داده های نامتوازن، رای گیری وزنی، تست های آماری
-
صفحات 109-129در این مقاله، ساختار نسخه های مختلف پروتکل امنیتی تترا در «مدل صوری» و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر مورد ارزیابی قرار می گیرند. پروتکل امنیتی شبکه تترا از نوع پروتکل های تبادل کلید تصدیق شده است که در آن، طرفین ضمن احراز هویت یکدیگر، یک کلید نشست نیز می سازند. این پروتکل همچنین از کلیدهای محرمانه از پیش توزیع شده استفاده می کند که مبتنی بر ساز و کارهای رمزنگاری متقارن است. تحلیل امنیتی پروتکل مذکور در «مدل صوری» و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر انجام شده است. در ابتدا، هشت ویژگی امنیتی: محرمانگی، احراز هویت، امنیت پیشرو، امنیت کلید ناشناخته، کلید نشست یکسان، امنیت کلید معلوم، گمنامی و تمامیت را در بستر این ابزارها مدل سازی نموده و سپس با استفاده از هر دو ابزار، امنیت پروتکل مذکور را نسبت به این ویژگی ها مورد بررسی قرار می دهیم. مقایسه نتایج حاصل از تحلیل صوری این ویژگی ها با نتایج حاصله از تحلیل های غیرصوری در منابع آشکار دلالت بر وجود ضعف هایی جدید در ویژگی های «امنیت پیشرو» و «تمامیت» در ساختار این پروتکل دارد. در نهایت، روش-هایی برای غلبه بر این ضعف ها ارایه شده است.کلیدواژگان: تحلیل امنیتی، مدل های صوری، ابزار تحلیل خودکار، شبکه تترا
-
Pages 1-15Botnet" is a network of infected computers connected to the Internet that is under management of the command and control server and is used for denial of service attacks, for sending spams and other malicious operations. The size of a botnet depends on the complexity and number of computers employed. Users usually do not know that their systems are remotely controled and abused. Botnets are attractive for cyber criminals, because they are capable of being reset for various offenses, moved to new hosting services, or they are reprogrammed in response to new developments in security. Despite the specific characteristics of each botnet, bots in a botnet exhibit homogeneous behaviors and this can be the starting point for identifying a botnet within a network. Discoverable behavior of bots in a botnet can lead to production of features and attributes. Analyzing of these features, we can classify traffic to malicious and non-malicious traffic.This approach uses network flow analysis and machine learning methods to detect peer to peer botnets. Furthermore,this approach is flow-based and analyzes features extracted from flows based on the behavior of well-known botnets such as Weasel, etc and determines that the new traffic is an attack or not.Keywords: Botnet, Bot, Peer to Peer Botnet, Network Flow Analysis, Machine Learning
-
Pages 17-27In this paper, a new method has been presented for chaos synchronization using a nonlinear controller. In most so-far presented approaches, it is assumed that the mathematical models of the transmitter and reciever are completely the same. Due to the non-identical environmental circumstances in the transmitter and receiver and the influence of temperature on the chaotic system parameters, this assumption is not true. In this paper, a novel approach, in which uncertainties are modeled by a linear diffential equation with unknown constant coefficients, has been presented for estimation of these uncertainties . Since this function satisfies the conditions of the universal approximation theorem, it can estimate nonlinear functions with arbitrary small approximation error. However, since the coefficients are unknown, the parameters of these functions are unknown and should be estimated using the adaptation laws derived from the synchronization analysis. Simulation results verify the effectiveness of the proposed estimator. In comparison with other controllers such as fuzzy sliding mode controllers, the proposed controller response is faster. Moreover, its application in secure communications and cryptography has been studied, as well.Keywords: Chaos Synchronization, Secure Communication, Cryptography, Differential Equations, The Universal Approximation Theorem
-
Pages 29-41Software defined network (SDN) was born to make changes to existing network architectures and devices with specific function to reach an intelligent network. Recently, this networks have gained popularity in enterprise networks because of the flexibility in network service management and reduced operational cost. In this architecture, operating system and applications from the network switch are decoupled. They centralized in a virtual layer that called the controller. In the SDN, due to the centralized decision-making and resources controller limitations are exposed to all kinds of threats such as Distributed Denial of Service (DDoS) attacks. In this paper we will review SDN architecture and DDOS attacks in SDN. We proposed a novel detection and mitigation algorithm that takes advantage of unique features of the SDN architecture. In the proposed algorithm, for detecting DDOS attacks in SDN, a statistical method based on Hellinger distance and Exponential Weighted Moving Average (EWMA) technique are used. In this paper, DDOS attacks in SDN is simulated by MiniNet emulator with Pox controller. Our experiments performed in the simulator, showed the efficiency of the proposed method and its superiority compared to previous approaches.Keywords: Software Defined Networks, Distributed Denial of Service, Hellinger distance, Control plane, Data plane
-
Pages 43-53Steganography is an information hiding application which aims to hide secret messages imperceptibly into commonly used media. In this paper, we describe an Optimal embedding method based on linear codes that conforms to least significant bit, that is, the secret data is embedded into a cover message by parity check matrix. The new method not only benefits from the field of location and detection and error correction bit stream received by the receiver, but also can increase the Resistance between 94% to 100%, the transparency (PSNR) up to 84/71, and the similarity (SSIM) up to % 9999/99.Keywords: Steganography, Image Cover, Linear Code, Parity Check Matrix
-
Pages 55-67In a strong designated verifier signature scheme, a signer can issue a signature for a special receiver; i.e. only the designated verifier can verify the validity of the issued signature. Of course, the signature scheme should be such that no third party will be able to validate the signature. In other words, the designated verifier cannot transfer the issued signature to a third party. In this article, we propose a new ID -based designated verifier signature scheme that has provable security in the random oracle model and BDH assumption. The proposed scheme satisfies all security requirements of an IDVSS. In addition, the proposed scheme protects from user's privacy and from the efficiency point of view, and more precisely, in terms of parameters such as the size of output signature and computations required for signing and verification phases. As a result,our proposed scheme is comparable with other existing schemes; in other words, the proposed scheme is a light-weight construction. Finally, we introduce some practical scenarios of the proposed scheme in the Internet of Things concept.Keywords: ID-Based Signature Scheme, Designated Verifier Signature, Internet Of Things, Smart Home, Cloud, Provable Security, Bilinear Pairing
-
Pages 69-80Ad hoc networks include some wireless nodes which do not need any pre-existing networks substructure. The nodes communicate to each other without any infrastructure. Because of some specifications such as dynamic changes of networks structure, presumptions trust each other and ignore the node's actions, Ad hoc networks are not protected against attacks of destructive nodes. In this study, a new method has been represented by combining a safe route detection method and an opposition method to destructive nodes to black hole attack countermeasure in AODV routing protocol. At the first step, the source node confirms the validity of the route reply packet sender's node by finding more than one route to the destination. When a route reply packet arrives to a source node, then that node extracts the complete route to destruction and waits for other packs of route reply. The idea of this solution is waiting to receive route reply packet from more than two nodes. In the next step, according to nodes manner in the network, a voting from neighboring nodes has been done and by use of predefined rules, destructive nodes are identified and destroyed. Simulations results of OMNet simulator show some improvements of the proposed algorithm to the original AODV protocol which has been attacked by the black hole.Keywords: Ad Hoc Network, AODV Routing Protocol, Black Hole Attack, Safe Path
-
Pages 81-93Search engines can be introduced as a best tool for managing, retrieving and extracting important information from a massive set of web data. These engines are scheduled to search the vast web environment and collect countless pages stored in every corner of the web. Search engines providers are always looking for improving the relationship between the results and reducing response times to users, but both of these can be influenced by the automated traffic sent by the bots. This article first defines bots and challenges of detecting them. Then, it provides a method named boof for detecting Search robots. In the boof method, to achieve high accuracy in detecting anomaly robots, many different parameters are used to model the users behavior. After determining the priority of parameters in detecting users, decision tree is made and attempted to categorize users into groups of humans, bots, legal bots and the unknown. Robots detected in the decision tree, enable another part of the robot detection system to identify robots even with low request rate. This is done by detecting the botnet behavior pattern . Evaluation of the proposed method on test data shows 97.7 percent accuracy in recognizing users that this improves the accuracy of at least 9,9 percent compared to the methods examined previously in this area. This is a significant digit that influences decision-making about 2230 users during each day.Keywords: Search Engine, Search Robot, Log Analysis, Bot Detection, Decision Tree
-
Pages 95-108Security is a significant issue in this world and is given several dimensions by varying circumstances. Among different security areas, cyber security can be claimed to have one of the most important places in new circumstances of this world. In this study, two virtual honeynets were designed in two different laboratories to help study unknown attacks. Other scientific datasets were also used for this purpose. Imbalanced data always cause problems for network datasets and reduce the efficiency for the prediction of minority classes. To cope with this problem, ensemble learning methods were applied in order to detect network attacks, and most specifically, unknown attacks, while taking advantage of different techniques and action model learning. Statistical analysis was used as the research method in order to measure the reliability and validity of the findings. Finally, statistical techniques and tests were applied to show that the algorithm designed by weighted voting that is based on the genetic algorithm has a better performance than other twelve classifiers. According to the Fisher's criterion, the proposed approach was in the first place in the actual laboratory context and in the second place in the standard data set.Keywords: Honey-Net, Unknown Attacks, Ensemble Learning, Imbalanced Data, Weighted Voting, Statistical Tests
-
Pages 109-129In this paper, the structure of the various versions of the TETRA security protocol is investigated in the formal model using Proverif and Scyther automatic analysis tools. The TETRA's network security protocol is a key-exchange one, in which two parties also establish a session key while authenticating each other. This protocol also uses pre-distributed secret keys which are based on the symmetric-encryption schemes. The security analysis of the protocol has been done in the formal model, using the Proverif and Scyther automatic analysis tools. Firstly, eight security features including Confidentiality, Authentication, Forward Secrecy, Unknown Key-Share security, Identical Session Key, Unknown Key Security, Anonymity, and Integrity are modeled in these frameworks, and then using both of the two tools, the security of the protocol is investigated regarding the mentioned features. Comparing the results of the formal analysis of these features with the informal analysis resulted from the open sources indicates that there are new security flows in the structure of the protocol respect to Forward Secrecy and integrity. Finally, several solutions are suggested to overcome these weaknesses.Keywords: Security Analysis, Formal Models, Automatic Analysis Tools, TETRA Network
©2000-2024 magiran.com All Rights Reserved.