تعريف و بررسي نامتغيرهاي امنيتي روي توصيف ماشين حالت پروتكل هاي رمزنگار  Fulltext 

[ بهروز ترك لاداني ] - گروه كامپيوتر دانشكده مهندسي دانشگاه اصفهان
[ سعيد جليلي ] - گروه كامپيوتر دانشكده مهندسي دانشگاه تربيت مدرس

خلاصه مقاله:

در اين مقاله روشي براي تحليل پروتكل هاي رمزنگاري بر اساس مدل سازي پروتكل و نفوذي در قالب مجموعه اي از ماشين هاي حالت محدود تعميم يافته (EFSM) مرتبط با يكديگر ارائه شده است. براي وارسي پروتكل ها ابتدا ويژگي هاي امنيتي مورد نظر در قالب برخي نامتغيرهاي ويژه توصيف شده، سپس صحت يا عدم صحت اين نامتغيرها روي توصيف ماشين حالت پروتكل بررسي ميشود. توصيف برخي ويژگي هاي امنيتي در پروتكل ها به كمك نامتغيرهاي تعريف شده و الگوريتم هايي براي بررسي صحت يك نامتغير داده شده روي EFSM ارائه شده است. به كمك الگوريتم هاي ارائه شده علاوه بر ارزيابي نامتغير مي توان سناريوي حمله متناظر با شكست يك نامتغير Liveness يا موفقيت يك نامتغير Safety را نيز ايجاد نمود. يك ويژگي خاص روش ارائه شد به دليل استفاده از روش هاو ابزارهاي متعار توسعه پروتكل هاي ارتباطي، كم كردن فاصله موجود بين تخصص لازم براي تحليل درحوزه خاص پروتكل هاي رمزنگاري و تحليل و طراحي در حوزه عام تر پروتكل هاي ارتباطي است.

وارسي پروتكل هاي رمزنگاري ، بررسي مدل ، بررسي نامتغيرها ، SDL