ارائه ی مدل صوری طرح امضای کور با استفاده از روش استقرایی

خصوصیات امنیتی پروتکل های امنیتی می تواند با رویکرد وارسی مدل و یا رویکرد اثبات قضیه درستی یابی شو د. روش اثبات قضیه،برخلاف روش وارسی مدل، مدل را متناهی فرض نمی کند و لذا دارای این مزیت است که خصوصیات امنیتی پروتک ل ه ا را در حضور تعداد نامحدودی عامل شرکتکننده درستی یابی و اثبات می نماید. به علاوه، این رویکرد می تواند در تحلیل پروتکل های پیچیده، بدون آنکه مشکل محدودیت مدل را داشته باشد، مورد استفاده قرار گیرد. اما از آنجایی که غالب ساختارهای صوری، تصمیم ناپذیر هستند، ابزارهای اثبات قضیه عموماً خودکار نبوده و نیاز به تعامل با کاربر دارند. از روشهای اثبات قضیه که علی رغم خودکار نبودن ابزار، در تحلیل و اثبات خصوصیات امنیتی پروتکلهای کلاسیک و کاربردی مختلفی موفق بود هند، روش استقرایی است. این روش در طی یک دهه، از جنبه های گوناگونی گسترش داده شده است به گونه ای که قابلیت توصیف و درستی یابی پروتکل های پیچیده تری نظیر پروتکل تجارت الکترونیک SET پروتکل های کارت های هوشمند و پروتکل های جوابگو را پیدا نموده است. امضای رقمی کور، یکی از پر کاربردترین مفاهیم پیشرفته رمزنگاری است که در پروتکل هایی نظیر رای گیری الکترونیکی و پول رقمی مورد استفاده قرار می گیر د. در این مقاله، از آنجایی که درستی یابی این دسته از پروتکل ها، از چالش های مطرح در سال های اخیر می باشد و با توجه به قابلیت گسترش روش استقرایی در جهت توصیف پروتکل های پیچیده، ساختار رمزنگاری فعلی این روش، بر ای پشتیبان ی از امض ای کو ر گسترش داده می شود. برای این منظور پس از ارائه ی بیان صوری طرح امضای کور، قضایا و لم های مرتبط جهت ارزیا بی سازگا ری آن با ساختارهای قبلی، به کمک ابزار اثبات قضیه ی ایزابل، معرفی و اثبات می گردد.

Keywords:

امضای رقمی کور , پروتکلهای امنیتی , روش اثبات قضیه , روش استقرایی