امنیت در سامانه های RFID

امنیت در سامانه های RFID

اسلاید 1: امنیت در سامانه های RFIDارائه دهنده: معصومه صفخاني14 اردیبهشت ماه 1395

اسلاید 2: فهرست مطالب23معرفي سيستم هاي شناسايي بسامد راديويي4تحليل پروتکل هاي شناسايي بسامد راديويي156جمع بندياصول طراحی پروتکل هاي شناسايي بسامد راديويياثبات امنیت پروتکل هاي شناسايي بسامد راديوييپیشنهاداتی برای کار در این زمینه

اسلاید 3: چکيدهدر اين ارائه: مشکلات امنيتي موجود در پروتکل هاي شناسايي بسامد راديويي به تفصيل تحليل و بررسي ي شود.براي برخي از پروتکل هاکه در چند سال اخير پيشنهاد شده اند حملات کارا ارائه مي شود.حملات ارائه شده يک يا چند مورد از اهداف امنيتي محرمانگي، يک پارچگي و دسترس پذيري را نقض مي کنند.و در نهایت جمعبندی و پیشنهاداتی برای کار در این زمینه داده می شوند.

اسلاید 4: SN1234568معرفي سيستم هاي شناسايي بسامد راديويي

اسلاید 5: اجزاي يک سيستم شناسايي بسامد راديويي نوعي برچسب2برچسبnبرچسب3برچسب6برچسب5برچسب4برچسب1برچسب7برچسب خوانپايگاه دادهغير فعالنيمه فعالفعالانواع بر چسب ها:

اسلاید 6: 1-امنيت2- جلوگيري از دزدي و سرقت3- بسته بندي4- بانکداري5- رديابي انسان، حيوان و اشيا کاربردها6- گذرنامه هاي الکترونيکي7- جايگزين بارکدها8- مباحث پزشکي9- کتابخانه ها10- کنترل دسترسي11- پرداخت عوارض جاده اي و ...

اسلاید 7: تهديدات و حملات سامانه هاي شناسایی بسامد رادیویی

اسلاید 8: واحد برچسب خوان خرابکارجستجوي برچسب های RFID معتبر و جمع آوري شناسه آنها براي ساخت برچسب هایRFID جعلياز واحد هاي RFID جعلي مي توان در جعل نمودن کالاها، گذر نامه، گواهينامه رانندگي و ... استفاده نمود.ب برچسب RFID2واحد RFIDnبرچسب RFID3برچسب RFID6واحد RFID5برچسب RFID4برچسب RFIDiبرچسب RFID1برچسب RFID7تهديدات امنيتي RFID

اسلاید 9: برچسب خوان خرابکار مي تواند شناسه برچسب های RFID کاربران انتهايي را جستجو کند.و از اين شناسه ها براي رديابي کاربر استفاده نمايد.حريم خصوصي1500 يورو در کيف پولشماره سريالها :597387,389473…کلاه گيسمدل #4456 (پلي استر ارزان)سه قلم پيراهن مردانهکتاب هند بوک الکترونيکپاي مصنوعي شماره قطعه پزشکي #459382سال 2020 ...تهديدات امنيتي RFID

اسلاید 10: برچسب خوانبرچسب RFID3برچسب RFID4افزايش واحد هاي جعلي موجب سوء مصرف منابع محاسباتي سرور مي شود.پايگاه دادهبرچسب RFID3برچسب RFID3برچسب RFID2برچسب RFID5برچسب RFID4برچسب RFIDnبرچسب RFID4برچسب RFID4برچسب RFID جعليبرچسب RFID معتبرتهديدات امنيتي RFIDبرچسب RFID2 برچسب RFIDnبرچسب RFID3برچسب RFID6 برچسب RFID5برچسب RFID4برچسب RFIDiبرچسب RFID1برچسب RFID7

اسلاید 11: مهم تريـن تهديدات سيستم هاي شناسايي بسامد راديويي

اسلاید 12: راه حل هاي پيشنهادي براي امن سازي فناوري RFID

اسلاید 13: دستور کشتنراه حل هاي امن سازي RFID بدون استفاده از رمزنگاري روش قفس فاراديتوليد پارازيت فعالراه ديگر براي ايزوله نمودن برچسب، مشوش نمودن کانال راديويي است.

