ارزیابی منطقی و صوری یک پروتکل احراز هویت برای شهرهای هوشمند

با توجه به نیاز روزافزون به طراحی و ارزیابی انواع پروتکلهای امنیتی برای راه اندازی شهرهای هوشمند، ارائه روشهای کارآمدی که بتوانند اطمینان لازم از صحت این پروتکل ها را ایجاد کنند، بسیار ضروری است. منطق باروز-ابادی-نیدهام، معروف به منطق BAN اولین منطق باور است که به طور گسترده ای برای تجزیه و تحلیل صوری کامل بودن پروتکل ها مورد استفاده قرار گرفته است. تلاش های زیادی نیز به منظور غلبه بر محدودیتهای آن صورت گرفته و منطق GNY (گونگ-نیدهام-یاهالوم)، به عنوان یکی از مشهورترین تعمیم های منطق BAN، به شکل موفقیت آمیزی افزونگی ها و یا نقص های موجود در پروتکلهای مختلف را آشکار کرده است. بنابراین، ما در این مقاله قصد داریم به منظور ارزیابی فرمال یک پروتکل احراز هویت که برای حفظ حریم خصوصی در شهرهای هوشمند قابل استفاده است، ضمن توصیف اهداف، گزاره ها و فرضیات مورد نیاز، از منطق GNY استفاده کنیم. نتیجه ارزیابی های ما نشان میدهد که پروتکل مذکور از امنیت لازم برخوردار بوده و مهاجمین با استفاده از حملات مرسوم قادر به نفوذ، ردیابی، جعل هویت، تزریق اطلاعات نادرست یا تحریف اطلاعات نیستند.

Keywords:

ارزیابی منطقی پروتکل , درستی یابی صوری , منطق BAN , منطق GNY , کانال امن.