Preview

Машиностроение и компьютерные технологии

Расширенный поиск

Исследование практической возможности решения одной задачи на обобщенных клеточных автоматах с использованием SAT-решателей

https://doi.org/10.24108/1118.0001439

Полный текст:

Аннотация

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

Рассматривается задача, которую мы назовем задачей восстановления ключа обобщенного клеточного автомата. Задачу эту сформулируем следующим образом. Дан обобщенный клеточный автомат, натуральное число s, начальные значения некоторых ячеек и значения некоторых ячеек после s шагов этого автомата. Требуется найти начальные значения остальных ячеек (их количество будем называть длиной ключа).

Для решения этой задачи были опробованы SAT-решатели Picosat, MiniSat, Glucose, Lingeling, CryptoMiniSat. Лучшим оказался MiniSat, который и использовался в дальнейших вычислительных экспериментах.

Задача восстановления ключа решалась для обобщенных клеточных автоматов малого размера посредством SAT-решателя MiniSat. В качестве графов этих автоматов использовались графы Пайзера. При этом длина ключа составляла приблизительно половину от числа ячеек автомата. В результате проведенного исследования оказалось, что время работы SAT-решателя весьма существенно (на несколько порядков) превышает оценку времени решения методом полного перебора на ПЛИС, а эмпирические зависимости времени работы SAT-решателя от длины ключа имеют экспоненциальный характер.

Полученные результаты подтверждают, что SAT-решатели не позволяют эффективно решать рассматриваемую задачу. Это позволяет лучше обосновать криптографическую стойкость криптоалгоритмов, основанных на обобщенных клеточных автоматах, по отношению к основанным на использовании SAT-решателей методам криптоанализа.

Об авторе

П. Г. Ключарев
МГТУ им. Н.Э. Баумана, Москва
Россия


Список литературы

1. Bard G.V. Algebraic cryptanalysis. Dordrecht; N.Y.: Springer, 2009. 356 p.

2. Ключарёв П. Г. Клеточные автоматы, основанные на графах Рамануджана, в задачах генерации псевдослучайных последовательностей // Наука и образование. МГТУ им. Н.Э. Баумана. Электрон. журн. 2011. № 10. Режим доступа: http://www.technomag.edu.ru/doc/241308.html (дата обращения 25.12.2018).

3. Pizer A.K. Ramanujan graphs and Hecke operators // Bull. of the Amer. Math. Soc. 1990. Vol. 23. No. 1. Pp. 127–137. Режим доступа: https://www.ams.org/journals/bull/1990-23-01/S0273-0979-1990-15918-X.pdf (дата обращения 26.12.2018).

4. Petit Ch. On graph-based cryptographic hash functions. Doct. diss. Louvain-la Neuve: Catholic Univ. of Louvain, 2009. 282 p.

5. Charles D.X., Lauter K.E., Goren E.Z. Cryptographic hash functions from expander graphs // J. Cryptology. 2009. Vol. 22. No. 1. Pp. 93–113. DOI: 10.1007/s00145-007-9002-x

6. Bosma W., Cannon J., Playoust C. The Magma algebra system. I. The user language // J. of Symbolic Computation. 1997. Vol. 24. No. 3-4. Pp. 235–265. DOI: 10.1006/jsco.1996.0125

7. Handbook of satisfiability / Ed. by A. Biere. Amst.; Wash.: IOS Press, 2009. 966 p.

8. Davis M., Logemann G., Loveland D. A machine program for theorem-proving // Communications of the ACM. 1962. Vol. 5. No. 7. Pp. 394–397. DOI: 10.1145/368273.368557

9. Paturi R., Pudlák P., Saks M.E., Zane F. An improved exponential-time algorithm for k-SAT // J. of the ACM. 2005. Vol. 52. No. 3. Pp. 337–364. DOI: 10.1145/1066100.1066101

