ifodalash uchun rasmiy tillar va matematik modellardan foydalanishni oʻz
ichiga
oladi.
Protokol spetsifikatsiyasi:
Rasmiy tekshirishning birinchi bosqichi
kriptografik
protokolning
rasmiy
spetsifikatsiyasini
yaratishdir.
Ushbu
spetsifikatsiya
protokolning maqsadlari, kirishlari, natijalari
va kutilgan xatti-
harakatlarini aniq va aniq tarzda belgilaydi.
Modelni tekshirish:
Modelni tekshirish - bu protokolning barcha mumkin
boʻlgan ijro yoʻllarini muntazam ravishda oʻrganish,
potentsial xatolar yoki
zaifliklarni tekshirish uchun rasmiy tekshirishda qoʻllaniladigan usul.
Toʻgʻriligini isbotlash:
Kriptografik protokol oʻzining moʻljallangan
xavfsizlik talablari va xususiyatlariga javob berishini koʻrsatish uchun rasmiy
dalillardan foydalaniladi. Bu dalillar matematik
mantiq va mulohazalardan
foydalangan holda tuzilgan.
Tekshiruv vositalari:
Protokolning xatti-harakatlarini avtomatik ravishda
tahlil qilish va uning xavfsizlik xususiyatlarini rasmiy
spetsifikatsiyaga muvofiq
tekshirish uchun rasmiy tekshirishda maxsus vositalar va dasturlardan foydalaniladi.
Tasdiqlash muammolari:
Rasmiy tekshirish murakkab va hisoblashni talab
qiladigan jarayon boʻlishi mumkin, ayniqsa katta va murakkab kriptografik
protokollar uchun. Bu kriptografiya va rasmiy usullarda tajriba talab qiladi.
Xavfsizlik xususiyatlari:
Rasmiy tekshirish kriptografik
protokollarning
maxfiylik, yaxlitlik, autentifikatsiya va muayyan hujumlarga qarshilik kabi turli xil
xavfsizlik xususiyatlarini tekshirish uchun ishlatilishi mumkin.
Dostları ilə paylaş: 
