Learning Plaintext-Ciphertext Cryptographic Problems via ANF-based SAT Instance Representation
Authors: Xinhao Zheng
Yang Li
Cunxin Fan
Huaijin Wu
Xinhao Song
Junchi Yan
Venue: NeurIPS 2024 poster (2024)
Keywords: Boolean Satisfiability Problem
Cryptography
Primary area: machine_learning_for_other_sciences_and_fields

Abstract: Cryptographic problems, operating within binary variable spaces, can be routinely transformed into Boolean Satisfiability (SAT) problems regarding specific cryptographic conditions like plaintext-ciphertext matching. With the fast development of learning for discrete data, this SAT representation also facilitates the utilization of machine-learning approaches with the hope of automatically capturing patterns and strategies inherent in cryptographic structures in a data-driven manner. Existing neural SAT solvers consistently adopt conjunctive normal form (CNF) for instance representation, which in the cryptographic context can lead to scale explosion and a loss of high-level semantics. In particular, extensively used XOR operations in cryptographic problems can incur an exponential number of clauses. In this paper, we propose a graph structure based on Arithmetic Normal Form (ANF) to efficiently handle the XOR operation bottleneck. Additionally, we design an encoding method for AND operations in these ANF-based graphs, demonstrating improved efficiency over alternative general graph forms for SAT. We then propose CryptoANFNet, a graph learning approach that trains a classifier based on a message-passing scheme to predict plaintext-ciphertext satisfiability. 
Using ANF-based SAT instances, CryptoANFNet demonstrates superior scalability and can naturally capture higher-order operational information. Empirically, CryptoANFNet achieves a 50x speedup over heuristic solvers and outperforms SOTA learning-based SAT solver NeuroSAT, with 96\% vs. 91\% accuracy on small-scale and 72\% vs. 55\% on large-scale datasets from real encryption algorithms. We also introduce a key-solving algorithm that simplifies ANF-based SAT instances from plaintext and ciphertext, enhancing key decryption accuracy from 76.5\% to 82\% and from 72\% to 75\% for datasets generated from two real encryption algorithms.

Learning Plaintext-Ciphertext Cryptographic Problems via ANF-based SAT Instance Representation
Xinhao Zheng, Yang Li, Cunxin Fan, Huaijin Wu, Xinhao Song, Junchi Yan' Dept. of CSE & School of AI & Moe Key Lab of AI, Shanghai Jiao Tong University {void_zxh, yanglily, sjtuu1011225529, whj1201, sxh001, yanjunchi)@sjtuu edu.
Abstract
Cryptographic problems, operating within binary variable spaces, can be routinely transformed into Boolean Satisfiability (SAT) problems regarding specific erypto- graphic conditions like plaintext-ciphertext matching, With the fast development of learning for discrete data, this SAT representation also facilitates the utilization machine-learning approaches with the hope of automatically capturing patterns and strategies inherent in cryptographic structures in a data-driven manner. Existing neural SAT solvers consistently adopt conjunctive normal form (CNF) for instance representation, which in the cryptographic context can lead to scale explosion and loss of high-level semantics. In particular, extensively used XOR operations in cryptographic problems can incur an exponential number of clauses. In this paper, we propose graph structure based on Arithmetic Normal Form (ANF) to efficiently handle the XOR operation bottleneck. Additionally, we design an encoding method for AND operations in these ANF-based graphs, demonstrat- ing improved efficiency over alternative general graph forms for SAT. We then propose CryptoANFNet, a graph learning approach that trains classifier based on a pvessage-passsigg scheme to predict plaintext-cipherten satisfiability. Using ANF-based SAT instances, CryptoANFNet demonstrates superior scalability and can naturally capture higher-order operational information. Empirically, Cryp- toANFNet achieves 50x speedup over heuristic solvers and outperforms SOTA learning-based SAT solver NeuroSAT, with 96% vs. 91 % accuracy on small-scale and 72% vs. 55% on large-scale datasets from real encryption algorithms. We also introduce key-solving algorithm that simplifies ANF-based SAT instances from plaintext and ciphertext, enhancing key decryption accuracy from 76.5% to 82% and from 72% to 75% for datasets generated from two real encryption algorithms.
Introduction
Machine Learning (ML) has shown promise solving discrete problems such as Mixed Integer Programming (MIP) [I] and Boolean Satisfiability (SAT) (2). Meanwhile, ML has also made sigmificant strides the field of SAT-based cryptanalysis B Neural solvers for SAT (5 7 enjoy flexibility and automation in handling large datasets through data-driven learning, demonstrating advantages in prediction speed and adaptive learning. Plaintext-ciphereext cryptographic problems running in binary variable spaces can seamlessly be transformed into Boolean Satisfiabllity (SAT) problems, involving specific cryptographic conditions like plaintext-ciphertex matching. This SAT representation facilitates the utilization of machine learning methods to automatically learn inherent patterns and strategies in cryptographic structures a data-driven manner.
*Corresponding author. This work was supported by NSFC (92370201, 62222607) and Shanghai Municipal Science and Technology Major Project under Grant 202ISHZDZX0102..
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

However, the large scale and complex structure of cryptographic instances pose significant challenges for previous ML algorithms, which typically rely on conjunctive normal form (CNF) to encode cryptographic problems and are primarily effective with instances containing relatively small numbers of variables, usually in the range of tens. Cryptographic algorithms frequently entail constraints like XOR, modular addition, AND, and OR operations, thus making the logical XOR operator prevalent in SAT-based cryptanalysis and resulting in the proliferation of XOR clauses. However, XOR operations are generally challenging to represent in CNF. Converting clause connected by XOR with k literals into CNF a well-known process that results in nearly 2 OR clauses, each with &: literals. This could lead to the problem size ballooning considerably, thereby increasing computational complexity, and such encoding may compromise high-order operational information.
CNF is conjunction (and-ing) of clauses, with each clause consisting of a disjunction (or-ing) of positive and negative variables called literals. The innate versatility of "and" and "or" constraint set of CNF allows for efficient application in SAT solving, yet it often requires introducing additional variables to represent more complex logical operations like XOR. Therefore, we propose to adopt an alternative constraint set, Algebraic Normal Form (ANF), to directly represent native XOR operations in the formulas. In ANF, formulas are expressed as collections of polynomials using addition (XOR) and multiplication (AND) operations on Cl) Compared to CNFs, ANFs are more adept at capturing information about higher-order operations and are more concise in handling complex operations. This renders ANF fitting choice for representing the structure and logic of cryptographic algorithms. However, representing ANF as graphs for efficient learning is challenging, and its application to existing SAT solvers is not straightforward CNF, resulting in obstacles to applying ANF in subsequent applications in complex scenarios like cryptographic problems.
To organize effective learning- baaedd SAT practices in ANE, we propose an ANF-based graph structure to represent SAT instances for cryptographic applications. Building upon the graph representations, we propose CryptoANFNet, which employs message-passing scheme and is trained as classifier to predict satisfiability through dedicatedly constructed data encoded from cryptographic problems. The introduction of higher-order operations via ANF simplifies the resulting graph problems that would otherwise require hundreds or thousands of nodes using CNF to merely dozens of nodes. This simplification not only enhances the effecctiveness of learning- based methods but also enables models to naturally capture higher-order operational information. Compared to learning-based SAT solvers, Crypto NNNNet can handle larger instances with greater accuracy and achieves 50x speedup over traditional heuristic solvers. Moreover, for the key-solving problem, we propose a key decryption algorithm that creates and simplifies ANF-based SAT instances from the plaintext and ciphertext, and uses the outputs from two derived SAT instances to deduce the correct key bit values. Given an input plaintext-ciphertext pair and an encryption algorithm, we proceed in three steps: 1) Use the encryption algorithm and the given plaintext-ciphertext to obtain the original ANF-bbsed SAT instance; 2) For a specific bit in the key, create two extended SAT instances by assigning 0 or the chosen bit: 3) Pass these instances to CryptoANFNet in corresponding pairs, output paired scores, and determine the bit value based on which instance has higher score. In this way, we can further improve the accuracy on datasets generated from two real encryption algorithms. The highlights of this paper include:
Based on the Arithmetic Normal Form (ANF), we propose a graph structure succinetly represent the excessive XOR operations in cryptographic problems. We then design two ways to encode the AND operations in the AbT--based graph to represent SAT instances derived from cryptographic problems. In Tab. D our ANF-graph is more efficient than the general graph form for SAT in (5).
We propose (supervised) learning to solve (for the first time to our knowledge) the challenging cryptographic problem: plaintext-ciphertext satisfiability prediction, which could otherwise be intractable by traditional SAT methods. Our proposed GNN-based classifier CryptoANFNet with ANF--based SAT instances as input, achieves a 50x speedup over heuristic solvers, and outperforms the SOTA learning-base SAT solver AT [5] by 96% vs. 91% and 72% vs. 55% accuracy on small and large scale datasets, generated from real encryption algorithms, respectively.
We extend to the key decryption problem. We propose a key-solving algorithm that derives ANF-based SAT instances further simplified by our devised techniques, from the plaintext and ciphertext, and use the output of two derived SAT instances to infer the key values. It boosts accu- racy by 76.5% -22% and 72%->75% on datasets generated from two real encryption algorithms.
2

---

