Наведені правила при аналізі кріптопротоколов можуть доповнюватися, однак певною мірою їх можна вважати основоположними, оскільки вони описують найбільш поширені ситуації.

PbelievesQ <>, Psees (X) K

PbelievesQsaidX

Якщо Р вірить, що Q, і Р поділяють між собою секретний ключ К, і бачить повідомлення X, зашифроване на ключі К, і до того леї р не зашифрував дане X на ключі К, тоді Р має підстави вірити, що X було надіслано Q .

PbelievesX (X), PbelievesQtelievesX PbelievesX Якщо Р вірить в те, що X до цього не використовувалося і що Q посилав X, тоді Р може вважати, що Q довіряє X.

PbelievesQcontrolsX, PbelievesQ> elievesX PbelievesX

Якщо Р вірить, що Q, права має на X, і Р вірить, що Qдоверяет X, тоді Р довіряє X.

Згідно BAN-логіки, перш ніж приступити до аналізу кріптопротокола, його необхідно представити в ідеалізованої формі. Наприклад, процес передачі повідомлення А -* В: (A, Kab) Kbs в ідеалізованої формі може бути зафіксований у наступному вигляді: А -* | В: (А <Ка'> B) Kbs. Коли ж У одержить це повідомлення, його можна відповідно до правил BAN-логіки записати так: У sees (А <КаЬ> B) Kbs. У ідеалізованої формі частину повідомлення, яка не бере участь у доведенні, опускається. Значить, відкрита частина повідомлення не включається до ідеалізовану форму, оскільки вона може бути змінена зловмисником. У загальному випадку ідеалізована форма повідомлення виглядає так: (Xi) Kt ... (Xn) Kn, де кожне зашифроване повідомлення представлено незалежно від інших.

Звідси можна зробити висновок, що аналіз передбачає наступні кроки:

1. Подання протоколу в ідеалізованої формі.

2. Присвоєння початкових значень.