10. Быков А.Ю., Крыгин И.А., Муллин А.Р. Алгоритмы распределения ресурсов системы защиты между активами мобильного устройства на основе игры с нулевой суммой и принципа равной защищенности // Вестник Моск. гос. техн. ун-та им. Н.Э. Баумана. Сер. Приборостроение. 2018. № 2 (119). С. 48–68. DOI: 10.18698/0236-3933-2018-2-48-68

11. Biere A. PicoSAT essentials // J. on Satisfiability, Boolean Modeling and Computation. 2007. Vol. 4. Pp. 75–97. Режим доступа: https://satassociation.org/jsat/index.php/jsat/article/view/45 (дата обращения 27.12.2018).

12. Een N., Sorensson N. MiniSAT v1.13 - A sat solver with conflict-clause minimization // SAT Competition 2005: 8th intern. conf. on theory and applications of satisfiability testing: SAT 2005 (St. Andrews, Scotland, UK, June 19-23, 2005): Proc. 2005. Pp. 502–518. Режим доступа: http://minisat.se/downloads/MiniSAT_v1.13_short.pdf (дата обращения 27.12.2018).

13. Een N., Sörensson N. An extensible SAT-solver // Theory and applications of satisfiability testing: 6th Intern. conf. on theory and applications of satisfiability testing: SAT 2003 (Santa Marherita Ligure, Italy, May 5-8, 2003): Selected revised papers. B.; Hdbl.: Springer, 2004. Pp. 502–518. DOI: 10.1007/978-3-540-24605-3_37

14. Audemard G., Simon L. On the Glucose SAT solver // Intern. J. on Artificial Intelligence Tools. 2018. Vol. 27. No. 1. Pp. 1–25. DOI: 10.1142/S0218213018400018

15. Biere A. CaDiCaL, lingeling, plingeling, treengeling, YalSAT entering the SAT Competition 2017 // SAT Competition 2017: Solver and Benchmark Descriptions: 20th intern. conf.on theory and applications of satisfiability testing: SAT 2017 (Melbourne, Australia, Aug. 28 – Sept. 1, 2017): Proc. Vol. B-2017-1. Helsinki, 2017. Pp. 14–15. Режим доступа: http://fmv.jku.at/papers/Biere-SAT-Competition-2017-solvers.pdf (дата обращения 27.12.2018).

16. Soos M., Nohl K., Castelluccia C. Extending SAT solvers to cryptographic problems // Theory and applications of satisfiability testing: 12th intern. conf. on theory and applications of satisfiability testing: SAT 2009 (Swansea, UK, June 30-July 3, 2009): Proc. B.; Hdlb.: Springer, 2009. Pp. 244–257. DOI: 10.1007/978-3-642-02777-2_24

17. Ключарёв П.Г. Производительность и эффективность аппаратной реализации поточных шифров, основанных на обобщенных клеточных автоматах // Наука и образование. МГТУ им. Н.Э. Баумана. Электрон. журн. 2013. № 10. С. 299–314. Режим доступа: http://technomag.edu.ru/doc/624722.html (дата обращения 25.12.2018).

18. Ключарёв П.Г. Реализация хэш-функций, основанных на обобщенных клеточных автоматах, на базе ПЛИС: производительность и эффективность // Наука и образование. МГТУ им. Н.Э. Баумана. Электрон. журн. 2014. № 1. С. 214–223. DOI: 10.7463/0114.0675812


Для цитирования:


Ключарев П.Г. Исследование практической возможности решения одной задачи на обобщенных клеточных автоматах с использованием SAT-решателей. Машиностроение и компьютерные технологии. 2018;(11):11-22. https://doi.org/10.24108/1118.0001439

For citation:


Klyucharev P.G. Exploring Practicability for Solving a Task Based on the Generalized Cellular Automata via SAT Solvers. Mechanical Engineering and Computer Science. 2018;(11):11-22. (In Russ.) https://doi.org/10.24108/1118.0001439

Просмотров: 148


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2587-9278 (Online)