2
Related Works
Learning for SAT. Learning has shown promise in automatically uncovering heuristics for solving combinatorial problems in data-driven manner [8] TO, 12 13. There are primarily two routes dominating these efforts in SAT solving. Learning-aider solvers replace certain components in traditional solvers with learning-aides counterparts to enhance performance. The learning uti- lization encompasses branching heuristies [5), variable initialization [6 18), glue clause prediction [9]. etc. End-to-ent neural solvers conceive SAT solving as a graph-based prediction task based on its CNF representation. They utilize neural networks to directly predict satisfiability or minimal unsatisfied cores via graph maassage-passing networks [3] O or transformers (20). These methods do not rely on handcrafted strategies and demonstrate the potential for magnitude speedup by circumventing exhaustive search procedures. However, neural networks may struggle with large-scale problems, posing a significant challenge, particularly in cryptographic applications where the XOR operation can lead to scale explosion in CNF-based literal-clause graph representations. Besides solving, there are also learning-based efforts that provide support for problem solving, like generating pseudo-industrial instances to resolve data bottlenecks 22 23 M.]
Learning for cryptanalysis. The rise of deep learning has dramatically transformed the ability to analyze encrypted data in its raw state [24] 255, particularly for lightweight block ciphers, as noted in recent studies [26 27
28 29 Gohr 30 pioneered the application of learning- -baed
cryptanalysis on round-reduced SPECK, demonstrating that deep differential-neuree distinguishers could identify features that elude traditional strong distinguishers. This breakthrough highlighted the potential of neural networks in cryptanalysis. Subsequently, further insights into differential- neural distinguishers were provided by [31] showcasing that these networks could learn not only the differential distribution on the output pairs but also those in the penultimate and pent-peeultimate
rounds. Moreover, [32] developed a machine learning-bast based key-recovery attack that successfully carried out the first practical 13-round attacks on SPECK, with extensions to 14-rounds subsequently reported in [33]. However, despite the introduction of neural networks, these methods still fall within the framework of differential analysis and do not directly utilize machine learning to handle plaintext-ciphertexx satisfiability prediction or key-solving problems.
SAT for eryptanalysis The cryptography community has significantly increased its use of auto- mated tools for cryptanalysis, specifically in searching for linear and differential trails, leveraging methods such as the Boolean Satisfiability Problem (SAT) [44] 35 4 Programming (MILP) In SAT-based cryptanalysis, significant strides have been made: (38 explored differential trails in ARX ciphers using SAT methods, while (39) developed an automated search technique for ciphers with Sboxes achieve more accurate and probable differential trails. Additionally, [40] created an SAT-based automated search toolkit applied to SHA-3. These efforts essentially involve converting cryptographic algorithms into SAT instances and then conducting cryptanalysis by searching for differential paths, but they all need handcrafted strategies.
36) and Mixed Integer Linear
To date, no methods have focused establishing effective graph representations and developing SAT solvers based on the XOR-friendly ANF representation. This paper pioneers the utilization of graph forms to represent the excessive XOR operations in cryptographic problems succinetly. As far know, we are the first to integrate graph neural networks and SAT for encryption algorithms.
3 Preliminaries
ANF formula. Algebraic Normal Form (ANF) is polynomial representation of Boolean functions, instrumental in cryptographic applications due to its efficient handling of XOR and AND operations. Formally, logical formula can be rewritten becomes the AND operation and addition in GF2(+) becomes the XOR operation. Then, the SAT instance constituted by the conjunction of logical formulas can be rewritten as several Boolean functions equal to O, ie., several Boolean equations. Therefore, a standard SAT instance in ANF form can be described by multiple Boolean equations, illustrated by the example of ANF-form SAT instance shown at the top of Fig.
boolean function: GF2; multiplication in GF2 (-)
T (a).
Here, each variable is referred to as a vanilla literal. In Boolean equation, the right side is always 0 and the Boolean function on the left side, formed by the XOR connection of monomials, called a clause. Each monomial is either constant term 1, vanilla literal, product of variables. The
3

---

21 + 21 4- 1-2 22
SUPSPPRR
Y PINESTIA
SERORERS
2: - Paff +
Yim
V- X0
+
39 1p-thigg -0
De 05 -0
Al 2i -
3o 12 -0
by +
35 1-
Se
23 to Oy addiit modiiar addilionn B3))
diecuaar left stifts oxt
cieculor right shills (x)
2
B-Y
2 X-Y
Py +-V
AL Pi- -0
F3 Ry +
+
Ro Ry = bitwis AND( -)
Figure I: (a) Example ANF formula graph from MQ problem; (b) The transformations to express the circular left shifts (<<), circular right shifts (>)) modular addition bitwise XOR (e), and bitwise AND (.) operations in ANF.
product of variables is called literal of different orders based on the number of variables multiplied; for example, x 122 called a second-order literal. A literal appears literal exists in the Boolean function represented by the clause. For simplicity, we will omit the multiplication operator (.) for the rest of the paper as long as its use in monomials implicit.
clause if and only if that
MQ problem. Encryption algorithms,, like SPECK. typically use a set of simple and efficient operations, including circular left shifts (<C), circular right shifts (*)), modular addition (H), bitwise XOR (+), and bitwise AND (.) operations. The algebraic properties of these operations allow them to be converted into systems of boolean polynomial equations. In the examples shown in Fig. bb), circular shifts, XOR, and bitwise AND operations can be directly expressed in polynomial form, while modular addition can be represented through quadratic equations. These equations consist solely of variables, second-order products of variables, and the Boolean constant term, which means the encryption process can be transformed into a Multivariate Quadratic (MQ) problem.
In practice, for example, consider the toy formula for the 8-bit plaintext in one round shown below:
X 13122120
Y V3V2V116.
K kykgkiku
Z= 21
W = WzW2WW WD
Z = ((X > 2) YY) K, W (Y << 1)
where K represents the key for the encryption algorithm, X and Y represent the high and low bits of the round function's 's input, respectively, and Z and W represent the high and low bits of the round function's output. It can be transformed into several standard multivariate quadratic equations:
222 + 1/0 + 50 0, T23/ + co =0, + + 81 0, 33C0 + C1 + I331 + c1 0
Zg + 1/2 + ci +2 = 00 JDC1 + 1/211 + Tol2 + C2 = 0, 01 + 3/ + + 83 =
23 + 83 hig = 0, z2
+ k2 0, 21 + ki 0,
50 + 80 +
0
W3 + Zzll2 = O, W2 + F2 = O, w1 x190 = O, W/ + rof3
where 3j, y/. 2;, u; 8i, and & are all Boolean variables and each equation has its right side equal to 0. Thus, by using these transformations, in ANF, and in the following section, we will only address solving the MQ problem.
convert the encryption process into MQ problem
4 Model
4.1
Approach Overview
AbF-based Graph Structures Given the ANF formula of an MQ problem, we propose a graph- based representation for ANF. First, we categorize clause nodes into positive and negative based on whether they contain a constant term. We then directly encode ANF formula into an undirected graph for representing variables and second-order literals: We encode the ANF as undirected graph with one node for every independent literal and second-order literal, two complementary nodes for every clause with the same set of literals, edge between every literal and every second-order literal

---

it corresponds to, edge between every second-order literal and every clause it appears in, and a different type of edge between each pair of complementary clauses.
General Architecture Similar to NeuroSAT 5 we employ a peessage-passingg neural network to derive clause and literal embeddings by executing specified number of iterations. Then, use these embeddings to predict a satisfiability vote through classification multilayer perceptrons((MLP))) Note that we have two key differences: We only retain embeddings for vanilla literals and clauses. The second-order literals' embeddings are derived by concatenating first-order literals's embeddings. 2) We only use clause embeddings and apply two separate classification MLPs for positive and negative clause embeddings to predict the satisfiability vote, respectively.
Key-solving Algorithm With the model CryptoANNNeet, we evaluate the satisfiability of an individual ANF instance individual. Due to the uniqueness of solutions in key-solving problems, we propose algorithm to determine the value of specific bit in key. Given a plaintext-ciphertex pair and an encryption algorithm, our approach derives an ANF-based SAT instance from the input data, generates two derived SAT instances for a specific bit by assigning model to evaluate and determine the most likely value for the bit.
1, and then uses a scoring
4.2 ANF formula Graph
Similar to CNF, the literal-clause structure in an ANF formula has inherent permutation invariance, making it compatible with truphbbaedd representations. However, unlike in CNF, there are no negated literals ANF. Instead, due the constant term, there are complementary relationships between clauses that contain the same literals but have different constant terms. Additionally, compared to CNF, the clauses in ANF formulas exhibit internal asymmetry, where high-order literals, created by combining vanilla literals with AND operations, form special structure within the clause and require further decomposition. Note that in the MQ problem, the ANF formula has at most second-order literals. To represent second-order literals, we directly encode an ANF into an undirected graph G, which can directly derived from an ANF formula follows:
Each vanilla literal z; and second-order literal rıæl (including x,0;)) in the ANF becomes a vertex in graph G.
Each clause becomes two vertices (2, and c)) in graph G according to the set of literals it contains, where denotes clauses with constant term 0, called the positive clause, while denotes clauses with constant term 1, called the negative clause.
An edge between second-order literal Tjæy and clause e is in if and only if myay appears in clause cg. Especially, an edge between second-order literal myب, and clause e₁ is in G if and only if x; appears in clause Ck-
A different edge between each clause vertex and its complementary clause vertex C
A special edge between vanilla literal 2; (and zT)) and second-order literal 2, is in G.
Fig. (a) shows an example graph derived from an ANF formula. The graph is a tripartite graph with three columns of nodes from top to bottom: vanilla literals, second-order literals, and clauses. Nodes at each level are connected to related nodes at the next level, and clauses are additionally connected to their complementary clauses. Besides, we introduce another graph structure that transforms ANF into a bipartite graph by replacing second-order literals with independent variables. This facilitates the use of networks designed for the CNF formula but introduces more nodes. Please refer to Appendix B for more details.
4.3 Model Architecture
Given the ANF formula graph, propose the neural network model, CryptoANFNet, which first extracts the embedding of vanilla literals and clauses from the ANF graph and then predicts the satisfiability vote based on the embedding of clauses. CryptoANFNet uses message-passing neural network to iteratively refine a vector space embedding for nodes the graph. Here, different from NeuroSAT, at each time step t, we only save the embedding of vanilla literals and pairs of complementary clauses.
In each iteration, the model aggregates information from neighboring nodes to update the embeddings. First, each clause receives information from associated literals and its complementary clause and updates its embedding accordingly. We obtain the second-order literal embedding by concatenating
5

---

