密码学SAT入门003——关于流密码入门算法A5-1的学习

A5_1.alg program describes 128 steps of the A5/1 keystream generator which produced 128 keystream bits (with constant len).
The translation of this program results in a5_1_128.cnf CNF-formula.

Values of registers cells at the start are encoded with Boolean variables number 1 .. 64, in particular:
- variables number 1 .. 19 encode values of cells of the first register(regA),
variable number 1 corresponds to cell regA[0], ..., variable number 19 - to cell regA[18];
- variables number 20 .. 41 encode values of cells of the second register(regB),
variable number 20 corresponds to cell regB[0], ..., variable number 41 - to cell regB[21];
- variables number 42 .. 64 encode values of cells of the third register(regC),
variable number 42 corresponds to cell regC[0], ..., variable number 64 - to cell regC[22];

Keystream output is always encoded by last Boolean variables in the order in which generator creates corresponding keystream bits.
So in a5_1_128.cnf keystream bits are encoded with variables number 8298, ..., 8425,
where variable number 8298 encodes 1st keystream bit, ... , variable number 8425 encodes 128th keystream bit.

To construct a cryptanalysis problem one needs to add to this CNF known keystream bits via unit clauses.
Secret key for this problem is the assignment of first 64 variables that can be extracted from the satisfying assignment of the CNF.

 1 define len 128;
 2 __in bit regA[19];
 3 __in bit regB[22];
 4 __in bit regC[23];
 5 __out bit result[len];
 6 
 7 bit shift_rslosA()
 8 {
 9     bit x = regA[18];
10     bit y = regA[18]^regA[17]^regA[16]^regA[13];
11     for(int j = 18; j > 0; j=j-1)
12     {
13         regA[j] = regA[j-1];
14     }
15     regA[0] = y;
16     return x;
17 }
18 
19 bit shift_rslosB()
20 {
21     bit x = regB[21];
22     bit y = regB[21]^regB[20];
23     for(int j = 21; j > 0; j=j-1)
24     {
25         regB[j] = regB[j-1];
26     }
27     regB[0] = y;
28     return x;
29 }
30 
31 bit shift_rslosC()
32 {
33     bit x = regC[22];
34     bit y = regC[22]^regC[21]^regC[20]^regC[7];
35     for(int j = 22; j > 0; j=j-1)
36     {
37         regC[j] = regC[j-1];
38     }
39     regC[0] = y;
40     return x;
41 }
42 
43 bit majority(bit A, bit B, bit C)
44 {
45     return A&B|A&C|B&C;
46 }
47 
48 void main()
49 {
50     int midA = 8;
51     int midB = 10;
52     int midC = 10;
53     bit maj;
54     for(int i = 0; i < len; i= i + 1)
55     {
56         maj = majority(regA[midA],regB[midB],regC[midC]);
57         if(!(maj^regA[midA])) shift_rslosA();
58         if(!(maj^regB[midB])) shift_rslosB();
59         if(!(maj^regC[midC])) shift_rslosC();                
60         result[i] = regA[18]^regB[21]^regC[22];
61     }
62 }

p cnf 8425 38262
c input variables 64
c literals count 128374
65 9 30 0
65 9 52 0
-65 9 -30 -52 0
65 -9 -52 0
-65 -9 30 52 0
65 -9 -30 0
66 -19 65 0
66 -18 -65 0
-66 19 65 0
-66 18 -65 0
67 -18 65 0
67 -17 -65 0
-67 18 65 0
-67 17 -65 0