5.      Упражнения для самостоятельного выполнения

Упражнение 1.
Запишите идеализацию, желаемые веры и начальные предположения симметричного протокола Нидхема-Шрёдера в терминах BAN-логики.
Упражнение 2.
Запишите идеализацию, желаемые веры и начальные предположения асимметричного протокола Нидхема-Шрёдера в терминах BAN-логики.
Упражнение 3.
Методами BAN-логики проведите формальный анализ протокола широкоротой лягушки. Сделайте вывод по результатам анализа.