Fan nomi: Axborot xavfsizligi protokollari

P X ga ishonadi: R X haqiqat bo‘lgandagidek harakat qiladi, va X ni boshqa xabarlarda ham tasdiqlamog‘i mumkin.

P X ga haqqi bor: P ning X to‘g‘risidagi tasdiqlariga ishonish kerak.

P X deydi: bir vaqtda P X (ga ishonib) xabar yuboradi, shuningdek P

X ga boshqa ishonmasligi mumkin.

• 
  P X ni ko‘radi: P X xabarni qabul qiladi, X ni o‘qishi va uzatishi mumkin.
  
• 
  {X}_K: X K kalit bilan shifrlangan.
  
• 
  Yangi (X): shu vaqtgacha X hyech bir xabarda yuborilmagan.
  
• 
  Kalit (K, P↔Q): P va Q K kalit yordamida bog‘lanishi mumkin.
  

Bu ta’riflarning mohiyatini quyidagi mantiqiy ifodalardan tushunish mumkin: Agar R kalit (K, P↔Q) ga ishonsa, va R {X}_K ni ko‘radi, u holda R (Q X deganiga) ishonadi. Agar R (Q X deganiga) va yangi (X) ga ishonsa, u holda (Q X ga ishonishiga) ishonadi. Bunda R X ning yangiligiga ishonishi lozim, aks holda X eski xabar bo‘lib, hujum qiluvchi tomonidan qayta yuborilgan bo‘ladi.
Agar R (Q ni X da haqqi borligiga) ishonsa va R (Q X ga ishonishiga) ishonsa, u holda R X ga ishonadi. Shuningdek, xabarlar kompozisiyasi bilan ishlash uchun foydalaniladigan yana bir qancha texnik tasdiqlar mavjud. Masalan, agar P Q ning <X, Y> (X va Y ning konkatensiyasi)ga ishonsa, u holda R Q X deganiga va Q Y deganiga ishonadi. Ushbu belgilashlardan foydalanib, autentifikasiyalash protokollari tavsifini shakllantirish mumkin. Shuningdek bu tasdiqlar yordamida, mazkur mijozlar aloqa uchun berilgan kalitlardan foydalanishga ishonishini tekshirish mumkin.
Quyida BAN-mantiq yordamida “Qurbaqa protokolining” tahlili keltiriladi [62]. Autentifikasiyalash protokolining juda sodda protokoli bo‘lgan, “Qurbaqa protokoli” ikkita A va V ishtirokchilar uchun ular ikkisi ham ishongan S serverdan foydalanib himoyalangan aloqa o‘rnatish va vaqtni sinxronlash imkonini beradi. Standart belgilashlardan foydalanib, protokol quyidagicha yozilishi mumkin:
A →S : A, {T_A, K_ab, B}_Kas S →B : {T_S, K_ab, A}_Kbs


A va V ishtirokchilar S server bilan bog‘lanish uchun mos ravishda K_as va
K_bs kalitlarga ega. Bundan quyidagi natijalarni keltirish mumkin: