Abstrakt Ushbu qisqa qo'llanmaning maqsadi avispa

SPANda exercise1.hlpsl faylini oching. Tekshirish vositasini tanlang va \Execute" tugmasini bosing. Ajablanarlisi, protokol xavfsiz ekanligi da'vo qilinadi! Buning sababi shundaki, HLPSL spetsifikatsiyasi to'liq bajarilmaydi ... va protokol yugurmaydi, hech qanday sirni oshkor qila olmaydi! Spetsifikatsiyaning bajarilmasligi simulyatsiya orqali aniqlanadi:

\Protokol simulyatsiyasi" tugmasini bosing. Ochilgan oynada siz \Kiruvchi voqealar yo'qligini ko'rishingiz mumkin" protokolda hech qanday xabar almashish mumkin emas degan ma'noni anglatadi. Shunday qilib, HLPSL spetsifikatsiyasida xatolik mavjud.

Odatda HLPSLda xabar almashish mumkin bo'lmaganda, bu yuborilgan xabar noto'g'ri yoki noto'g'ri bo'lganligi sababli chunki qabul qiluvchining namunasi noto'g'ri edi. Keling, muharrirda matndagi exercise1.hlpsl faylini ko'rib chiqaylik. B rolida qabul qilish sxemasi noto'g'ri: RCV({Na}_Kab) B shifrlangan xabarni u biladigan kalit KAB bilan (bu to'g'ri) va uning mazmuni u ham biladigan Na qiymati qabul qilishini bildiradi. Biroq,