اسلاید 14: برچسبRFID مسدود کنندهراه حل هاي امن سازي RFID بدون استفاده از رمزنگاري 1و2و3و...و2023و ....(در خواندن برچسب های RFID شکست مي خورند.) مسدود کننده تمام شماره سريال هاي برچسب هاي RFID ممکن را شبيه سازي مي کند!!

اسلاید 15: يک سامانه شناسايي بسامد راديويي امن تامين خاصيت محرمانگيتامين خاصيت يک پارچگيتامين خاصيت دسترس پذيرينياز به استفاده از پروتکل هاي رمزنگاري در شناسايي بسامد راديويي وجود دارد. ملزومات امنيتي سامانه شناسايي بسامد راديويي

اسلاید 16: پروتکل هاي سيستم هاي شناسايي بسامد راديويي

اسلاید 17: معرفي سيستم هاي شناسايي بسامد راديويي راه حل هاي امن سازي با استفاده از رمزنگاري

اسلاید 18: استاندارد EPC Class 1- Generation 2 پشتیبانی برچسب ها از عملیات منطقی ساده ، CRC و PRNG با طول 16 بیتبرچسب ها دو گذرواژه به نام Access Password و Kill Password دارند. Kill Password برای غیر فعال کردن حافظه برچسب به کار می رود. Access Password برای نوشتن داده در حافظه برچسب به کار می رود. چند جمله ای CRC در این استاندارد X16+X12+X5+1 است.123123123123123 استاندارد EPC-Class1 Generation2

اسلاید 19: پروتکلهاي انساني براي احراز هويت انسان و کامپيوتر به کار مي روند. اين مفهوم براي اولين بار توسط آقاي ويس ارائه شد..به دليل شباهت زياد توانایی محاسباتی و عملیاتی انسان به برچسب های شناسايي بسامد راديويي، اين پروتکل ها مي توانند براي احراز اصالت برچسب ها نيز به کار روند.پروتکل هاي انساني خانواده پروتکل هاي HBمقايسة برچسب ها با انسانشباهت ها1- مانند انسان نمي توانند پسوردهاي طولاني را به خاطر بسپارند.2- مانند انسان نمي توانند محاسبات طولاني را انجام دهند.تفاوت ها1-برچسب ها، در عمليات منطقي مانند AND ، OR، XOR بهتر از انسان هستند.2- در انتخاب اعداد تصادفي بهتر از انسانها هستند.

اسلاید 20: v,ν’ ∈R {0,1}پروتکل هاي انساني -پروتکل احراز اصالت ++ HBz=(a⋅x)⊕(b⋅y)⊕νz=(a.x)⊕(b.y)?a ∈ {0,1}kبرچسب (x, y,x’,y’) (x, y,x’,y’) رb ∈ {0,1}kz’=(f(a)⋅x’)⊕(f(b)⋅y’)⊕ν’z’=(f(a)⋅x’)⊕(f(b)⋅y’)?بيت های نويز به منظور جلوگيري کردن از آشکارشدن x وy,x’,y’ براي حمله کنندگان غير فعال هر پروتکل احراز اصالت شامل r دور مي باشد که r يک پارامتر امنيتي است. برچسب خوان برچسب را احراز اصالت مي کند اگر وتنها اگر از (1-η)r دور با موفقيت عبور نمايد.

اسلاید 21: تحليل پروتکل هاي شناسايي بسامد راديويي

اسلاید 22: انواع حملات انجام شده در سامانه های RFID

اسلاید 23: حمله جعل برچسب خوان

اسلاید 24: حمله جعل برچسب خوان(ادامه)احتمال موفقيت حمله= 1 پيچيدگي حمله = سه بار اجراي پروتکل

اسلاید 25: راهکار مقابله با حمله جعل برچسب خوان در بعضی از کارها:استفاده از دو عدد تصادفي توليد شده توسط قرائت گر و برچسب و ياي انحصاري آنها به دليل کم نمودن طول پيام پردازشي حمله جعل برچسبمثال: پروتکل هاي LCGL، ARAP، WHC، ACSP، SEAS ، HAA ، CTJ و . . . حمله جعل برچسباز ياي انحصاري پيام ها به گونه اي که قابل کنترل براي دشمن باشد بايد پرهيز نمود.

