سال انتشار: ۱۳۸۶

محل انتشار: سومین کنفرانس بین المللی فناوری اطلاعات و دانش

تعداد صفحات: ۸

نویسنده(ها):

سعید جلیلی – گروه مهندسی کامپیوتر، دانشکده فنی و مهندسی، دانشگاه تربیت مدرس
سیدمهدی سجادی – گروه مهندسی کامپیوتر، دانشکده فنی و مهندسی، دانشگاه تربیت مدرس

چکیده:

در این مقاله، مدل تحلیل صحت و آسیب پذیری Analyze به گونه ای گسترش داده شده است که بتوان ویژگی های وابسته به زمان را نیز توصیف و وارسی کرد . در مدل گسترش یافته، فرایند تحلیل صحت و آسیب پذیری در دو فاز و شش مرحله انجام می شود . در فاز اول قدم های یک پروتکل به صورت یک مجموعه قواعد، توصیف شده و آنگاه ویژگی های صحت این پروتکل وارسی
می شود . در فاز دوم برای توصیف ویژگی های زمانی، از منطق زمانی PS-LTL استفاده می شود و برای وارسی این ویژگی ها قدم های پروتکل به دستگاه حل محدودیت بهبود یافته نگاشت می شود و سپس ویژگی های امنیتی وابسته به زمان با روش حل محدودیت، وارسی می گردد . به عنوان نمونه، پروتکل توافق کلید EKE در مدل گسترش یافته وارسی شده و یک حمله نشست موازی برای آن اثبات شده است .