حمیدرضا خیرمند - دانشجوی کارشناسی ارشد، دانشگاه پیام نور
مهدی جوانمرد - استادیار، دانشگاه پیام نور

وارسی مدل روشی خودکار برای بررسی سیستم های همزمان و سیستم هایی با حالات متناهی می باشد. امروزه وارسی مدل به شکل گسترده ای در آنالیز و ارزیابی صحت سخت افزار، سیستم های نرم افزاری و به خصوص پروتکل های امنیتی مورد استفاده قرار می گیرد. پروتکل گوئیلو- کوئیس کواتر که یک پروتکل مبتنی بر دانایی صفر است، برای اهداف تصدیق هویت کاربرد دارد. در این مقاله ما مدلی از این پروتکل در قالب ماشین حالت متناهی ارائه، ویژگی هایی را به صورت CTL بیان، و پس از پیاده سازی توسط ابزار وارسی مدل نمادین NuSMV اقدام به وارسی و ارزیابی این پروتکل کردیم. با توجه به نتایج حاصل شده، این پروتکل در تمام حالات به درستی عملیات اعتبارسنجی را انجام نمی دهد.

وارسی مدل، پروتکل تصدیق هویت دانایی صفر، پروتکل گوئیلو کوئیس کواتر، NuSMV, CTL