اسلاید 26: حمله جعل برچسب (ادامه)(مرحله اول: شنود و ذخيره مقادير)

اسلاید 27: احتمال موفقيت حمله= 1 پيچيدگي حمله = دو بار اجراي پروتکل(مرحله دوم: جعل برچسب)حمله جعل برچسب (ادامه)چگونه از حمله فوق جلوگيری می شود؟M. Safkhani, N. Bagheri, S. K. Sanadhya, M. Naderi, and H. Behnam “On the Security of Mutual Authentication Protocols for RFID Systems: The Case of Wei et al.s Protocol”, DPM 2011 and SETOP 2011, LNCS 7122,, 2012.

اسلاید 28: راهکار : استفاده از عمليات پيمانه ايمثال: پروتکل HRAPRID مستقل از NT مي شود.حمله جعل برچسب (ادامه)

اسلاید 29: تحرک پذيري برچسب خوان ها مستلزم نا امن بودن کانال ما بين برچسب خوان و پايگاه داده مي باشد.در چنين شرايطي، امکان جعل مجموعه قرائت گر و برچسب براي پايگاه داده وجود دارد. مثال پروتکل CHTJحمله جعل مجموعه برچسب خوان و برچسب

اسلاید 30: N’db,M’3احتمال موفقيت حمله مي باشد .اين حمله مي تواند بعنوان حمله جعل قرائت گر و يا رديابي هم استفاده شود.پايگاه داده هم بايد در تصادفي سازي شرکت نمايد. عدم تدوين مناسب سناريو منجر به حمله اخلال در همزماني مي شود.مثال: پروتکل WHCحمله اخلال در هم زماني

اسلاید 31: استفاده از برچسب زماني براي اجتناب از حمله تکرار و نيز تصادفي سازيمثال : پروتکل AFMAPحمله اخلال در هم زمانيM. Safkhani, M. Naderi and N. Bagheri, “ Cryptanalysis of AFMAP “, IEICE Electronics Express, Vol. 7 , No. 17, pp. 1240-1245, 2010.

اسلاید 32: حمله اخلال در هم زماني (ادامه)يک روش براي اجتناب از حمله تکرار و نيز اينکه پيام ها قابل مرتبط نمودن به هم نباشند ، بهنگام کردن برخي از مقادير پروتکل ( مانند کليد و يا مقادير مخفي مشترک) بعد از هر احراز هويت موفق مي باشد.معمولاٌ يکي از طرفين پيام آخر را مي فرستد و بدون مطمئن شدن از دريافت پيام توسط ديگري مقادير مشترک خود را بهنگام مي کند.-------> حمله اخلال در همزمانيبراي حل اين موضوع، در بعضي از پروتکل ها طرفي که پيام آخر را مي فرستد دو نسخه قديمي و فعلي از مقادير را نگاهداري مي کند.اگر سناريوي بالا خوب تدوين نشده باشد---> حمله اخلال در همزمانيمثال: پروتکل WHC

