Машиностроение и компьютерные технологии. 2018; : 11-22
Исследование практической возможности решения одной задачи на обобщенных клеточных автоматах с использованием 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
Mechanical Engineering and Computer Science. 2018; : 11-22
Exploring Practicability for Solving a Task Based on the Generalized Cellular Automata via SAT Solvers
https://doi.org/10.24108/1118.0001439Abstract
The paper deals with exploring practicability to solve a task of the recovery key of generalized cellular automata via SAT solvers.
The problem, which we call a task of the key recovery of generalized cellular automata, is under consideration. This task is formulated as follows. The generalized cellular automata, the positive integer s, the initial values of some cells, and the values of some cells after the s steps of the automata are given. It is required to find the initial values of the remaining cells (their number will be called the key length).
To solve the task, were tested Picosat, MiniSat, Glucose, Lingeling, and CryptoMiniSat SAT solvers. In further computational experiments, was used the MiniSat, which was the best.
The key recovery task was solved for the generalized cellular automata of a small size via the MiniSat SAT solver. Pizer's graphs were used as graphs of the automata. The key length was approximately half the number of the cells in the automata. As a result of the study, it turned out that operation time of a SAT solver quite significantly (several orders of magnitude) exceeds the estimated time of solution using the FPGA exhaustive method, and the empirical dependencies of the SAT-solver operation time on the key length are exponential.
The obtained results confirm that SAT solvers disable effective solving a task under consideration. This allows giving the better reasons for the cryptographic security of the crypto-algorithms based on the generalized cellular automata with regard to the cryptanalysis methods using SAT solvers.
References
1. Bard G.V. Algebraic cryptanalysis. Dordrecht; N.Y.: Springer, 2009. 356 p.
2. Klyucharev P. G. Kletochnye avtomaty, osnovannye na grafakh Ramanudzhana, v zadachakh generatsii psevdosluchainykh posledovatel'nostei // Nauka i obrazovanie. MGTU im. N.E. Baumana. Elektron. zhurn. 2011. № 10. Rezhim dostupa: http://www.technomag.edu.ru/doc/241308.html (data obrashcheniya 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. Rezhim dostupa: https://www.ams.org/journals/bull/1990-23-01/S0273-0979-1990-15918-X.pdf (data obrashcheniya 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. Bykov A.Yu., Krygin I.A., Mullin A.R. Algoritmy raspredeleniya resursov sistemy zashchity mezhdu aktivami mobil'nogo ustroistva na osnove igry s nulevoi summoi i printsipa ravnoi zashchishchennosti // Vestnik Mosk. gos. tekhn. un-ta im. N.E. Baumana. Ser. Priborostroenie. 2018. № 2 (119). S. 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. Rezhim dostupa: https://satassociation.org/jsat/index.php/jsat/article/view/45 (data obrashcheniya 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. Rezhim dostupa: http://minisat.se/downloads/MiniSAT_v1.13_short.pdf (data obrashcheniya 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. Rezhim dostupa: http://fmv.jku.at/papers/Biere-SAT-Competition-2017-solvers.pdf (data obrashcheniya 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. Klyucharev P.G. Proizvoditel'nost' i effektivnost' apparatnoi realizatsii potochnykh shifrov, osnovannykh na obobshchennykh kletochnykh avtomatakh // Nauka i obrazovanie. MGTU im. N.E. Baumana. Elektron. zhurn. 2013. № 10. S. 299–314. Rezhim dostupa: http://technomag.edu.ru/doc/624722.html (data obrashcheniya 25.12.2018).
18. Klyucharev P.G. Realizatsiya khesh-funktsii, osnovannykh na obobshchennykh kletochnykh avtomatakh, na baze PLIS: proizvoditel'nost' i effektivnost' // Nauka i obrazovanie. MGTU im. N.E. Baumana. Elektron. zhurn. 2014. № 1. S. 214–223. DOI: 10.7463/0114.0675812
