جلسه دفاع پایان نامه دکتری- گرايش نرم افزار-شرر احمدي

منطق‌های دانش مختلفی برای درستی‌یابی صوری پروتکل‌های تصدیق اصالت طراحی شده‌اند. این منطق‌ها به استدلال در مورد دانش عامل‌های درگیر در اجرای پروتکل می‌پردازند. با وجود این گاهی تنها استفاده از عملگر دانش برای تحلیل این پروتکل‌ها کافی نیست و باید بُعد زمان به یک منطق دانش افزوده شود. از طرف دیگر، منطق‌های دانشی که از معناشناسی کریپکی استاندارد استفاده می‌کنند همه‌چیزدانی منطقی دارند که بر اساس آن عامل‌ها تمام نتایج منطقی حاصل از آن‌چه را که می‌دانند را می‌دانند. درستی‌یابی پروتکل‌های تصدیق اصالت با استفاده از چنین منطق‌هایی ممکن است منجر به قضاوت‌های نادرست شود زیرا همه‌چیزدانی منطقی، محدودیتی را که روی دانش عاملی که یک پیام رمزشده را دریافت می‌کند ولی کلید مناسب را برای استخراج اطلاعات از پیام رمزشده ندارد زیر پا می‌گذارد. تلاش‌هایی جهت حل این مشکل  صورت گرفته اما هیچ منطق زمانی دانشی برای درستی‌یابی پروتکل‌های تصدیق اصالت ارائه نشده است که هم صحیح و تمام بوده و هم مشکل  همه‌چیزدانی را نداشته باشد. در این رساله یک منطق دانش فارغ از همه‌چیزدانی را با عملگرهای زمانی بسط داده و صحت و تمامیت  منطق حاصل را اثبات می‌کنیم و نشان می‌دهیم که این منطق در تحلیل برخی پروتکل‌های تصدیق اصالت که نمی‌توان با منطق‌های مشابه آن‌ها را درستی‌یابی کرد مفید است. مهم‌ترین بحث چالش‌برانگیز رساله پیدا کردن مدل‌هایی شهودیست به نحوی‌که تمامیت منطق همچنان قابل اثبات باقی بماند. چنین مدل‌هایی باید به صورت طبیعی بازتابی از مفهوم اجرای پروتکل باشند، به همین جهت معناشناسی را در قالب درستی روی حالت‌های ممکن صورتی از مدل کریپکی که بر پایه‌ی سامانه‌ی تفسیر‌شده‌ی مبادله‌ی پیام است تعریف می‌کنیم. در ادامه نیز با توجه  به این معناشناسی به بررسی مدل مهاجم و استنتاج پیام در درستی‌یابی پروتکل‌های تصدیق اصالت می‌پردازیم.

ضميمه

ضميمه

ارسال کننده خبر: مهندسي کامپيوتر و فن اوري اطلاعات| | تاريخ: ۱۳۹۶/۱۱/۱۶