Abstrakt Ushbu qisqa qo'llanmaning maqsadi avispa

9-rasm: Need ham Schroeder ochiq kalit protokoli simulyatsiyasi.



10-rasm: Needham Shroeder ochiq kalit protokoli simulyatsiyasi, strelkalarni qayta belgilash.

5 HLPSL spetsifikatsiyalarini yozishni osonlashtirish uchun CAS+ sintaksisidan foydalanish CAS+ oddiy protokol spetsifikatsiyasi sintaksisi bo'lib, odatdagi Alice va Bob notatsiyasiga juda yaqin. CAS+ nima ekanligini ko'rish uchun fayllar SPANda simpleProtocol.cas CAS+ faylini oching. Mana to'liq sharhlangan kod.

%% Ma'lumot qismida, har bir agent uchun biz ma'lumotni e'lon qilamiz

%% u PROTOKOL SESSIYANI BOSHLASHDAN OLDIN biladi.

%% Ma'lum bo'lgan ma'lumotlar faqat oldingi "identifikator" bo'limining o'zgaruvchilari bo'lishi mumkin.

%% Bu erda, masalan, A o'zini biladi, S, B va uzoq muddatli umumiy kalit Kas. Lekin,

%% A Kabni bilmaydi!!! Chunki, ushbu protokolda biz Kab seans kaliti bo'lishini xohlaymiz

Har bir seans uchun %% hosil boʻladi (masalan, bir marta). B uchun ham xuddi shunday: u Kabni bilmaydi

Protokolni boshlashdan oldin %%, u xabarni oladi. S ikkalasini ham biladi

%% tugmalari Kas va Kbs, lekin Kab emas.

%% Ushbu "Bilimlar" bo'limi bog'langan haqida hech narsa ayollanmasligi kerak!

%% "session_instances" ustidagi barcha bo'limlar *** standart protokolni *** belgilaydi.

%% buzg'unchisiz. Shunday qilib, biz hech qachon buzg'unchi yoki tajovuzkor kalitlarni aniqlamaymiz

%% va hokazo... Ular quyida tavsiflanadi.

%% bu standart seans bo'lib, u erda alice, bob, server, kas, kbs

%% - o'zgaruvchilarni misol qilish uchun tanlangan ixtiyoriy konstantalar

%% faqat ***"bilim" bo'limida ta'riflangan***. Jumladan

%% Kab uchun doimiyni aniqlamasligingiz kerak, chunki biz buni xohlaymiz

%% Protokolning bajarilishi davomida hosil bo'ladi.

%% Bu seans bo'lib, unda A roli o'ynaydi

%% i, bu tajovuzkorni ifodalovchi zahiralangan konstanta.

%% Chunki S va B o'yinlarini avvalgilariga qaraganda bir xil agentlar o'ynaydi

%% seans, bu ikkinchi seansni belgilash uchun doimiy kbs ishlatiladi

%% B va S o'rtasidagi uzoq muddatli maxfiy kalit.

%% A ni i o'ynaganligi sababli biz kalit uchun yangi doimiy kis yaratamiz

%% buzg'unchi va server o'rtasida taqsimlanadi.

; %% Seanslar roʻyxati nuqtali vergul bilan tugaydi.

intruder_knowledge

elis, bob, server, kis; %% bosqinchi Alisa, Bob, server va Kisni biladi