|
چکیده
|
نقش شبکه های ارتباطی در جهان امروز هر روز پررنگتر و بیشتر می گردد و دائما بر تاثیر آنها بر زندگی بشری افزوده می گردد. این نقش روز افزون و گسترش مخاطراتی که این شبکه ها با آن روبرو هستند ضرورت ایمن سازی هر چه بیشتر اجزای گوناگون آنها از جمله پروتکلهای بکار رفته توسط آنان را یادآوری می نماید. انواع گوناگونی از پروتکلها در بخشهای گوناگون آنها بکار گرفته می شوند که از مهمترین آنها از جهت امنیتی می توان قراردادهای مرتبط با امنیت شبکه را نام برد. تحلیل دستی قراردادهای امنیتی بعلت فراوانی تعداد مراحل موردنیاز جهت انجام، فرآیندی با احتمال اشتباه بسیار می باشد. در حالیکه ابزارهای تحلیل فرمال خطاهای تحلیل دستی را مرتفع می نمایند. آنها اثباتهایی را فراهم می نمایند که مشخص می کند آیا براساس مفروضات و شرایط در نظر گرفته شده در زمان طراحی پروتکل خصوصیات و اهداف طراحی مورد نظر تائید و یا نقض می شوند. روشهای فرمال ترکیبی از مدلهای ریاضی و یا منطقی یک سیستم و نیازمندیهای آن بهمراه روشی موثر برای اثبات اینکه سیستم نیازمندیهای لحاظ شده برای آنرا برآورده می نماید یا خیر می باشند. این روشها مشخصات یک سیستم را براساس یک مدل ریاضی بیان نموده و سپس صحت و یا عدم صحت سیستم را اثباتیا نقض می نمایند. این روشها جهت مدلسازی و تحلیل قراردادهای امنیتی دو رویکرد متفاوت را دنبال می نمایند. اولین روش که از آن بعنوان مدل محاسباتی (computational model) نام برده می شود از منظری محاسباتی به خصوصیات رمزنگاری می نگرد. در حالیکه روش دوم با نام مدل فرمال (formal model) یا مدل نمادین (symbolic model) منظری جبری از خصوصیات امنیتی را بکار می گیرد. در این ارائه تعدادی از ابزارهای فرمال تحلیل قراردادهای امنیتی مانند BAN logic، Scyther، Hermes، CryptoVerif، SHVT و شبکه های پتری رنگ شده مختصرا معرفی شده و بعضی از خصوصیات آنها مورد نقد قرار گرفته اند.
|