Приведенные правила при анализе криптопротоколов могут дополняться, однако в некотором роде их можно считать основополагающими, поскольку они описывают наиболее распространенные ситуации.

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. Присвоение начальных значений.