Суть данного подхода - в разработке формальных моделей, позволяющих анализировать криптопротоколы на основе изучения алгебраических свойств криптографической системы. Среди достоинств данного подхода следует отметить возможность создания инструментариев, с помощью которых допускается автоматизировать процесс исследования криптопротоколов. В результате появился протокольный анализатор (NRL Protocol Analyzer), посредством которого были обнаружены как известные, так и неизвестные уязвимости. На сегодняшний день данный подход к анализу криптопротоколов практически не используется.