IJMEMES logo

International Journal of Mathematical, Engineering and Management Sciences

ISSN: 2455-7749


A New Cryptographic Scheme Utilizing the Difficulty of Big Boolean Satisfiability

A New Cryptographic Scheme Utilizing the Difficulty of Big Boolean Satisfiability

Waleed Ahmad
Department of Electrical and Computer Engineering, Faculty of Engineering, King Abdulaziz University, P. O. Box 80204, Jeddah 21589, Saudi Arabia.

Ali Muhammad Ali Rushdi
Department of Electrical and Computer Engineering, Faculty of Engineering, King Abdulaziz University, P. O. Box 80204, Jeddah 21589, Saudi Arabia.

DOI https://dx.doi.org/10.33889/IJMEMS.2018.3.1-005

Received on March 24, 2017
  ;
Accepted on June 10, 2017

Abstract

A search problem may be identified as one, which requires an actual “search” for an answer or a solution. Such a problem may have no obvious method, which could be followed to determine a solution, other than to intelligently search through all candidate or potential solutions, which constitute the search space, until a satisfactory one is found. Typically, we may have an efficient way of determining whether one of the possible solutions is actually correct, but no efficient way of determining how to find a correct solution. There are many such search problems, both theoretically and practically motivated, but they all have these difficulties in common. Consider the example of RSA cryptanalysis, where we are given an integer n which is the product of two large prime numbers a and b, and we need to factor n into its factors a and b. This can be achieved by attempting (according to the sieve of Eratosthenes) to divide n by every prime integer between 2 and √n, and hence it is a special kind of a search problem in itself. Several efforts in the past aimed to translate various encryption and hashing schemes into Boolean satisfiability (SAT). The SAT problem is a computationally intractable (NP-hard) problem but relatively efficient SAT-Solvers are built having computational complexity of 2^k (1-∈), where 0< ∈ <1 and thus can prune the search space significantly. Guided by the above concepts, we propose herein a scheme that can encrypt a message by using a ‘big’ Boolean function, which produces an equation that cannot be solved by the conventional SAT-Solvers and leads to a dramatic increase in the search space from 2^n to 〖〖(2〗^(2^m ))〗^n in the worst case. Logical cryptanalysis shows that the proposed scheme is very hard to break, indeed. To the best of our knowledge, the adversary cannot reduce or prune the search space (except for shortening the task needed at every node), and is forced to traverse the whole search space. He might arrive at several candidate solutions, and has to search for clues as to which of them is the correct solution.

Keywords- Cryptography, Boolean satisfiability, Big Boolean algebras, Inverse problems.

Citation

Ahmad, W., & Rushdi, A. M. A. (2018). A New Cryptographic Scheme Utilizing the Difficulty of Big Boolean Satisfiability. International Journal of Mathematical, Engineering and Management Sciences, 3(1), 47-61. https://dx.doi.org/10.33889/IJMEMS.2018.3.1-005.

Conflict of Interest

Acknowledgements

The authors are greatly indebted to Dr. Ahmad Ali Rushdi of the University of California, Davis, California, USA for the technical help he offered in the preparation of this manuscript.

References

