2

そこで、同僚が考案したいくつかの方程式を cnf ファイル形式に変換して、オープン ソースの sat ソルバーで使用できるようにしました。

方程式は次のとおりです。

S ボックス:

y1= 1+x1+x2+x4+x1x2

y2= 1+x1+x2+x3+x3x2

y3= 1+x1+x4+x1x2+x1x3+x2x3+x3x4+x1x2x3

y4= x1+x2+x3+x1x3+x1x4+x2x4+x3x4+x1x2x3+x2x3x4

混合カラム:

Y1= 2.X1+3.X2+1.X3+1.X4

Y2= 1.X1+2.X2+3.X3+1.X4

Y3= 1.X1+1.X2+2.X3+3.X4

Y4= 3.X1+1.X2+1.X3+2.X4

. denotes multiplication in GF(2^4) with x^4+x+1 being the irreducible polynomial.

攻撃には、

Z= z1|z2|...|z16, 1<= i<=16

Then, ui= (1+z(4i-3)) ^ (1+ z(4i-2)) ^ (1+z(4i-1)) ^ (1+ z(4i)), 1<=i<=4

Then, (1+u1) V (1+u2) V (1+u3) V (1+u4) =1; ui + uj=1, i<=i<=j<=4

これらを cnf ファイル形式に変換する方法について、参照リンクを含め、情報をいただければ幸いです。cnf ファイル形式で上記のような制約を指定することに関するヘルプもいただければ幸いです。

4

1 に答える 1

2

ここに1つの提案があります：

  1. 算術演算 (GF(16) での加算、乗算など) を回路としてエンコードします。デジタル ロジック デザインのコースを受講したことがある場合は、その方法がわかります。そうでないとちょっと大変です。さらに詳しい情報が必要な場合は、あなたの経歴を教えてください。具体的な提案をしようと思います。
  2. Tseitin 変換を使用して、回路を CNF に変換します。

PS。SAT ソルバーを使用して暗号を実行しようとしているようです。私の知る限り、これはMiniSatのような標準的なソルバーではうまく機能しません。CryptoMiniSatの方が優れているかどうかはわかりませんが、この種の問題は従来、SAT ソルバーにとって困難であったことを覚えておくとよいでしょう。

于 2014-03-03T02:13:11.097 に答える