مهدی آبادی - دانشکده فنی و مهندسی دانشگاه تربیت مدرس
سعید جلیلی - دانشکده فنی و مهندسی دانشگاه تربیت مدرس

هر سناریوی نفود یک توالی از سوء استفاده های قابل اجرا توسط نفوذی است که با یک هدف خاص مانند دستیابی به پایگاه داده ها، جلوگیری از سرویس و غیره انجام می شود. در این مقاله، چگونگی استفاده از شیوه بررسی مدل LTL برای کشف خودکار سناریوهای نفوذ به شبکه های کامپیوتری نشان داده می شود. بدین منظور، فرض می شود که در شبکه مورد نظر یک سیستم تشخیص نفوذ مبتنی بر شبکه (NIDS) وجود دارد و نفوذی قصد دارد با انجام یک توالی از سوء استفاده ها و بدون این که NIDS هشداری را اعلام کند به هدف خود برسد. برای کشف سناریوی نفوذ، ابتدا اجزاء شبکه با استفاده از زبان مدل سازی PROMELA توصیف می شوند. سپس، مشخصه ای که نقیض هدف نفوذی را توصیف می کند، در منطق زمانی LTL بیان می شود. در نهایت، به کمک بررسی کننده مدل SPIN که یک بررسی کننده مدل LTL است، هر گونه تخطی از مشخصه فوق (به عبارت دیگر سناریوی نفوذ) بدست اورده می شود. همچنین، الگوریتمی ارائه می شود که با استفاده از آن میتوان از روی سناریوی نفوذ کشف شده سناریوی نفوذ حداقل را بدست اورد.

سناریوی نفوذ ، بررسی مدل ، وارسی خودکار ، منطق زمانی LTL