اسلاید 33: )مرحله اول: شنود و ذخيره مقادير(حمله اخلال در هم زماني (ادامه)

اسلاید 34: )مرحله دوم: اخلال در همزماني(احتمال موفقيت:پيچيدگي: دو بار اجراي پروتکلحمله اخلال در هم زماني (ادامه)M. Safkhani, N. Bagheri, S. K. Sanadhya, M. Naderi, and H. Behnam “On the Security of Mutual Authentication Protocols for RFID Systems: The Case of Wei et al.s Protocol”, DPM 2011 and SETOP 2011, LNCS 7122,, 2012.

اسلاید 35: حمله رديابي در چه صورت مي توان برچسب را رديابي کرد؟مرتبط نمودن داده هاي برچسب در دو نشست مختلفبدست آوردن اطلاعات ثابتي مرتبط با هويت برچسباستفاده از مدل زير و . . . فرض هاآزمونهاتصميم گيريT0: ID0,K0,…T1: ID1,K1,…تصميم مي گيرد b=0 است يا b=1.حمله رديابي

اسلاید 36: بدست آوردن اطلاعات ثابت به نوع عمليات بستگي ندارد.مثال: پروتکل LMAP++ (فوق سبک)فرض هاآزمونهاتصميم گيريID0 mod 2=0ذخيره پيام هادر نظر گرفتن LSB پيام هاتبديل جمع پيمانه اي به ياي انحصاريID1 mod 2=1حمله رديابي (ادامه)M. Safkhani, N. Bagheri, M. Naderi, S. K. Sanadhya,” Security Analysis of LMAP++, an RFID Authentication Protocol”, 6th International Conference on Internet Technology and Secured Transactions, pp. 689-694, United Arab Emirates, 2011.

اسلاید 37: مثال: پروتکل احراز هويت TCL (مبتني بر تابع چکيده ساز)فرض هاآزمونهاتصميم گيريT0: ID0,K0,…T1: ID1,K1,…ذخيرهذخيرهحمله رديابي (ادامه)M. Safkhani, P. Peris-Lopez, N. Bagheri, M. Naderi, J. Cesar Hernandez-Castro,” On the Security of Tan et al. Serverless RFID Authentication and Search Protocols”, RFIDSec, pp. 1-19, 2012

اسلاید 38: حمله افشاي شناسه (ادامه)مثال : پروتکل جستجوي پايه TCL( مبتني بر تابع چکيده ساز). حمله با فرض اينکه تابع چکيده ساز ساختار ديويس مير داشته باشد، انجام مي گيرد.ساختار ديويس مير X[1]Y[2]

اسلاید 39: چگونگي بدست آوردن اطلاعات ثابت به نوع عمليات مورد استفاده بستگي ندارد.مثال : افشاي مقادير مخفي پروتکل IS-RFID با 16^2*3 عملياتحمله افشاي مقادير مخفي39M. Safkhani, N. Bagheri and M. Naderi, ” A Note on the Security of IS-RFID, an Inpatient Medication Safety“, International Journal of Medical Informatics, Accepted Dec. 2012.

اسلاید 40: پروتکل SPRS

اسلاید 41: پروتکل مناسبطراحي پروتکل مناسب و امن شناسايي بسامد راديويي

اسلاید 42: نيازمنديهاي طراحينيازمندي هاي طراحياصل 1: هر پيام بايد نشان دهنده معناي خود باشد. اصل 2: شرايط هر پيام بايد شفاف بيان شوند.اصل 3: اگر اصالت يک طرف پروتکل ضروري باشد، بايد نام طرف در پيام گنجانده شود.اصل 4: دليل استفاده از رمزنگاري بايد مشخص باشد.اصل 5: نبايد استنتاج شود کسي که يک پيام رمز شده را امضا مي کند محتواي آن را مي داند.اصل 6: فرض ها در مورد اعداد تصادفي يکبار مصرف بايد مشخص باشند.اصل 7: حفاظت از کميت هاي قابل پيش بيني مانند يک شمارنده براي اجتناب از حملات تکراراصل 8: تفاوت ساعت در واحدهاي مختلف پروتکل بايد خيلي کمتر از مقدار زمان مجاز باشد.اصل9: استفاده از يک کليد تازه در يک پروتکل، نه خاصيت تازگي پروتکل را ضمانت مي نمايد و نه امنيت پروتکل را.اصل 10: ساز و کار رمزگذاري استفاده شده در پروتکل، بايد معلوم و آشکار باشد.اصل 11: طراح بايد بداند که پروتکلش به چه روابط اعتمادي، وابستگي دارد و چرا ؟

اسلاید 43: جمع بندينام پروتکلنام حملهاخلال در هم زماني(نقض دسترس پذيري)افشاي شناسه(نقض محرمانگي)رديابي (نقض محرمانگي)جعل برچسب(نقض يک پارچگي)جعل قرائت گر (نقض يک پارچگي)جعل مجموعه قرائت گر -برچسب براي پايگاه داده(نقض يک پارچگي)LRWTSLKazahayaIS RFID systemLCGL ARAPHAARAPPCHTJCTJLMAP++ACSPHRAPAFMAP FLMAP  WHCSEASGW 

اسلاید 44: جمع بنديفراهم آوردن خاصيت محرمانگي :بايد تمام طرف هاي پروتکل در تصادفي سازي پيام ها شرکت کنند. تمام پيام هاي پروتکل بايد غير قابل پيش بيني و غير قابل کنترل براي دشمن باشند. اطلاعات ثابت مرتبط با اصالت طرفين پروتکل نبايد از پيام هاي يک نشست پروتکل و يا پيام هاي چند نشست متوالي قابل استخراج باشند.مقادير مشترک بعد از هر اجراي موفق پروتکل بايد بهنگام شوند.بايد مقاومت پروتکل در مقابل انواع حملات رديابي، افشاي شناسه و ... که در آن ها مقادير مرتبط با اصالت آشکار مي شود، بررسي و برآورده شدن آن اثبات گردد.

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

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

اسلاید 47: محورهای کاری در زمینه امنیت RFID

اسلاید 48: Cryptography and Secure Systems LabComputer Engineering DepartmentShahid Rajaee Teacher Training University(sSRTTU)Email: Safkhani@srttu.edu سئوالبا تشکر از توجه شما

اسلاید 49: طراحي يک پروتکل کنترل دسترسي براي شناسايي بسامد راديويي

اسلاید 50: طراحي پروتکل کنترل دسترسي تيماررساله دکتري: تحليل و طراحي پروتکل هاي امنيتي شناسايي بسامد راديوييEmail:M_Safkhani@iust.ac.ir50M. Safkhani, N. Bagheri and M. Naderi, ”On the Designing of a Tamper Resistant Prescription RFID Access Control System“, Journal of Medical Systems, Vol. 36, pp. 3995-4004, Dec. 2012. شناسه پويای برچسبکليد برچسبمجوز دسترسیمقدار مستعار نسخه h(pi)زنجيره چکيده سازی نسخه h(pi,pi-1) شناسه قرائت گرکليد قرائت گرشمارنده افزايشیکپی شمارندهکليد پايگاه دادهويژگي هاي پروتکل تيمار: امکان برقراري ارتباط با قرائت گرهاي مختلفاستفاده از فقط عمليات رمزگشايي در برچسب که موجب کاهش منابع مي شود.تامين خواص امنيتي محرمانگي، يک پارچگي و دسترس پذيري

اسلاید 51: روش تحليل با منطق BAN :بيان پيام هاي پروتکلايجاد مدل ايده آلبيان فرض ها و اهداف امنيتيتحليل پروتکلمنطق BAN 19 قانون منطقي دارد. (P1)(P2)تحليل صوري پروتکل تيمار1. چکيده2. گزارش فعاليـت هاي پژوهشي3. معرفي سيستم هاي شناسايي بسامد راديويي4. تحليل پروتکل هاي شناسايي بسامد راديويي

اسلاید 52: M1:M2:M3:M4:M5:M6:تحليل صوري پروتکل تيمارمرحله اول: بيان پيام هاي پروتکل

اسلاید 53: IM1:IM2:IM3:IM4:IM5:تحليل صوري پروتکل تيمارمرحله دوم : ايجاد مدل ايده آل

اسلاید 54: مرحله سوم : بيان فرضيات و اهداف پروتکلA1:A2:A3:A4:A5:A6:مربوط به تازگي پيام هامربوط به مقادير مشترک پيام هاتحليل صوري پروتکل تيمارG1:G2:G3:G4:G5:موجب اطمينان مي شوند که دشمن هيچ کنترلي روي NT، NR، DIDT، HPi-1، HCi ندارد.

اسلاید 55: روي IM2 و با استفاده از A2 و P1D1:روي D1 و با استفاده از P2D2:روي IM3 و با استفاده از A4 و P2D3:روي D3 و با استفاده از P2D4:روي IM5 و با استفاده از A1 و P1D5:روي D5 و با استفاده از P2D6:روي D5 و با استفاده از P2D7:روي D5 و با استفاده از P2D8:مرحله چهارم: استنباط اهداف امنيتيتحليل صوري پروتکل تيمار

اسلاید 56: طراحي يک پروتکل اثبات گروهي براي سيستم هاي شناسايي بسامد راديويي

اسلاید 57: طراحي پروتکل اثبات گروهي ناظرP. Peris-Lopez, M. Safkhani, N. Bagheri and Majid Naderi, “RFID in eHealth: How Combat Medications Errors and Strengthen Patient Safety”, Journal of Medical and Biological Engineering, Accepted Dec. 2012. ويژگي هاي پروتکل ناظر: امکان برقراري ارتباط با قرائت گرهاي مختلفامکان اثبات حضور i برچسب به صورت همزمانتامين خواص امنيتي محرمانگي، يک پارچگي و دسترس پذيري

اسلاید 58: مقايسه امنيتي پروتکل اثبات گروهي ناظرپروتکل ناظرپروتکل WCZپروتکل Kazahaya نام پروتکلنام ويژگيداردنداردداردتامين خاصيت دسترس پذيريدارد نداردنداردتامين خاصيـت محرمانگيدارددارددارد تامين خاصيت يک پارچگيداردداردندارداحراز اصالت دو طرفه و امنيت پيشرودارددارددارداثبات گروهي4L5L4Lاندازه حافظه در برچسب2L--اندازه حافظه در قرائت گر6L4L4Lاندازه حافظه در پايگاه داده به ازاي هر برچسبانواع عمليات برچسب-انواع عمليات قرائت گر-انواع عمليات پايگاه داده30L27L17Lتعداد پيام ارسالي براي اثبات حضور دو برچسب

اسلاید 59: جمع بنديدر اين ارائه انواع مشکلات و آسيب پذيري هاي امنيتي سامانه هاي شناسايي بسامد راديويي تجزيه و تحليل شده است. هم چنين انواع راه حل هاي امن سازي اين سامانه ها به همراه نقاط قوت و ضعف آن ها ارائه شده است.هدف اين بوده که نقاط قوت در طرح هاي آتي مورد استفاده قرار گيرند و از معايب و نقاط ضعف اجتناب گردد.

اسلاید 60: مقايسه امنيتي پروتکل تيماررساله دکتري: تحليل و طراحي پروتکل هاي امنيتي شناسايي بسامد راديوييEmail:M_Safkhani@iust.ac.ir2/671. چکيده2. گزارش فعاليـت هاي پژوهشي3. معرفي سيستم هاي شناسايي بسامد راديويي4. تحليل پروتکل هاي شناسايي بسامد راديويي 5. طراحي پروتکل کنترل دسترسي6. طراحي پروتکل اثبات گروهي7. جمع بندي8. ارائه پيشنهادها نام پروتکل مشخصاتپروتکل CHTJپروتکلCTJپروتکل تيمار تامين خاصيت دسترس پذيريداردداردداردتامين خاصيت محرمانگينداردنداردداردتامين خاصيت يک پارچگينداردندارددارداحراز اصالت دو طرفه، امنيت پيشرو، کنترل دسترسيدارددارددارداندازه حافظه در برچسب5L8L5Lاندازه حافظه در قرائت گر2L-3Lاندازه حافظه در پايگاه داده به ازاي هر برچسب3L3L4Lانواع عمليات برچسبانواع عمليات قرائت گر-انواع عمليات پايگاه دادهتعداد پيام ارسالي28L8L22L

اسلاید 61: مرحله اول: بيان پيام هاي پروتکل اثبات گروهي ناظر تحليل صوري پروتکل ناظر61M1:M2:M3:M4:M5:M6:M7:M8:M9:M10:M11:M12:M13:M14:

اسلاید 62: تحليل صوري پروتکل ناظرمرحله دوم: ايجاد مدل ايده آل62IM1:IM2:IM3:IM4:IM5:IM6:IM7:IM8:IM9:IM10:

اسلاید 63: مرحله سوم : بيان فرض ها و اهداف پروتکلتحليل صوري پروتکل ناظر63A1:A2:A3:A4:A5:A6:A7:A8:A9:A10:A11:A12:A13:A14:A15:A16:A17:A18:A19:A20:A21:A22:A23:A24:A25:A26:A27:A28:A29:A30:A31:A32:G1:G2:G3:پيام IM6 و فرض A7 طبق قانون P1D1:پيام IM8 و فرض A15 طبق قانون P1D2:پيام IM10 و فرض A23 طبق قانون P1D3:مرحله چهارم : استنباط اهداف پروتکل