Afianti, F., & Barmawi, A. M. (2015). Strengthening Crypto-1 cipher against algebraic attacks. Journal of ICT Research and Applications, 9(1), 88-110.
Ambrose, J. A. (2009). Power analysis side channel attacks: the processor design-level context (Doctoral dissertation, University of New South Wales).
Biere, A. (2008, May). Adaptive restart strategies for conflict driven SAT solvers. In International Conference on Theory and Applications of Satisfiability Testing (pp. 28-33). Springer Berlin Heidelberg.
Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., & Zhu, Y. (1999, June). Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the 36th annual ACM/IEEE Design Automation Conference (pp. 317-320). ACM.
Boyan, J. A., & Moore, A. W. (1998, July). Learning evaluation functions for global optimization and Boolean satisfiability. In Innovative Applications of Artificial Intelligence Conference, AAAI/IAAI (pp. 3-10).
Brown, F. M. (1990). Boolean Reasoning: The logic of Boolean equations. Kluwer Academic Publishers, Boston, MA, USA.
Courtois, N. T. (2003, August). Fast algebraic attacks on stream ciphers with linear feedback. In Annual International Cryptology Conference (pp. 176-194). Springer Berlin Heidelberg.
Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3), 201-215.
Davis, M., LogMeIn, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394-397.
Diffie, W., & Hellman, M. E. (1977). Special feature exhaustive cryptanalysis of the NBS data encryption standard. Computer, 10(6), 74-84.
Eén, N., & Sörensson, N. (2003, May). An extensible SAT-solver. In International conference on theory and applications of satisfiability testing (pp. 502-518). Springer Berlin Heidelberg.
Faizullin, R. T., Khnykin, I. G. E., & Dylkeyt, V. I. (2009). The SAT solving method as applied to cryptographic analysis of asymmetric ciphers. arXiv preprint arXiv:0907.1755.
Gomes, C. P., Selman, B., & Kautz, H. (1998). Boosting combinatorial search through randomization. AAAI/IAAI, 98, 431-437.
Hu, Y., Shih, V., Majumdar, R., & He, L. (2007) Efficient SAT-based Boolean matching for heterogeneous FPGA technology mapping. In Proceedings of the 2007 IEEE/ACM International Conference on Computer-Aided Design (ICCAD’07), IEEE Press.
Hughes, G., & Bultan, T. (2008). Automated verification of access control policies using a SAT solver. International Journal on Software Tools for Technology Transfer (STTT), 10(6), 503-520.
Jovanović, D., & Janičić, P. (2005, September). Logical analysis of hash functions. In International Workshop on Frontiers of Combining Systems (pp. 200-215). Springer Berlin Heidelberg.
Kamal, A. A., & Youssef, A. M. (2010, July). Applications of SAT solvers to AES key recovery from decayed key schedule images. In Emerging Security Information Systems and Technologies (SECURWARE), 2010 Fourth International Conference on (pp. 216-220). IEEE.
Kim, S., & Lee, J. Y. (2007). A system architecture for high-speed deep packet inspection in signature-based network intrusion prevention. Journal of Systems Architecture, 53(5), 310-320.
Larrabee, T. (1992). Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 11(1), 4-15.
Lee, C. C., Jiang, J. H. R., Huang, C. Y. R., & Mishchenko, A. (2007, November). Scalable exploration of functional dependency by interpolation and incremental SAT solving. In Proceedings of the 2007 IEEE/ACM International Conference on Computer-Aided Design (ICCAD’07), (pp. 227-233). IEEE Press.
Legendre, F., Dequen, G., & Krajecki, M. (2014). Logical reasoning to detect weaknesses about SHA-1 and MD4/5. IACR Cryptology ePrint Archive, 2014, 239.

Luby, M., Sinclair, A., & Zuckerman, D. (1993). Optimal speedup of Las Vegas algorithms. Information Processing Letters, 47(4), 173-180.

Marques-Silva, J. P., & Sakallah, K. A. (1997, January). GRASP—a new search algorithm for satisfiability. In Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design (pp. 220-227). IEEE Computer Society.

Marques-Silva, J. P., & Sakallah, K. A. (1999). GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5), 506-521.

Marques-Silva, J. P., (1999, September). The impact of branching heuristics in propositional satisfiability algorithms. In Portuguese Conference on Artificial Intelligence (pp. 62-74). Springer Berlin Heidelberg.

Matsui, M., & Yamagishi, A. (1992, May). A new method for known plaintext attack of FEAL cipher. In Workshop on the Theory and Application of Cryptographic Techniques (pp. 81-91). Springer Berlin Heidelberg.

Mironov, I., & Zhang, L. (2006, August). Applications of SAT solvers to cryptanalysis of hash functions. In International Conference on Theory and Applications of Satisfiability Testing (pp. 102-115). Springer Berlin Heidelberg.

Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001, June). Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference (pp. 530-535). ACM.

Pipatsrisawat, K., & Darwiche, A. (2007a). RSAT 2.0: SAT solver description. SAT competition, 7.

