این درس دانشجویان را با انواع مدل‌های صوری امنیت، به‌ویژه امنیت جریان اطلاعات، و نیز با روش‌های تحلیل صوری پروتکل‌های امنیتی آشنا می‌نماید. همچنین، دانشجویان با گذراندن این درس می‌توانند سامانه‌ها، اهداف امنیتی، و توانایی-های مهاجم را به صورت صوری توصیف نموده و آنگاه اثبات نمایند سامانه داده شده، که می‌تواند یک برنامه یا پروتکل امنیتی باشد، اهداف امنیتی را برآورده می‌سازد.

1. مقدمه: روشهای صوری و کاربرد آن‌ها در تحلیل سامانه‌ها، مفاهیم، مزایا و نقاط ضعف
2. امنیت جریان اطلاعات و عدم تداخل: مدل بِل‌ـ‌لاپاجولا، مدل جریان اطلاعات دِنینگ، مدل کوهِن، عدم تداخل
3. امنیت جریان اطلاعات در سامانه‌های غیرقطعی: عدم تداخل اِمکانی، مدل سادرلَند و نااستنتاج‌پذیری، اصلاح‌پذیری پیشرو، مدل محدودیت، ویژگی‌های امنیتی تلفیق‌پذیر، چارچوب‌های تعریف عدم تداخل امکانی
4. عدم تداخل در سامانه‌های همروند: عدم تداخل احتمالاتی برای سامانه‌های همروند، قطعیت مشاهده‌ای، عدم تداخل مستقل از زمان‌بند
5. رویکرد کمّی به امنیت جریان اطلاعات: تداخل و عدم تداخل کمّی، آنتروپی و جریان اطلاعات، اندازه‌گیری جریان اطلاعات و عدم تداخل تقریبی
6. اِعمال خط‌مشی‌های جریان اطلاعات: روش‌های ایستا و زمان اجرا، چند اجرایی امن، شفافیت و دقت در اِعمال
7. تحلیل صوری پروتکل‌های امنیتی: ضرورت، مثال‌ها، مدل دُلِوـ‌یائو
8. مدل‌سازی پروتکل‌ها: استفاده از منطق، حساب فرآیندها، حساب پی، پیام‌ها و استنتاج، نظریه موازنه‌ای، هم‌ارزی ایستا
9. توصیف ویژگی‌های امنیتی: رخدادها، محرمانگی، تصدیق اصالت و موضوع توافق
10. راستی‌آزمایی خودکار: استخراج سامانه قیود، حل قیود، ناتصمیم‌پذیری، استفاده از بندهای هورن
11. رویکردهای دیگر به تحلیل صوری پروتکل‌ها: وارسی مدل، فضاهای استرند، سامانه‌های نوع و تحلیل پیاده‌سازی پروتکل
12. موضوعات تکمیلی

• تمرین‌ها و پروژه: ۳۰ درصد نمره
• آزمون‌های میان‌ترم و پایانی: ۵۰ درصد نمره
• پروژه پژوهشی: ۲۰ درصد نمره