Даний підхід є найменш поширеним, оскільки його основна ідея полягає в поданні кріптопротокола як програми з подальшою спробою докази його коректності. Проте тут же необхідно відзначити, що з докази коректності протоколу не слід доказ його безпеки. Найбільш успішними в даному напрямі вважаються формальні методи, автором яких є Кеммерер, і формальний мова LOTOS (Language of Temporal / Ordering Specification), створений для аналізу протоколів аутентифікації. Кеммерер у своїх роботах виділив дві цілі, для досягнення яких можна використовувати формальні методи аналізу кріптопротоколов:

- Формальний аналіз того, що кріптопротокол задовольняє вимогам безпеки;

- Виявлення вразливостей в кріптопротоколах.

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

Прикладом використання кінцевих автоматів є аналіз протоколів аутентифікації. Для кожної процедури (ітерації кріптопротокола) визначається стан кріптопротокола (системи), що виражається в описі станів учасників і комунікаційних каналів між ними. Після чого кожен набір станів аналізується на предмет коректності і відсутності тупикових ситуацій.