Pipatsrisawat, K., & Darwiche, A. (2007b). A lightweight component caching scheme for satisfiability solvers. In International conference on theory and applications of satisfiability testing (pp. 294-299). Springer Berlin Heidelberg.

Prasad, M. R., Biere, A., & Gupta, A. (2005). A survey of recent advances in SAT-based formal verification. International Journal on Software Tools for Technology Transfer, 7(2), 156-173.

Rudeanu, S. (1974). Boolean functions and equations, North-Holland Publishing Company & American Elsevier, Amsterdam, the Netherlands.

Rushdi, A. M. (2001). Using variable-entered Karnaugh maps to solve Boolean equations. International Journal of Computer Mathematics, 78(1), 23-38.

Rushdi, A. M. (2012). A comparison of algebraic and map methods for solving general Boolean equations. Journal of Qassim University: Engineering and Computer Sciences, 5(2), 147-173.

Rushdi, A. M. A. (2004). Efficient solution of Boolean equations using variable-entered Karnaugh maps. Journal of King Abdulaziz University: Engineering Sciences, 15(1), 115-131.

Rushdi, A. M. A., & Ahmad, W. (2016). Finding all solutions of the Boolean satisfiability problem, if any, via Boolean-equation solving. Journal of King Abdulaziz University: Engineering Sciences, 27(1), 19-34.

Rushdi, A. M. A., & Albarakati, H. M. (2014). Prominent classes of the most general subsumptive solutions of Boolean equations. Information Sciences, 281, 53-65.

Rushdi, A. M. A., & Al-Qwasmi, M. A. (2015). Formal derivation of a particular input of a single AND (OR) gate in terms of its output and other inputs. Journal of King Abdulaziz University: Engineering Sciences, 26(2), 51-62.

Rushdi, A. M. A., & Amashah, M. H. (2010). Parametric general solutions of Boolean equations via variable–entered Karnaugh maps. Journal of Qassim University: Engineering and Computer Sciences, 3(1) 59-71.

Rushdi, A. M. A., & Amashah, M. H. (2012). Purely-algebraic versus VEKM methods for solving big Boolean equations. Journal of King Abdulaziz University: Engineering Sciences, 23(2), 75-85.

Rushdi, A. M., & Amashah, M. H. (2011). Using variable-entered Karnaugh maps to produce compact parametric general solutions of Boolean equations. International Journal of Computer Mathematics, 88(15), 3136-3149.

Ryan, L. (2004). Efficient algorithms for clause-learning SAT solvers (Doctoral dissertation, Theses (School of Computing Science)/Simon Fraser University).

Safarpour, S., Veneris, A., Baeckler, G., & Yuan, R. (2006, July). Efficient SAT-based Boolean matching for FPGA technology mapping. In Design Automation Conference, 2006 43rd ACM/IEEE (pp. 466-471). IEEE.

Sagahyroon, A., Aloul, F. A., & Sudnitson, A. (2011). Using SAT-based techniques in low power state assignment. Journal of Circuits, Systems, and Computers, 20(08), 1605-1618.

Selman, B., Kautz, H. A., & Cohen, B. (1993). Local search strategies for satisfiability testing. Cliques, Coloring, and Satisfiability, 26, 521-532.

Smith, A., Veneris, A., Ali, M. F., & Viglas, A. (2005). Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), 1606-1621.

Soos, M., Nohl, K., & Castelluccia, C. (2009, June). Extending SAT solvers to cryptographic problems. In International Conference on Theory and Applications of Satisfiability Testing (pp. 244-257). Springer Berlin Heidelberg.

Talbot, J., & Welsh, D. J. A. (2006). Complexity and cryptography: an introduction (Vol. 13). Cambridge University Press.

Zhang, H. (1997, July). SATO: An efficient propositional prover. In International Conference on Automated Deduction (pp. 272-275). Springer Berlin Heidelberg.

Zhang, L., & Malik, S. (2002, July). The quest for efficient Boolean satisfiability solvers. In International Conference on Computer Aided Verification (pp. 17-36). Springer Berlin Heidelberg.