the vanilla literals. Each clause then receives messages from neighboring second-order literal nodes and its complementary clause based on the graph's 's connectivity. Next, each literal updates its embedding by receiving messages from associated clauses. Specifically, this information transfer occurs in two rounds: first from the clause the intermediate second-order literal and then from the second-order literal to the vanilla literal.
Formally, every time step t, we have matrix (()) Rxdd whose i-th row contains the embedding for the vanilla literal 1 and two matrices C Gneg E TRmxd whose j-th row contains the embedding for the positive clause Cj and the relevant negative clause cj. We initialize these matrices by tiling
1 C Gneg E respectively. Then, single iteration consists of the following two updates:
First, each clause receives messages from associated literals and its complementary clause and updates its embedding accordingly.
L 12c = -122 (110
[C(0]
( Mazee Lmsg (L)2c)
m.pps
m,.eeg
(I)
1)
(hppss) 6 Cu. (1C()) pos
Cit) C(t)
negs mopsl)
pos
(Cpt=
(t++))
+ Cu neg (ICh. Cit) C(t)
h,neg
n.ge
past mm,negl
where = [0, 1, ................................ , 1 1, 1, , 2, 1 1| ER" IR and = 10,0, ,, 1, , n 1,
E E 1²n" represents the row and column index respectively. M22e is the adjacency matrix defined by Mizo(i,j) 1teh i-th second-order literal appears in the j-th clause). L121, Lmsg are two MLPs and Cu.pos, Ca,neg are two layer-norm LSTMs 41 with hidden states Ci(()
h. Ch,eg Rmx respectively.
Next, each literal updates its embedding by receiving messages from associated clauses.
I (0) 21 M1ze (1C(t), past Chegl
(2)
[ M12 Li2m (()))
(3)
(L(+)), L ((+1)) + La (L (t) (
(4)
where M121 is the the adjacency matrix defined by (i, 1 (the i-th vanilla literal appears in the j-th second-order literal). Lizm: Gmsgg are two MLPs and L., is a layer-norm LSTMs with hidden
states (.(0) Raxd
After T iterations for updating clause and literal embeddings, we use these embeddings to predict the satisfiability of the ANF formula. This prediction process involves a feedforward neural network that combines the embeddings of clauses to output a satisfiability vote representing whether the formula is satisfiable not. The feedforward neural network consists of two MLPs, which are designed for the positive and negative clauses respectively, and they compute each clause's 's satisfiability score for the SAT instance based its embedding. Then we sum up the votes of all the clauses and output the final satisfiability vote. This architecture is designed to be flexible and scalable, accommodating various ANF graph sizes and complexities.
Formally, the feedforward neural network outputs the satisfiability vote based on the clauses's embedding (Cpos; Oneg E mddd as follows:
V. f- Cyote (Cpos): V, f- Caace (Cnog) a (sum(V, + V.))
(5)
where V., V. 1m represent the satisfiability score of positive and negative clauses, respectively, O C denote two MIPs. sum(V. V.)) E R represent the sum of the clause votes, and (-)) represent the sigmoid funtion. & E [0, 1] represents the output prediction. We train the network to minimize the binary cross-entropy loss between the output prediction and the true label y.
4.4 Key-solving Algorithm
While we train CryptoANFNet as a classifier to predict satisfiability, we can also use CryptoANFNet for key solving. Given a plaintext-ciphertext pair and encryption algorithm, transform

---

Input:
Key
Output:
(K 11
Ri
ANF
? G
encryption
5k,=1
5g,-0
Ki
ANF formula generator
Key bit guessor
CryptoANFNet
otherwise
plaintext: plaintext-ciphortexx pair
The pipeline of the key-solving algorithm. Given a plaintext-ciphertexr pair and an encryption algorithm, we first transform them into an ANF-based instance of an MQ problem. Then, for a specific key bit K; (the i-th bit of key), we guess its value either 0 or 1 and generate two derived SAT instances. We then employ CryptoANENet to predict the satisfiability of each instance. The final determination of K; based on which instance receives higher satisfiability score.
Figure 2:
them into an ANF- instance of an MQ problem. Since key solutions are typically unique, natural idea is assign values each bit of the key one by one, derive extended instances from the original ANF instance, and then use CryptoANFNet's prediction results to determine each bit's value. For example, consider 4-bit key K kykgkı kg- We could guess K 1kgky get a derived ANF instance and then let CryptoAANNeet predict whether the derived ANF instance is satisfiable. If is, we conclude kz- = 1 otherwise, k3
In essence, it is not necessary to obtain exact classification probabilities for individual samples. Instead, we only need compare the satisfiability votes for samples generated by making two different guesses for the same bit. Based on this idea, we propose the key-solving algorithm to determine the value of specific bit in the key. The algorithm consists of three steps. First, we obtain the original ANF-based SAT instance from the encryption algorithm and the plaintext-ciphereet pair. the
Second, for a specific key bit, we create two derived SAT instances by assigning either selected bit. Third, we use CryptoANFNet to predict the satisfiability votes of these two instances and determine the bit's value based on which instance scores higher. Fig. provides high-level illustration of the algorithm.
Besides, in this algorithm, toANFNet, by minimizing the loss function, as follows.
the derived SAT instances in pairs train the network, Cryp-
N Leis = Σ BCE(c(s:)).u) Leomp Σ
2N
CE(softmax((s2; #24+1)), [126 (20+1))
(6)
Línal
Lets + + Leomp
(7)
where 8; E denotes the satisfiability vote of the i-th instance, Y/ E (0, 1} denotes the corresponding label. BCF(-), C-F(-), (-) and softmax(-) represent the binary cross-entropy loss, the cross-entropy loss, the sigmoid function, and the softmax function. Especially, 82; and 821+1 are two corresponding votes for derived SAT instances, generated by assigning either or to the selected bit of the key in the same original ANF instance.
Experiments
5.1 Datasets
For both training and test datasets, we evaluate our approach on two types of synthetic datasets.
For the first synthetic dataset, we use similar approach to NeuroSAT to generate instances of the MQ problem. These instances consist of the dataset called SR(n), where n the number of variables in the instance. The distribution SR(n) contains pairs of n variables of stochastic SAT instances in ANF formula. The pair of instances have following properties: one of them satisfiable and the other is unsatisfiable, and the difference between the two instances is only in the constant term in one of the clauses. To generate a clause e; of SAT instance ANF with a variables, we randomly sample number k (3 < k < 2n) as the clause's 's length. Then, from all n² second-order polynomials,
7

---

Table 1: Parameters of SAT problems in CNF and ANF
Scipher 3-8-16
Seipher 3-16-32
Scipher
Scipher
Speek 3-8-16
Speck 6-8-16
Datasets
SR(5)
SR(25)
6-8-16
6-16-32
#Literals
6
49
49
97
57
129
CNF
#Clauses
75
5492
195
225
735
1519
336
921
#Nodes
87
6340
245
323
833
1713
450
1179
#Literals
5
48
96
56
ANF
#Clauses
11
26
24
48
48
96
64
136
#Nodes
27
77
72
144
144
288
184
400
Table 2: Performance of different Barriig--based solvers on synthetic datasets
Scipher 3-8-16
Scipher 3-16-32
Scipher 6-8-16
Scipher 6-16-32
Speck 3-8-16
Speck 6-8-16
Datasets
SR(5)
SR(25)
NeuroSAT
91.0%
57.0%
74.0%
72.7%
53.0%
51.0%
55.0%
52.5%
CryptoANENet
96.0%
72.0%
76.5%
75.6%
69.0%
66.5%
72.0 %
68.5%
sample & to include literals in the clause. Polynomials of the form 2f are regarded producing vanilla literal 2;, while those of the form 2i # j) are considered as producing second-order literal m.a.. Additionally, there's s 50% probability of adding a constant term of 1 to the clause. Based on this, in the approach, we continue generating clauses adding them to the SAT instance, and then using traditional ANF-accessible solver, WDSat (22 to check the satisfiability until adding clause Cm finally made the instance unsatisfiable.
For the second synthetic dataset, we utilize instances generated from the real encryption algorithms to construct the dataset. Specifically, we use lightweight and popular block cipher (for certain reasons, do not disclose the specific name of the encryption algorithm, referred to Scipher; for its detailed encryption process, please refer to Appendix C and the SPECK algorithm. Given the length & of the seed key, the length of the plaintext, and the number of encryption rounds randomly generate the seed key and plaintext to generate an SAT instance in ANF corresponding to the encryption algorithm. Then, in each round, the final ciphertext. Based on the generated plaintext-ciphertes pairs and the encryption process, obtain the original ANF instance. Then, we select random bit of the seed key and modify it with and to obtain the corresponding satisfiable and unsatisfiable instances, thus forming the final dataset. Depending on the differences in the encryption algorithms used, the datasets generated by this process are called Scipher-r-k-n and Speck-r-k-n.
the seed key encrypt the plaintext and obtain
5.2 Satisfiability Prediction
Complexity SAT instances. To compare the solving efficiency of CNF solvers and ANF solvers, we first conduct complexity comparison experiments on SAT instances. By representing the same data using CNF and ANF, we compare the number of variables, the number of clauses, and the number of parameterized nodes in the constructed graphs in the learning-based solvers. Table lists the parameters of SAT instances for each dataset under CNF and ANF, Our ANF graph more efficient than the CNF graph, which is general graph previously used to represent SAT problems. In datasets containing XOR operations. CNF typically requires transforming logical expressions into conjunctive normal form, which may increase the number of literals and clauses; whereas ANF directly represents logical functions using polynomials, thus potentially having fewer literals.
Evaluation on different datasets. To evaluate the performance of our proposed CryptoANFNet, we conduct a series of experiments comparing it against the ofate-of-the-art model, NeuroSAT [5]. The primary focus of these experiments is solving SAT instances derived from the real encryption algorithms. For each dataset, we use Bosphorus 44 to convert (without simplification) based SAT instances in our dataset into CNF-based SAT instances, resulting in a CNF form of the same dataset. We then train AryNte on the CNF-form dataset and compared its results with those of SAT, which was trained the ANF-form dataset. Table 2 lists the results of
ANF.

---

Table 3: Performance for key-solving algorithm in solving MQ problems on synthetic datasets.
Scipher 3-8-16
Scipher
Scipher 6-8-16
Scipher
Speck 3-8-16
Speck
Datasets
3-16-32
6-16-32
6-8-16
NeuroSAT 74.0%
72.7%
53.0%
51.0%
55.0%
52.5%
CryptoANENet 76.5%
75.6%
69.0%
66.5%
72.0%
68.5%
CryptoANFNet+ key-solving
82.0% %
78.4%
70.0%
69.0%
75.0%
71.0%
Table 4: Comparing the efficiency of different solvers for solving the MQ problem on synthetic
datasets. (Average runtime: (SAT, UNSAT) ms/instance)
Scipher 3-8-16
Seipher
Scipher
Scipher
Speck 3-8-16
Speck
Datasets
SR(5)
SR(25)
3-16-32
6-8-16
6-16-32
6-8-16
NeuroSAT
S
(3,3)
(20,20)
(7,7)
(10,10)
(7.7)
(14,14)
(13,13)
(18,18)
CryptoANFNet
(2.2)
(5.5)
(8,8)
(9.9)
(10,10)
(8,8)
(11,11)
(14,14)
WDSat (36,34)
(2470,5662)
(38,38)
(39,39)
(40,37)
(86,150)
(44,47)
(46,46)
CryptoMimiSat 44
(4,4)
(13491,359122)
(4,4)
(7.9)
(8,9)
(410,1354)
(5,5)
(6,8)
Kissat 45
(2,2)
(4922, 14856)
(2,2)
(2,2)
(5,8)
(219,464)
(3,3)
(4,5)
AT and CryptoANFNet on synthetic datasets of different scales. On small-scale datasets, both models achieve high accuracy, but CryptoANFNet still outperforms NeuroSAT, such 96% vs. 91 % accuracy on the SR(5) dataset. On large-scale datasets, like SR(25), NeuroSAT can hardly predict the satisfiability of instances, with its prediction accuracy hovering around 50% and CryptoANNNet significantly outperforms NeuroSAT, such as 72% vs. 57% accuracy on the SR(25) dataset and 72% vs. 55% accuracy the Speck-3-8- dataset.
5.3 Key Bit Prediction
In addition to evaluating the satisfiability of individual ANF instances with the model CryptoANFNet, we conduct a comparative experiment to validate the key-solving algorithm. We assess the effec- tiveness of the key-solving algorithm in determining specific bit values in cryptographic keys by testing on datasets generated from real encryption algorithms, such as Scipher-r-k-n and Speck-r-k-n. For each dataset, we use the associated SAT-UNSAT instance pairs generated by the key-solving algorithm to train CryptoANFNet. In this experiment, we set À = 0.1. Table lists the comparison shown, the key-solving algorithm
of results before and after using the key-solving algorithm. somewhat improves performance on the tested datasets. Notably, it boosts the accuracy from 76.5% 82% and from 72% to 75% on the Scipher-3-o 16 and Speck-3-8- datasets, respectively.
5.4 Comparsion with Heuristic SAT solvers
In this section, we evaluate the efficiency of our proposed model, CryptoANFNet, in comparison with traditional heuristic SAT solvers. These experiments focused on assessing the efficiency of solving the following
SAT instances derived from real encryption algorithms. We compare CryptoANFNet solvers: the best currently available implementation of CryptoMiniSat 44 (a CNF-based solver specifically designed for handling complex problems cryptanalysis), Kissat (45 (a highly efficient CNF-based solver that has demonstrated its ability to solve challenging SAT instances in the SAT competition), and WDSat 42
(an bNF-based solver for instances in algebraic normal form).
To fairly compare the efficiency of solvers, we test the unit solving time (ms/instance) for UNSAT and SAT instances for each dataset. For the ANF--baed solver, we directly test the instances in ANF form. For CNe-b solvers, we use Bosphorus 43 to convert the ANF instances (without simplification) to CNF form for testing. We test all solvers on an AMD Ryzen Threadripper 3970X 32-Core Processor and an NVIDIA GeForce RTX 3090 GPU. Table lists the results of different solvers and more results are shown in Appendix A We find that the learning-based model Crypto and AT solve SAT instances derived from cryptographic problems much more quickly and CryptoANFNet achieves a 50x speedup on average over traditional heuristic solvers. These results make it possible to apply learning- based solvers in practice.

---

Conclusion and Outlook
In this paper, we propose a graph structure based on Arithmetic Normal Form (ANF) to efficiently handle XOR operations in cryptographic problems. We also design an encoding method for AND operations within these ANF-based graphs, demonstrating improved efficiency over traditional graph forms. Building on this, introduce CryptoANNNett graph learning framework for SAT- based cryptanalysis utilizzig ANF. CryptoANNNeet addresses the challenging problem of plaintext- ciphertext satisfiability prediction and achieves remarkable 50x speedup over heuristic solvers. also outperforms the state-of-the-art learning-based SAT solver, NeuroSAT. Furthermore, we introduce key-solving algorithm that simplifies ANF-based SAT instances derived from plaintext and ciphertext, enhancing key decryption accuracy. In this way, future research could explore further optimization of the ANF-based graph structures and the integration of more advanced neural network models to push the boundaries of cryptographic problem-solving.
References
[1] J. Zhang, C. Liu, X. Li, H.-I.. Zhen, M. Yuan, Y. Li, and Yan, "A survey for solving mixed integer programming via machine learning," Neurocomputing, vol. 519, pp. 205-217, 2023.
[2] W. Guo, H.-L. Zhen, X. Li, W. Luo, M. Yuan, Y. Jin, and Yan, "Machine learning methods in solving the boolean satisfiability problem." Machine Intelligence Research, 2023.
[3] L. Sun, D. Gerault, A. Benamira, and T. Peyrin, "Neurogift: Using a machine learning based sat solver for cryptanalysis." in Cyber Security Cryptography and Machine Learning. S. Dolev, V. Kolesnikov, S. Lodha, and G. Weiss, Eds. Cham: Springer International Publishing, 2020,
pp. 62-84.
[4] S. Nejati and V. Ganesh, "Cdel (crypto) sat solvers for cryptanalysis," arXiv preprint arXiv:2005.13415 2020.
[5] D. Selsam, M. Lamm, B. Bünz, Liang, L. de Moura, and D. L. Dill, "Learning sat solver from single-bit supervision." in International Conference on Learning Representations, 2019.
[6] 7. Li, J. Guo, and X. Si, "G4satbench: Benchmarking and advancing sat solving with graph neural networks," arXiv preprint arXiv:2309. 16941, 2023.
[7] C. Cameron, R. Chen, J. Hartford, and K. Leyton- Leyton-Brown, "Predicting propositional satisfiability via end-to-end learning." in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, no. 04, 2020, pp. 3324-3331.
[8] Y. Bengio, A. Lodi, and A. Prouvost, "Machine learning for combinatorial optimization: a methodological tour d' d'horizon." European Journal of Operational Research, vol. 290, no. 2, pp. 405-421, 2021.
[9] Y. Li, J. Guo, R. Wang, and J. Yan, "T2t: From distribution learning in training to gradient search in testing for combinatorial optimization." in Advances in Neural Information Processing Systems, 2023.
[10] X. Li, F. Zhu, H.-L. Zhen, W. Luo, M. Lu, Y. Huang. 7. Fan, Z. Zhou, Y. Kuang. 7. Wang et al., Maachnee learning insides optverse ai solver: Design principles and applications," arXiv preprint arXiv:2401.088 055960 2024.
[11] Z. Guo. Y. Li. C. Liu, W. Ouyang, and J. Yan, "Acm-milp: Adaptive constraint modification via grouping and selection for hardness milp instance generation," " in The Forty-first International Conference Machine Learning, 2024.
[12] H. Geng, H. Ruan, R. Wang. Y. Li, Y. Wang, Chen, and Yan, "There is no silver bul- let: Benchmarking methods in predictive combinatorial optimization," Advances in Neural Information Processing Systems, 2024.
[13] Y. Li, J. Guo, R. Wang. H. Zha, and J. Yan, "Fast 12t: Optimization consistency speeds up diffusion-based training-to- to-testing solving for combinatorial optimization," in Advances in Neural Information Processing Systems (NeurIPS), 2024.
[14] D. Selsam and N. Björner, "Guiding high-performance sat solvers with unsat-core predictions," in International Conference Theory and Applications of Satisfiability Testing, 2019.
10

---

[15] V. Kurin, S. Godil, S. Whiteson, and B. Catanzaro, "Can q-learning with graph networks learn generalizable branching heuristic for sat solver?" Advances in Neural Information Processing Systems, vol. 33, pp. 9608-9602 2020.
[16] H. Wu, "Improving sat-solving with machine learning." in Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, 2017, pp. 787-788.
[17] H. Duan, S. Nejati, G. Trimponias, Poupart, and V. Ganesh, "Online bayesian moment match- ing based sat solver heuristics," in International Conference on Machine Learning. PMLR,
2020, pp. 2710-2719.
[18] Z. and Si, "Nsnet: general neural probabilistic framework for satisfiability problems," Advances in Neural Information Processing Systems, vol. 35, pp. 553-2 585, 2022.
[19] J. M. Han, "Enhancing sat solvers with glue variable predictions," arXiv preprint arXiv:2007. 7,059, 2020.
[20] Z. Shi, M. Li, Y. Liu, S. Khan, J. Huang, H.-L. Zhen, M. Yuan, and Q. Xu, "Satformer: brand unsat core learning," in 2023 IEEE/ACM International Conference Computer Aided Design (ICCAD). IEEE, 2023, pp. 1-4.
[21] You, H. Wu, C. Barrett, R. Ramanujan, and Leskovec, "G2sat: Learning to generate sat formulas," in Advances in neural information processing systems, vol. 32, 2019.
[22] Y. Li, X. Chen, W. Guo, X. Li, W. Luo, J. Huang, H.-L. Zhen, M. Yuan, and J. Yan, "Hardsatgen: Understanding the difficulty of hard sat formula generation and a strong grructre-hardnee aware baseline," " in ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD), 2023.
[23] X. Chen, Y. Li, R. Wang, and Yan, "Mixsatgen: Learning graph mixing for sat instance generation." in The Twelfth International Conference on Learning Representations, 2024.
[24] E. Wenger, M. Chen, F. Charton, and K. E. Lauter, "Salsa: Attacking lattice cryptography with transformers," Advances in Neural Information Processing Systems, vol. 35, pp. 34 981-341--4 994, 2022.
[25] C. Li, E. Wenger, Z. Allen-Zhu, F. Charton, and K. E. Lauter, "Salsa verde: machine learning attack on lwe with sparse small secrets," Advances in Neural Information Processing Systems, vol. 36, pp. 53 343-53 361, 2023.
[26] A. Singh, K. B. Sivangi, and A. N. Tentu, "Machine learning and cryptanalysis: An in-depth exploration of current practices and future potential," Journal of Computing Theories and Applications, vol. 2, no. 1, pp. 27-42, 2024.
[27] J. So, "Deep learning-based cryptanalysis of lightweight block ciphers," Security and Communi- cation Networks, vol. 2020, pp. 1-11, 2020.
[28] A. Baksi and A. Baksi, "Machine learning-assisted differential distinguishers for lightweight ciphers," Classical and Physical Security of Symmetric Key Cryptographic Algorithms, pp. 141-162, 2022.
[29] Z. Hou, J. Ren, and S. Chen, "Cryptanalysis of round -rduucd simon32 based on deep learning." Cryptology ePrint Archive, 2021.
[30] A. Gohr, "Improving attacks on round-reduced speck32/64 using deep learning," " in Advances in Cryptology-CRYPP 2019 39th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 18-22, 2019, Proceedings, Part II 39. Springer, 2019, pp. 150-179.
[31] A. Benamira, D. Gerault, T. Peyrin, and Q. Q. Tan, "A deeper look machine learning-base based cryptanalysis." " in Advances in Cryptology EUROCRYPT 2021: 40th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Zagreb, Croatia, October 17-21, 21, 2021, Proceedings, Part I 40. Springer, 2021, pp. 805-835.
[32] Z. Bao, J. Guo, M. Liu, L. Ma, and Y. Tu, "Enhancing differential-neurall cryptanalysis," in International Conference on the Theory and Application of Cryptology and Information Security. Springer, 2022, pp. 318-347.
[33] Z. Bao, J. Lu, Y. Yao, and L. Zhang, MMore insight on deep Sarning-aided cryptanalysis," International Conference on the Theory and Application of Cryptology and Information Security. Springer, 2023, pp. 436-467.
11

---

[34] F. Lafitte, "Cryptosat: a tool for sat-based cryptanalysis." IET Information Security, vol. 12, no. 6, pp. 463 463-474, 2018.
[35] M. Soos, "The cryptominisat 5 set of solvers competition 2016," Proceedings of SAT Competition, p. 28, 2016.
[36] J. Lu, Y. Liu, T. Ashur, B. Sun, and C. Li, "Improved rotational-xor xor cryptanalysis of simon- block ciphers," " IET Information Security, vol. 16, no. 4, pp. 282-300, 2022.
[37] N. Mouha, Q. Wang, D. Gu, and B. Preneel, "Differential and linear cryptanalysis using Information Security and Cryptology: 7th International
mixed-integer linear programming."
Conference, Inserypt 201 1, Beijing, China, November 30-December 3, 2011. Revised Selected Papers 7. Springer, 2012, pp. 57-76.
[38] N. Mouha and B. Preneel, "Towards finding optimal differential characteristics for Applica- tion to salsa20," Cryptology ePrint Archive, 2013.
[39] L. Sun, W. Wang, and M. Wang. "More accurate differential properties of led64 and midori64," IACR Transactions Symmetric Cryptology, pp. 93-123, 2018.
[40] J. Guo, G. Liu, I.. Song, and Y. Tu, "Exploring sat for cryptanalysis:quannuai collision attacks against 6-round sha-3," " in International Conference on the Theory and Application of Cryptology and Information Security. Springer, 2022, pp. 645-674,
[41] I. Bello, H. Pham, Q. V. Le. M. Norouzi, and S. Bengio, "Neural combinatorial optimization with reinforcement learning," 2017.
[42] M. Trimoska, S. Ionica, and G. Dequen, Parity (XOR) Reasoning for the Index Calculus Attack. Springer International Publishing, 2020, p. 774-790. [Online]. Available: http:/dxxdoii.og 10/g//1..lo 10007/988-3-00--544-8
[43] D. Choo, M. Soos, K. M. A. Chai, and K. S. Meel, "Bosphorus: Bridging anf and enf solvers." in Proceedings of Design, Automation, and Test in Europe(DATE), 2019.
[44] M. Soos, K. Nohl, and C. Castelluccia, "Extending sat solvers to cryptographic problems." in International Conference on Theory and Applications of Satisfiability Testing. Springer, 2009, pp. 244-257.
[45] A. Biere and M. Fleury, "Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022," in Proc. of SAT' Competition 2022 Solver and Benchmark Descriptions, ser. Department of Computer Science Series of Publications B, T. Balyo, M. Heule, M. Iser, M. Järvisalo, and M. Suda, Eds., vol. B-2022-1. University of Helsinki, 2022, pp. 10-11.
[46] B. Selman, H. A. Kautz, B. Cohen et al., "Noise strategies for improving local search," in AAAI, vol. 94, 1994, pp. 337-343.
[47] J. Elffers and J. Nordström, "Divide and conquer: Towards faster pseudo-booled solving." in IJCAI, vol. 18, 2018, pp. 1291-1299.
[48] A. Kyrillidis, A. Shrivastava, M. Vardi, and Zhang, "Fouriersat: A fourier expansion-bai algebraic framework for solving hybrid boolean constraints," in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, no. 02, 2020, pp. 1552-1560.
12

---

+ Mp Mg Mg +
as + ta
By Mg 24 + Mg
X1 + Mo
2:022
Mi - -arggg
144 Ky3
M: - K24
Ril li - 44-5
N4 K2
My My
Me Migh S
My M4
u. + Mo H Ma + Ms + 0
as + ou 0u
+ My + Mi + = 0
as + 02 uy +
my M4 1-10
ae i uu up 1 ui
61)
Figure 3: (a) A example ANF formula for changing the original ANF formula to a formula without AND operation; (b) Example ANF formula graph focusing on second-order literals
A
Efficiency of incomplete solvers
Table 5: Comparing the efficiency of incomplete solvers for solving the MQ problem on synthetic datasets. (Average runtime: (SAT, UNSAT) ms/instance)
Seipher 3-8-16
Scipher
Scipher
Scipher 6-16-32
Speck 3-8-16
Speck
Datasets
SR(5)
SR(25)
3-16-32
6-8-16
6-8-16
WalkSAT
H6
(3.640)
(762,744)
(4.6)
(10,12)
(289,26)
(831,899)
(39,480)
(482,538)
RoundingSAT
4
(3,3)
(36758,50122)
(3,5)
(7,10)
(28,20)
1861)
(23,24)
(29,35)
ATurierSA
4R
(1275,8670)
(9620.9687)
(983,426)
(1779,459)
(8163,416)
(8830,8862)
(8733,8689)
(8799,8912)
B ANF Graph Structure focusing on second-order literals
This ANF graph structure retains only second-order literals and regards them as independent vanilla literals, representing original literals through these new literals and adding additional constraint equations. In this case, the graph has node for every literal and every clause, an edge between every literal and each clause in which it appears, a different edge for each pair of complementary clauses, and special edge between corresponding sets of literals.
For this type of graph, we focus on the unified representation of the vanilla literal and second-order literal. Note that we can represent all the vanilla literals with the second-order literals and their negations. For example, the vanilla literal xi can be represent T1 x2 + 21 Based this idea, we introduce the negations of a second-orden literal (e.g. Fi32, I1 of 2)x2) as the new vanilla literals and we update the original ANF formula, where every three corresponding literals consist of literal subset. Then, the ANF instance of an MQ problem with n variables is represented as the ANF instance of a linear problem with 3n(n 1) variables.
Since the newly introduced variables are independent of each other except for the atomic clauses, to ensure that the original problem doesn't 't become too relaxed due to the increase in variables, we add the following two types of constraints: 1) The new vanilla literal combinations must represent the same literal in the original ANF instance; At most of the three new vanilla literals derived from the same second-order literal in the original ANF instance can be true. Notably, the second constraint not presented in the form of an ANF formula but as an inequality, represented as a special type of edge in the graph construction. As the toy example shown in Fig. (a), the redefined vanilla literals u1 = 22 U2 = TJ Ug I x102 and u4 2 23,, Un 3143, u3 2₁ have the constraint u1 uu + u Uig 0 due to I1 = 22 + Zizy = Ii + x Ty in ug = ua + us. Besides, since U1, U2 us and u4, Us Ug belong to the same literal subset respectively. we have 41 + U2 + Us S 1 and u4 + Us + Us < 1.
Then, an undirected graph is derived from an updated ANF formula as follows and Fig. 3bb shows the graph derived from the ANF formula in Fig. aa).
Each vanilla literal u, in the ANF becomes vertex in graph G.
13

---

Each clause becomes two vertices (2; and o;) in graph G according to the set of literals it contains, where e; denotes clauses with constant term 0, called the positive clause, while c denotes clauses with constant term 1, called the negative clause.
An edge between literal u, and clause G₁ is in g if and only if æ:5ıy appears in clause Cj. A different edge between each clause vertex e, and its complementary clause vertex G--
Two special edges between each literal u, and other literals in their common literal subset.
C Encryption Process of Scipher
Seipher has the following encryption process. Given the length k of the seed key, the length n of the plaintext, and the number of encryption rounds r. Scipher consists of multiple rounds of transformations. Each round uses round key that is derived from the original key through specific linear transformations, with length equal to half of the input and output lengths of that round. The input for the first round is the plaintext, and the output of the r-th round is the ciphertext. For the i-th round, we have the following round function:
T (L, < O)
< b), T2 = = <C
T3 = T1 ( T2 1 K;
I4+1 T3 R₁
R4+1 = L.
where K, represents the round key for the i-th round; a, b, are constants representing the number of shifted bits; L; and R; represent the high and low parts of the i-th round function's input, while Li+1 and R represent the high and low parts of the output.
D Limitations
The primary limitation of this paper lies in our focus on plaintext-cipherrextt cryptographic Problems, while not fully exploring other cryptographic issues. On the one hand, our objective is to introduce novel graph construction approach by leveraging the commonly encountered XOR operation in cryptographic problems, thereby proposing graph structure based on the Arithmetic Normal Form (ANF). This allows plaintext-ciphertext cryptographic Problems to be conveniently transformed into bas-b SAT instances. On the other hand, plaintext-ciphertext encryption algorithms are built on the hardness of the MQ problem, and thus the SAT instances derived from plaintext-ciphertext problems are also instances of the MQ problem. This provides a basis for exploring various aspects of the MQ problem. Consequently, we have chosen the widely studied plaintext-ciphertex cryptographic Problems for comprehensive decomposition and investigation. We believe that our exploration of ANF-based SAT instances will offer valuable insights and reference points for the field of SAT-based cryptanalysis. Furthermore, the proposed model can be adapted to other cryptographic problems that require the transformation of the original problem into instance of the MQ problem.
E
Impact Statements
The proposed CryptoANFNet, a novel graph learning framework for SAT-based cryptanalysis utilizing Arithmetic Normal Form (ANF), presents a fresh approach to tackling the challenging task of predicting plaintext-cipherten satisfiability. Its speed improvement, surpassing heuristic solvers by remarkable 50x and outperforming advanced lcarning-based SAT solvers like NeuroSAT, marks significant advancement in cryptographic problem-solving. These strides not only enhance the efficiency and accuracy of cryptographic solutions but also open up new avenues for optimizing learning- based SAT solvers, advancing decryption algorithms, and ultimately fostering the refinement of eneryption techniques.
14

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We summarize the contributions of this paper in both the abstract and the concluding paragraph of the introduction. Each claimed contribution is supported by explicit results presented within the paper.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
We have discussed the limitations in Appendix D
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model sell-speciiiatiinn asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
15

---

Answer:
[NA]
Justification:
The paper does not include theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proof's can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: We have provided the dataset settings in Section 5.1 and detailed experimental
settings in Section 5.2 and Section 5.4
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, descríbing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e-g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
5. Open access to data and code
16

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [No]
Justification:
The source code will be made publicly available upon acceptance.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips.co cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
//nips //iips.cc/pill wttpcccpppppppppeeeeeeeeeeeeeeee httpe//gggeeee/eeeuubbissssssss /Cc////oddiiisssseeeeeee ssiiiisiicyiiyyyy for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [Yes]
Justification: We have provided the dataset settings in Section 5.1 and detailed experimental settings in Section 5.2 and Section 5.4
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification:
We keep the same setting as the previous works.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi-
dence intervals, statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for
example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
17

---

The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma enror bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are range (e.g. negative enror rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We have provided the dataset settings in Section 5.1 and detailed experimental
settings in Section 5.2 and Section 5.4
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make it into the paper).
9. Code Of Ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics https: httpps://neurppp http://ss...ppulleccccccccceeeea
Answer: [Yes]
Justification: The research conducted in the paper conforms, in every respect, with the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification:
We have discussed the potential impacts of the paper in Appendix E
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
18

---

Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), faireess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The paper poses such risks.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: We have cited the assets used in the paper in Section 5.1 Section 5.2 and Section 5.4
Guidelines:
The answer NA means that the paper does use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
19

---

If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com/dataseta
latasets.papersstt
has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
this information is not available online, the authors are encouraged to reach out to the asset's s creators.
13. New Assets
Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Question:
Answer: [NA]
Currently, the paper does not release new assets. New assets, including code and toolkit, will be released upon the acceptance the paper with comprehensive documents.
Justification:
Guidelines:
The answer NA means that the paper does release assets.
Researchers should communicate the details the dataset/code/mooell as part their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsoureing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
The paper does not involve crowdsoureing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
20

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
21


Reviews:
[{"review_id": "iXRrrWtSv4", "reviewer": "Reviewer_imRj", "summary": "In this manuscript, the authors propose an ANF-based graph structure that efficiently handles XOR and AND operations in cryptographic problems. Additionally, they introduce CryptoANFNet, a message-passing neural network model designed to predict the satisfiability of cryptographic problems. The authors also present a key-solving algorithm that enhances key decryption accuracy.", "questions": "No", "limitations": "Discussed the limitations in Appendix B", "rating": 5, "confidence": 1, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. This work introduces efficient representations and learning strategies for encryption problems, which are highly innovative.\n2. In this work, CryptoANFNet excels in predicting satisfiability and key decryption, being up to 50 times faster and more accurate than existing methods.", "weaknesses": "1. In the “Introduction” of the article, the author mentioned that the application of ANF to existing SAT solvers is not as straightforward as CNF, but the article does not explicitly propose a solution that corresponds to it.\n2. Table 1 listed the parameters of SAT problems in CNF and ANF, but the article did not provide the algorithmic level explanations of these results.\n3. The author proposed CryptoANFNet and compared it with NeuroSAT. The results of the tests on different datasets were also listed in Table 2. However, the article lacks further comparison of the two algorithms.\n4. This article lacks a detailed description of the specific steps of the key-solving algorithm.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful review and for recognizing the innovative aspects of our work. We appreciate your positive assessment of our paper's contribution.Your feedback highlights the key strengths of our research, particularly the introduction of efficient representations and learning strategies for encryption problems. We are grateful for the opportunity to elaborate on our contributions and address any questions you have.\n\n---\n\nWe sincerely appreciate your time and effort in reviewing our manuscript.  We are committed to furthering this line of inquiry and contributing to the development of more efficient and effective cryptographic tools. We would sincerely appreciate it if you could reconsider your rating and we are more than happy to address any further concerns you may have.\n\n---\n\n#### Q1 \"In the “Introduction” of the article, the author mentioned that the application of ANF to existing SAT solvers is not as straightforward as CNF, but the article does not explicitly propose a solution that corresponds to it.\"\n\n**A1** Thank you for your comment. In line 54, we mention that “However, representing ANF as a graph for efficient learning is challenging, and applying it to existing SAT solvers is not as straightforward as CNF” for the following reasons:\n\n1. **Input Format Compatibility**: Existing traditional or ML-based SAT solvers predominantly accept CNF (Conjunctive Normal Form) as their input format. When dealing with cryptographic problems formulated in ANF (Algebraic Normal Form), it is necessary to convert ANF to CNF before inputting it into these solvers. This conversion process adds an extra step, making the application of ANF less straightforward compared to CNF.\n\n2. **Lack of ANF-based Graph Structures**: Unlike CNF, which has established graph representations such as Literal-Clause Graph (LCG) and Variable-Clause Graph (VCG) used in learning-based SAT solvers, ANF lacks similar graph structures. These graph representations are crucial for learning-based solvers as they facilitate efficient learning and problem-solving. The absence of well-defined ANF-based graph structures poses a significant challenge for applying learning-based approaches to ANF-formulated problems. This gap highlights the need for developing novel ANF-based graph structures to enable efficient learning and application in SAT solvers.\n\nTo address this challenge and enhance SAT practice within ANF, we propose a novel approach using an ANF-based graph structure to represent SAT instances relevant to cryptographic applications. This approach led to the development of CryptoANFNet, an ML-based SAT solver designed to directly predict the satisfiability of SAT instances in the ANF input format. By leveraging this method, we can effectively handle ANF-based SAT problems without the need for conversion to CNF, thereby streamlining the process and improving efficiency.\n\n---\n\n#### Q2 \"Table 1 listed the parameters of SAT problems in CNF and ANF, but the article did not provide the algorithmic level explanations of these results.\"\n\n**A2** Thank you for you question. We will provide a further explanation of Table 1 in two steps:\n\n1. **Literal and Clause Counts in ANF and CNF:** \n    - As stated in Section 3, Algebraic Normal Form(ANF) consist of Boolean equations, representing the conjunction of logical formulas in SAT instances. Each variable is referred to as a (vanilla) literal. In a Boolean equation, the right side is always 0 and the Boolean function on the left side, formed by the XOR connection of monomials, is called a clause. Each monomial is either a constant term 1, a (vanilla) literal, or a product of variables(literals).\n    - As stated in line 45, Conjunctive normal form(CNF) is a conjunction (and-ing) of clauses, with each clause consisting of adisjunction (or-ing) of the true and negated forms of literals. \n    - For the same cryptographic problem's SAT instance, let $n_a$  and $m_a$ denote the number of literals and clauses in ANF format, respectively, and $n_c$ and $m_c$ denote the number of literals and clauses in CNF format. Due to the different algebraic structure, CNF requires more literals and clauses to represent XOR operations in cryptographic problems. The rows corresponding to #literal and #clause in Table 1 reflect the number of literals and clauses in ANF and CNF formats, respectively.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "f32KTztvrv", "reviewer": "Reviewer_uZGu", "summary": "The paper strikes an interesting endeavor for introducing machine learning to address the Plaintext-Ciphertext Cryptographic Problems, which is to my best knowledge, new in literature. It lies in the between of AI and security and specifically crypto which goes beyond the line of research either in learning for combinatorics. I think this paper pushes the frontier of AI for discrete math. Overall I think the paper is interesting and worth publishing to the community to briduge the two communities: machine learning and crypto.", "questions": "1) how the presented techniques could impact the area of machine learning for crypto, in a more broad sense?\n2) Is there any impact or concerns to the world when the presented approach attains more success? What is the fundamental challenge for this line of research?", "limitations": "N/A", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1) the paper is well written which clearly introduces the background, the problem setting and the preliminaries. It is quite informative and could inspire the readers.\n2) specifically, the work introduces machine learning for plaintext-ciphertext satisfiability prediction. It on one hand outpeforms traditional heuristic methods by speed, and on the other hand outperforms peer learning-based NeuroSAT by accuracy.\n3) The authors further show extending their approach to the key decryption problem with a notable performance boost, compared with the one without our devised simplification approach.\n4) the experiments are themselves novel and well designed. The results are comprehensive and informative, which I think would inspire the future work in this emerging area.", "weaknesses": "1) the technical part is a bit simple from the top ML conference perspective, while of course this is often the case for machine learning applications to emerging areas", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your valuable comment and for recognizing its innovative aspects and experimental design. Your questions about the conclusions and insights offered by this paper are important and meaningful. We greatly appreciate the opportunity to elaborate on our contributions and address the points you've raised.\n\n---\n\nWe sincerely appreciate your insightful comments on our work. We fully agree that this research has the potential to foster collaboration and knowledge exchange between the machine learning and cryptography communities. Thank you again for your valuable comments and for recognizing the broad impact of our contributions. We are committed to continuing this line of research and look forward to seeing how it impacts future developments in AI-assisted cryptography and beyond.\n\n---\n\n#### W1 the technical part is a bit simple from the top ML conference perspective, while of course this is often the case for machine learning applications to emerging areas\n\n**A1** Thank you for your comment. We will address the technically non-trivial aspects of our work from the following aspects:\n\n1. **Introduction of ANF Formulas**:\n    We introduced the input format of SAT instances, ANF (Algebraic Normal Form), for efficiently solving SAT instances in cryptographic problems. ANF formulas can represent SAT instances in cryptographic problems with fewer literals and clauses, whereas CNF formulas, as used in NeuroSAT, often require a larger number of literals and clauses to represent common cryptographic operations like XOR. In this way, ANF formulas are more efficient for representing cryptographic problems.\n\n2. **ANF-Based Graph Representation**:\n    We proposed a new ANF-based graph representation to capture the operations in ANF, while NeuroSAT is based on a CNF-based graph representation (LCG). Since the high-order literals are used only as intermediate results in the message-passing process, the parameterized nodes in the ANF-based graph are less than in CNF-based graph.\n    \n    As shown in Table 1 of our paper, our ANF graph is more efficient than the general graph form used in NeuroSAT. Here, we provide a summary table comparing ANF with two types of CNF-based graph representations, Literal-Clause Graph (LCG) and Variable-Clause Graph (VCG). This demonstrates that our proposed ANF-based graph representation remains efficient.\n    |          | Datasets  | SR(5) | SR(25) | Simon 3-8-16 | Simon 3-16-32 | Simon 6-8-16 | Simon 6-16-32 | Speck 3-8-16 | Speck 6-8-16 |\n    | -------- | --------- | ----- | ------ | ------------ | ------------- | ------------ | ------------- | ------------ | ------------ |\n    |          | #Literals | 6     | 424    | 25           | 49            | 49           | 97            | 57           | 183          |\n    | CNF(LCG) | #Clauses  | 75    | 5492   | 195          | 403           | 735          | 1519          | 360          | 2950         |\n    |          | #Nodes    | 87    | 6340   | 245          | 501           | 833          | 1713          | 474          | 3316         |\n    |          | #Literals | 6     | 424    | 25           | 49            | 49           | 97            | 57           | 183          |\n    | CNF(VCG) | #Clauses  | 75    | 5492   | 195          | 403           | 735          | 1519          | 360          | 2950         |\n    |          | #Nodes    | 81    | 5916   | 220          | 452           | 784          | 1616          | 417          | 3133         |\n    |          | #Literals | 5     | 25     | 24           | 48            | 48           | 96            | 56           | 128          |\n    | ANF      | #Clauses  | 11    | 26     | 24           | 48            | 48           | 96            | 64           | 136          |\n    |          | #Nodes    | 27    | 77     | 72           | 144           | 144          | 288           | 184          | 400          |\n\n3. **Model Structure for ANF-Based Graph Representation**:\n\n    We proposed a model structure for handling ANF-based graph representation, which have better performance than NeuroSAT in MQ problem and can effectively extend to higher-order ANF formulas. \n    Due to the high-order literals in ANF formulas, the number of literal types increases exponentially with the order. Therefore, as stated in line 216 of Section 4.3, CryptoANFNet only retains embeddings for first-order nodes (vanilla literals) and clause nodes. High-order nodes are used only as intermediate results in the message-passing process. For high-order ANF formulas, i.e., AND terms with more than 2 variables, we have the similar message-passing process shown below:\n    - For the message-passing process from vanilla literal node to clause node, we have:\n\n      $L^{(t)}_{l2c} = L\\_{l2l}(M^T\\_{l2l}L^{(t)})$ \n\n      $[C^{(t)}\\_{m,\\text{pos}}, C^{(t)}\\_{m,\\text{neg}}] = M_{l2c}^T L_{\\text{msg}}(L^{(t)}_{l2c})$\n\n    - For the message-passing process from clause node to vanilla literal node, we have:\n\n      $L^{(t)}\\_{c2l} = M\\_{l2c} C\\_{\\text{msg}}([C^{(t)}\\_{\\text{pos}}, C^{(t)}\\_{\\text{neg}}])$\n\n      $L^{(t)}\\_m = M\\_{l2l} L\\_{l2m}(L^{(t)}\\_{c2l})$  \n\n    where $M_{l2l}$ is a **sparse** adjacency matrix defined by $M_{l2l}(i, j) = 1$(the i-th vanilla literal appears in the j-th high-order literal) and $M_{l2c}$ is the adjacency matrix defined by $M_{l2c}(i, j) =1$(the $i$-th high-order literal appears in the $j$-th clause). \n    Using the sparse matrix $M_{l2l}$, we only need to retain the edges between vanilla literal nodes and higher-order nodes, without storing the entire adjacency matrix, which grows exponentially with higher orders. This approach effectively handles datasets comprising SAT instances with literals in various orders.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "jDPJm376ZE", "reviewer": "Reviewer_6xjG", "summary": "This paper introduces an approach to handling cryptographic problems by transforming them into Boolean Satisfiability (SAT) problems using a graph structure based on Arithmetic Normal Form (ANF) to efficiently manage XOR operations, which are prevalent in cryptography. It proposes CryptoANFNet, a graph learning framework that predicts plaintext-ciphertext satisfiability using a message-passing scheme. CryptoANFNet demonstrates superior scalability, achieving a 50x speedup over heuristic solvers and outperforming the state-of-the-art learning-based SAT solver NeuroSAT in terms of accuracy. Additionally, the paper presents a key-solving algorithm that simplifies ANF-based SAT instances, resulting in improved key decryption accuracy for datasets generated from Simon and Speck algorithms.", "questions": "* What is the key novelty in the model part when compared to the existing work, NeuroSAT? It seems like the key difference lies in the different message passing design.\n* Does this paper select the-state-of-the-art works as its baselines? This paper considers some works that are in the form of competition, e.g., [42], while there are some related works, e.g., \"Learning To Solve Circuit-SAT: An Unsupervised Differentiable Approach\".\n* For dataset with encryption algorithms, this paper generates data with SIMON and SPECK, which are lightweight block cipers and not really popular in real-world applications. Can this paper extend its scope to more popular and complex ciphers, such as AES?", "limitations": "Limitations are addressed.", "rating": 5, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "* This paper formalize the ANF formula as the Multivariate Quadratic ( MQ ) problem that reduce the complexity of the problem\n* The evaluation results demonstrate a significant acceleration on SMT solving. 50x speedup is surprisingly good.", "weaknesses": "* The proposed approach of using graph neural network and message passing is less novel considering its close design compared to NeuroSAT.\n* For performance evaluation and baseline selection, this paper doesn't compare itself to state-of-the-art approaches.\n* This paper doesn't include popular encryption algorithms, such as AES, in its dataset.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your valuable comment and for recognizing the significance of our work in formalizing the ANF formula as a Multivariate Quadratic (MQ) problem. We appreciate your acknowledgment of how this approach reduces the complexity of the problem.  We are pleased to address our contribution in detail.\n\n---\n\nWe hope this response clarifies the importance of our work in reducing the complexity of cryptographic problems and significantly improving SAT solving efficiency. We believe this has the potential to open up new avenues for research and practical applications. We are committed to continuing this line of research and look forward to making further progress in this area.\n\n---\n\n#### W1&Q1 \"What is the key novelty in the model part when compared to the existing work, NeuroSAT? It seems like the key difference lies in the different message passing design.\"\n\n**A1** Thank you. CryptoANFNet is inspired by some excellent previous works, like NeuroSAT, but we do not consider our key novelty to be incremental. We will show our key novelty in the following aspects.\n\n1. **Introduction of ANF Formulas**:\n    We introduced the input format of SAT instances, ANF (Algebraic Normal Form), for efficiently solving SAT instances in cryptographic problems. ANF formulas can represent SAT instances in cryptographic problems with fewer literals and clauses, whereas CNF formulas, as used in NeuroSAT, often require a larger number of literals and clauses to represent common cryptographic operations like XOR. In this way, ANF formulas are more efficient for representing cryptographic problems.\n\n2. **ANF-Based Graph Representation**:\n    We proposed a new ANF-based graph representation to capture the operations in ANF, while NeuroSAT is based on a CNF-based graph representation (LCG). Since the high-order literals are used only as intermediate results in the message-passing process, the parameterized nodes in the ANF-based graph are less than in CNF-based graph.\n    \n    As shown in Table 1 of our paper, our ANF graph is more efficient than the general graph form used in NeuroSAT. Here, we provide a summary table comparing ANF with two types of CNF-based graph representations, Literal-Clause Graph (LCG) and Variable-Clause Graph (VCG). This demonstrates that our proposed ANF-based graph representation remains efficient.\n    |          | Datasets  | SR(5) | SR(25) | Simon 3-8-16 | Simon 3-16-32 | Simon 6-8-16 | Simon 6-16-32 | Speck 3-8-16 | Speck 6-8-16 |\n    | -------- | --------- | ----- | ------ | ------------ | ------------- | ------------ | ------------- | ------------ | ------------ |\n    |          | #Literals | 6     | 424    | 25           | 49            | 49           | 97            | 57           | 183          |\n    | CNF(LCG) | #Clauses  | 75    | 5492   | 195          | 403           | 735          | 1519          | 360          | 2950         |\n    |          | #Nodes    | 87    | 6340   | 245          | 501           | 833          | 1713          | 474          | 3316         |\n    |          | #Literals | 6     | 424    | 25           | 49            | 49           | 97            | 57           | 183          |\n    | CNF(VCG) | #Clauses  | 75    | 5492   | 195          | 403           | 735          | 1519          | 360          | 2950         |\n    |          | #Nodes    | 81    | 5916   | 220          | 452           | 784          | 1616          | 417          | 3133         |\n    |          | #Literals | 5     | 25     | 24           | 48            | 48           | 96            | 56           | 128          |\n    | ANF      | #Clauses  | 11    | 26     | 24           | 48            | 48           | 96            | 64           | 136          |\n    |          | #Nodes    | 27    | 77     | 72           | 144           | 144          | 288           | 184          | 400          |\n\n3. **Model Structure for ANF-Based Graph Representation**:\n\n    We proposed a model structure for handling ANF-based graph representation, which have better performance than NeuroSAT in MQ problem and can effectively extend to higher-order ANF formulas. \n    Unlike NeuroSAT, which retains embeddings for all literal nodes that may appear in clauses, the approach for ANF formulas presents a different challenge. Due to the high-order literals in ANF formulas, the number of literal types increases exponentially with the order and retaining embeddings for all possible literals would incur unacceptable costs. Therefore, unlike NeuroSAT, as stated in line 216 of Section 4.3, CryptoANFNet only retains embeddings for first-order nodes (vanilla literals) and clause nodes. High-order nodes are used only as intermediate results in the message-passing process. For high-order ANF formulas, i.e., AND terms with more than 2 variables, we have the similar message-passing process shown below:\n    - For the message-passing process from vanilla literal node to clause node, we have:\n\n      $L^{(t)}_{l2c} = L\\_{l2l}(M^T\\_{l2l}L^{(t)})$ \n\n      $[C^{(t)}\\_{m,\\text{pos}}, C^{(t)}\\_{m,\\text{neg}}] = M_{l2c}^T L_{\\text{msg}}(L^{(t)}_{l2c})$\n\n    - For the message-passing process from clause node to vanilla literal node, we have:\n\n      $L^{(t)}\\_{c2l} = M\\_{l2c} C\\_{\\text{msg}}([C^{(t)}\\_{\\text{pos}}, C^{(t)}\\_{\\text{neg}}])$\n\n      $L^{(t)}\\_m = M\\_{l2l} L\\_{l2m}(L^{(t)}\\_{c2l})$  \n\n    where $M_{l2l}$ is a **sparse** adjacency matrix defined by $M_{l2l}(i, j) = 1$(the i-th vanilla literal appears in the j-th high-order literal) and $M_{l2c}$ is the adjacency matrix defined by $M_{l2c}(i, j) =1$(the $i$-th high-order literal appears in the $j$-th clause). \n    Using the sparse matrix $M_{l2l}$, we only need to retain the edges between vanilla literal nodes and higher-order nodes, without storing the entire adjacency matrix, which grows exponentially with higher orders. This approach effectively handles datasets comprising SAT instances with literals in various orders.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "WKCOlnBm2H", "reviewer": "Reviewer_ZcPU", "summary": "The paper explores an approach for predicting the satisfiability of Algebraic Normal Form (ANF) Boolean SAT instances by graph neural networks (GNN). The approach is similar to the framework of NeuroSAT but a new graph structure is proposed for handling the quadratic terms in ANN. Experiments indicate that the proposed approach reaches better accuracy in predicting the satisfiability on certain ANF instances compared with NeuroSAT on CNF and the prediction time is much faster than the running time of SAT solvers.", "questions": "1. Can the proposed approach be extended to allowing AND terms with more than 2 variables? If so, how should one handle the exponentially many nodes in a graph?\n\n2. Would it be possible for the proposed approach to output a proof for its predication? For example, can you extract a satisfying assignment or an UNSAT core from the embeddings of the GNN?", "limitations": "Please see the discussion above.", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The paper picks up several interesting and important aspects. First, while CNF-based SAT solvers are dominating and CNF is the most prevalent format in SAT solving, non-CNF constraints, such as ANF, can still be useful in many applications. Encoding them into CNF can harm the performance of SAT solvers and it is desirable to have native solvers for those types of constraints. Second, using machine learning for an end-to-end framework for combinatorial problems has been an active research area.\n\nThis paper is clearly written, with technical details at an appropriate level.", "weaknesses": "1. The results of this paper, in my opinion, are not well claimed. The proposed approach based on GNN is only a predictor with errors. In contrast, SAT solvers must find proof for the answers they give, i.e., finding a satisfying assignment or proving unsatisfiability. Comparing the running time of making a prediction by GNN and that of a SAT solver is not fair, which should be clearly stated in the paper.\n\n2. The proposed approach only considers the ANF format up to order 2 while higher ordered cases are not discussed. This limitation makes it doubtful whether the proposed graph structure can be useful in general.\n\nAfter the rebuttal session, I decided to raise my score from 4 to 5.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "## Response to Reviewer ZcPU (Rating: 4 / Confidence: 4)\n\nThank you for your thoughtful response and for highlighting the key contributions of our paper. We are pleased that you recognized the appropriate technical depth of our work. Your elaboration on the significance of non-CNF constraints, particularly ANF, and the potential of machine learning in combinatorial problem-solving further underscores the importance of our research. Your astute observations have pinpointed crucial aspects of our work, providing us with an excellent opportunity to expound on the core contributions of our paper. We are delighted to address your points in detail below.\n\n---\n\nWe hope that this response clarifies the importance of our work in dealing with non-CNF constraints (especially ANFs) and in solving combinatorial problems using machine learning techniques. We believe that our approach has the potential to open up new avenues for research and practical applications in areas where traditional CNF-based methods may not be ideal. Our method also has great potential for solving higher-order ANF problems. We remain committed to advancing this area of research. We would appreciate it if you would reconsider your rating.\n\n---\n\n#### Q2 \"Would it be possible for the proposed approach to output a proof for its predication? For example, can you extract a satisfying assignment or an UNSAT core from the embeddings of the GNN?\"\n\n**A1** Thank you for your comment. We can provide proof for our prediction using the following methods:\n\n1. **Key-Solving Process**: In the plaintext-ciphertext cryptographic problem, CryptoANFNet can determine the assignment for a specific bit of the key by following the key-solving process outlined in Section 4.4 of our paper. Using the key-solving algorithm described, CryptoANFNet  can sequentially deduce the value of each key bit. As shown in Table 3 it demonstrates its capability in cryptographic key-solving tasks. \n\n2. **Extracting Satisfying Assignments**: CryptoANFNet can also extract satisfying assignments from the embeddings of the literals. To further validate this, we conducted experiments to predict assignments using the embeddings generated by CryptoANFNet on SR datasets. The results, as shown below, illustrate CryptoANFNet's effectiveness in producing assignments from the learned embeddings.\n\n|Dataset|SR(25)|SR(5)-high|SR(10)-high|\n|---|---|---|---|\nNeuroSAT | 57.0% | 53.5% | 51.0%\nCryptoANFNet | **71.5%**  | **71.0%** | **63.5%**\n\n---\n\n#### W1 \"The results of this paper, in my opinion, are not well claimed. The proposed approach based on GNN is only a predictor with errors. (see weaknesses).\"\n\n**A3** Thank you. We acknowledge the concern regarding the potential for prediction errors in ML-based solvers. No model can guarantee 100% accuracy across all datasets. But, as demonstrated in **Section 5.4** of the paper, CryptoANFNet exhibits a significantly faster solving speed compared to traditional solvers. With this rapid solving speed, our model can be effectively utilized as a solver in these practical applications below:\n\n1. As detailed in Section 4.4 of our paper, using the Key-solving algorithm, CryptoANFNet can sequentially determine the value of each specific bit of the key in a plaintext-ciphertext problem. \n\n2. Besides, CryptoANFNet can also extract satisfying assignments from the embeddings of the literals, as shown in **A1**. \n\nIn practice, this solver can achieve a preliminary solution for a key or a satisfying assignment with relatively high accuracy. Since the efficiency of verifying the correctness of these solutions is very high, CryptoANFNet offer a significant advantage over traditional solvers in terms of application efficiency, aligning with the primary research objective of our paper. \n\nTo demonstrate the feasibility of our approach, we compared the running time of making a prediction by GNN and that of a SAT solver. As shown in Table 4 of our paper, ML-based solvers like CryptoANFNet exhibit nearly 50x faster solving speed. Additionally, Table 3 in the paper and the table in **A1** indicate that CryptoANFNet can obtain a preliminary solution for a key or a satisfying assignment with relatively high accuracy.\n\n---\n\n#### W2&Q1 \"The proposed approach only considers the ANF format up to order 2 while higher ordered cases are not discussed.\"\n\n**A2** Thank you. We will address your concerns from the following three aspects:\n\n1. **In cryptography, MQ (Multivariate Quadratic) problems represented by second-order ANF (Algebraic Normal Form) are of great significance and have wide applications.** As explained in Section 3 of our paper, operations commonly used in cryptographic problems—such as modular addition, XOR, AND, left circular shift, and right circular shift—can be effectively represented using second-order ANF formulas. This conversion of cryptographic problems into MQ problems highlights the broad applicability of second-order ANF. Besides, previous research [cite 1] has already underscored the importance and application of MQ problems in cryptography. Second-order ANF is versatile enough to handle many tasks, demonstrating its extensive range of applications.\n\n2. **Second-order ANF formulas are complete, meaning that they can represent any finite-sized circuit or cryptographic problem.** Research [cite 2] has shown that CNF formulas can be converted into ANF formulas. Since CNF is complete, ANF formulas are inherently complete as well. Furthermore, higher-order ANF formulas can be converted into second-order ANF formulas. For a native method, consider a higher-order ANF formula like $x_1x_2x_3+x_3x_4=0$. By introducing the dummy variable $u_1$ and the equation $u_1+x_1x_2=0$, we can transform the original formula into $u_1x_3+x_3x_4=0$, effectively converting the higher-order ANF formula into a second-order ANF formula. In practice, more efficient conversion methods[cite 3] are proposed to reduce the number of dummy variables.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
We sincerely appreciate the reviewers’ time, valuable feedback, and constructive suggestions. Overall, the reviewers have deemed our work as "highly innovative" (imRj), "well-written" (uZGu, ZcPU), and having the appropriate  level of technical detail (ZcPU). They have acknowledged our methodology and experiment design as "novel and well-designed" (imRj, uZGu), with "excels" and "outperforms" being common sentiments. Furthermore, the results of our work have been described as "surprisingly good", "comprehensive", and "informative" (6xjG, uZGu). The main concerns are whether our proposed method is limited to 2nd order ANF formulations, whether it can be generalised to other popular ciphers, whether it can deliver a proof for its predication and the difference between the proposed CryptoANFNet and previous work such as NeuroSAT. To preempt this potential misunderstandings that might impact the evaluation of our work, we first restate our contributions compared to the previous works and address the concerns.

1. **Contributions**
    - **Efficient Input Formats and Graph Representations for SAT Instances**:
        Based on the Arithmetic Normal Form (ANF), we propose a graph structure to succinctly represent the excessive XOR operations in cryptographic problems. We then design two ways to encode the AND operations in the ANF-based graph to represent SAT instances derived from cryptographic problems. Our ANF-graph is more efficient than the general graph form for SAT Literal-Clause Graph (LCG) and Variable-Clause Graph (VCG).
    - **Better Performance**:
        We propose (supervised) learning to solve (for the first time to our knowledge) the challenging cryptographic problem: plaintext-ciphertext satisfiability prediction, which could otherwise be intractable by traditional SAT methods. Our proposed GNN-based classifier CryptoANFNet with ANF-based SAT instances as input,  achieves a 50x speedup over heuristic solvers, and outperforms the SOTA learning-based SAT solver NeuroSAT by 96% vs. 91% and 72% vs. 55% accuracy on small and large scale datasets, generated from Simon and Speck algorithms, respectively. Additionally, we referred to the benchmark G4satbench  to compare CryptoANFNet with various baselines, and the following table show that CryptoANFNet exhibits better performance on different datasets.
    - **Efficient Model Structures and Adaptability to SAT instances in high-Order ANF Formulas**:
        We design the CryptoANFNet to retain fewer embedding parameters, making the model more efficient.. As described in Section 4.3 of our paper, ANF clauses involve both AND and OR operations. When constructing the ANF graph for CryptoANFNet, there are first-order nodes, positive and negative clause nodes, and high-order nodes like $x_1x_2$. To do the message-passing process efficiently, CryptoANFNet only retains embeddings for first-order nodes (vanilla literals) and clause nodes, which making the model more efficient.
        Since high-order nodes are used only as intermediate results in the message-passing process, CryptoANFNet can be adapted to high-order ANF formulas. Using the sparse adjacency matrix, we only need to retain the edges between vanilla literal nodes and higher-order nodes, without storing the entire adjacency matrix, which grows exponentially with higher orders. This approach effectively handles datasets comprising SAT instances with literals in various orders.
    - **Key solving algorithm**
        We extend to the key decryption problem. We propose a key-solving algorithm that derives ANF-based SAT instances as further simplified by our devised techniques, from the plaintext and ciphertext, and use the output of two derived SAT instances to infer the key values. It boosts the accuracy by 76.5%->82% and 72%->75%, on datasets generated from Simon and Speck, respectively. 

2. Discussion
    - **Generalization to high-order ANF formulas**: Because high-order nodes are used only as intermediate results in the message-passing process, CryptoANFNet can be adapted to high-order ANF formulas by using the sparse adjacency matrix. CryptoANFNet still outperforms NeuroSAT on second-order ANF formulas dataset and better performance on higher-order ANF formulas.
         
    - **Generalization to other ciphers**: Theoretically, the methods proposed in this paper can be extended to more complex block ciphers that can be represented by ANF formulas. However, in practice, the efficiency of traditional solvers limits the generation of datasets for some complex block ciphers. Some block cipher structures (such as the use of S-boxes) lack efficient algorithms for conversion to ANF or CNF formulas. This results in a large number of clauses and literals, making it challenging to generate efficient datasets for the network to train on.
    
    - **Deliver a proof for the predication**: We can provide proof for our prediction using the key solving algorithm. Using the key-solving algorithm described, CryptoANFNet can sequentially deduce the value of each key bit. Besides, CryptoANFNet can also directly extract satisfying assignments of the key from the embeddings of the literals.
    
    - **Unfair comparsion of the running time between GNN and that of a SAT solver**:  We acknowledge the reviewer’s concerns regarding the potential for prediction errors in ML-based solvers. No model can guarantee 100% accuracy across all datasets. But, GNN-based solver can be used to get a preliminary solution for a key or a satisfying assignment with relatively high accuracy. Since the efficiency of verifying the correctness of these solutions is very high, these GNN-based solvers, like CryptoANFNet offer a significant advantage over traditional solvers in terms of application efficiency, aligning with the primary research objective of our paper. There, we perform this comparison to validate the advantages of CryptoANFNet in this regard.

Meta-review: **Summary:**

The paper proposes CryptoANFNet, a graph neural network approach for predicting satisfiability of Boolean SAT instances in Algebraic Normal Form (ANF), particularly for cryptographic problems. It introduces a new graph structure to efficiently handle XOR operations common in cryptography. CryptoANFNet demonstrates superior performance compared to existing methods like NeuroSAT in terms of accuracy and speed on certain datasets.

**Strengths:**

- Novel approach to handling non-CNF constraints (ANF) which are relevant for cryptographic problems
- Efficient graph representation for ANF formulas
- Good performance in terms of accuracy and speed compared to baselines
- Ability to handle higher-order ANF formulas beyond just quadratic terms

**Weaknesses:**

- Initially limited to 2nd order ANF, though authors later showed it can handle higher orders
- Comparison of prediction time to complete SAT solver runtime was seen as unfair by some reviewers
- Limited evaluation on more complex ciphers like AES due to practical constraints

**Key Discussion Points:**

- *Novelty compared to NeuroSAT:* Authors clarified the key differences in input format, graph representation, and model structure.
- *Handling higher-order ANF:* Authors demonstrated how CryptoANFNet can be extended to higher-order formulas efficiently.
- *Proof generation:* Authors showed CryptoANFNet can provide satisfying assignments and solve for encryption keys sequentially.
- *Comparison to incomplete solvers:* In response to reviewer feedback, authors added comparisons to incomplete SAT solvers like GSAT and WalkSAT, showing CryptoANFNet still offers speed advantages.
- *Applicability to complex ciphers:* Authors explained challenges in applying the method to AES due to limitations in generating efficient datasets, not theoretical limitations of the approach.

Overall, the reviewers acknowledged the paper's contributions and innovations, particularly after clarifications in the rebuttal. The main remaining concerns were about fair comparisons to other solvers and the current practical limitations for very complex ciphers. Most reviewers increased or maintained positive scores after the rebuttal, suggesting the paper makes a valuable contribution to the field.
Decision: Accept (poster)