Криптографические доказательства не поддаются автоматизации: мнение

Развитие формальных методов в математике и постоянное повышение вычислительных мощностей компьютеров привели к возможности автоматизировать доказательства некоторых теорем и гипотез.

Так, еще в 1976 г. американские математики, используя компьютерную программу, обосновали знаменитую гипотезу о четырех красках для раскрашивания географических карт. Существуют такие системы автоматизированного доказательства теорем (Automated Theorem Proving, ATP), как Otter, E, SPASS, Vampire, Waldmeister, ACL2, Coq, HOL, Nqthm и др.

Однако не все ученые согласны с тем, что применение ATP-систем является обоснованным. Как считает известный математик и криптоаналитик, профессор Вашингтонского университета Нил Коблиц (Neal Koblitz), их потенциал в криптографии невелик.

Профессор Коблиц проанализировал три работы по криптографии, касающиеся схем FDH, Крамера-Шоупа и Эль-Гамаля. Авторы этих работ анализировали стойкость указанных криптографических схем, используя автоматизированные системы доказательства. Коблиц сравнил полученные результаты с данными других исследований, сделанных без применения ATP-систем, и показал, что последние являются математически более строгими.