وارسی ویژگی های زمانی پروتکل های امنیتی با رویکرد منطق زمانی PS-LTL
محل انتشار: سومین کنفرانس بین المللی فناوری اطلاعات و دانش
سال انتشار: 1386
نوع سند: مقاله کنفرانسی
زبان: فارسی
مشاهده: 1,351
فایل این مقاله در 8 صفحه با فرمت PDF قابل دریافت می باشد
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
ICIKT03_013
تاریخ نمایه سازی: 22 فروردین 1387
چکیده مقاله:
در این مقاله، مدل تحلیل صحت و آسیب پذیری Analyze به گونه ای گسترش داده شده است که بتوان ویژگی های وابسته به زمان را نیز توصیف و وارسی کرد . در مدل گسترش یافته، فرایند تحلیل صحت و آسیب پذیری در دو فاز و شش مرحله انجام می شود . در فاز اول قدم های یک پروتکل به صورت یک مجموعه قواعد، توصیف شده و آنگاه ویژگی های صحت این پروتکل وارسی
می شود . در فاز دوم برای توصیف ویژگی های زمانی، از منطق زمانی PS-LTL استفاده می شود و برای وارسی این ویژگی ها قدم های پروتکل به دستگاه حل محدودیت بهبود یافته نگاشت می شود و سپس ویژگی های امنیتی وابسته به زمان با روش حل محدودیت، وارسی می گردد . به عنوان نمونه، پروتکل توافق کلید EKE در مدل گسترش یافته وارسی شده و یک حمله نشست موازی برای آن اثبات شده است .
کلیدواژه ها:
نویسندگان
سعید جلیلی
گروه مهندسی کامپیوتر، دانشکده فنی و مهندسی، دانشگاه تربیت مدرس
سیدمهدی سجادی
گروه مهندسی کامپیوتر، دانشکده فنی و مهندسی، دانشگاه تربیت مدرس
مراجع و منابع این مقاله:
لیست زیر مراجع و منابع استفاده شده در این مقاله را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود مقاله لینک شده اند :