Вот ещё нашёл культурное развлечение - проверка протоколов. Общаются между собой клиент и сервер, подключается хакер и пытается кого-нибудь обмануть. На первой картинке записан протокол (словечки вроде senc и aenc означают разные виды шифрования, symmetric encription, asymmetric encription и т.д.) Запускаем программу ProVerif и она находит способ взлома, который изображён на второй картинке. Вертикальные линии обозначают клиента, сервер и хакера, а горизонтальные стрелки - сообщения, которые они друг другу посылают (обычно шифрованные). Хакер, выдавая себя за клиента, получает от сервера зашифрованный секрет, а потом ловко обманывает клиента, чтобы тот его расшифровал.