Исследование применимости SMT/SAT доказательств в криптоанализе хеш-функций семейства Keccak

Abstract

Статья посвящена проблеме использования средств доказательства теорем в криптоанализе функций Keccak-p на разных этапах преобразования. В статье описаны возможности использования SMT/SAT на примере поиска дифференциальных характеристик в начальных раундах преобразования хеш-функции, приводятся основные подходы SMT верификации при моделировании преобразований, описаны существующие средства доказательства теорем