• وارسی ویژگی های زمانی پروتکل های امنیتی با رویکرد منطق زمانی ps-ltl

    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1386/01/01
    • تاریخ انتشار در تی پی بین: 1386/01/01
    • تعداد بازدید: 670
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
    در این مقاله، مدل تحلیل صحت و آسیب پذیری analyze به گونه ای گسترش داده شده است که بتوان ویژگی های وابسته به زمان را نیز توصیف و وارسی کرد. در مدل گسترش یافته، فرایند تحلیل صحت و آسیب پذیری در دو فاز و شش مرحله انجام می شود. در فاز اول قدم های یک پروتکل به صورت یک مجموعه قواعد، توصیف شده و آنگاه ویژگی های صحت این پروتکل وارسی می شود. در فاز دوم برای توصیف ویژگی های زمانی، از منطق زمانی ps-ltl استفاده می شود و برای وارسی این ویژگی ها قدم های پروتکل به دستگاه حل محدودیت بهبود یافته نگاشت می شود و سپس ویژگی های امنیتی وابسته به زمان با روش حل محدودیت، وارسی می گردد. به عنوان نمونه، پروتکل توافق کلید eke در مدل گسترش یافته وارسی شده و یک حمله نشست موازی برای آن اثبات شده است.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها