3
저는 AES와 비슷한 경량 블록 암호 인 Piccolo에 대한 공격을 공식화하기 위해 Cryptominisat (유사한 기능을 수행 할 것입니다)을 사용하려고했습니다.SAT 솔버 및 cnf 파일에 대해서
방정식은 다음과 같이이다 : | Z2 |
Z = Z1 ... | Z16 1 <를 = 난 < =이어서 16
, UI = (1 + Z (4I -3-))^(1 + Z (4I-2))^(1 + Z (4I-1))^(1 + Z (4I)), 1 = 1 < < = 4
이어서, (1 + 1) V (1 + u2) V (1 + u3) V (1 + u4) = 1; ui + uj = 1, i < = i < = 4
다음 단계에 관해 도움이 필요합니다. 나는 공격과 암호 해독을위한 CNF 방정식을 준비했습니다. 실제로 그것을 솔버로 사용하고 CNF 파일 형식으로 저장하는 방법에 대한 도움이 필요합니다. 나는 인터넷 곳곳을 둘러 보았으나 어느 곳에서나 명확한 방법이 주어지지 않았다. 어떤 도움을 주시면 감사하겠습니다. 더 자세한 정보가 필요하면 언제든지 물어보십시오. 위의 방정식을 cnf 파일에 넣어야합니다.
관련된 방정식이 꽤 복잡하기 때문에 (더 많은 내용이 있습니다.) cnf 파일과 그 작업에 대한 몇 가지 참조 또는 예제가 멋지게 나옵니다.
감사합니다. 필자는 AES와 매우 흡사 한 Piccolo에서 작업 중이므로 관련 Block 암호를 해결하는 데 사용되는 예제 CNF 파일이 도움이 될 것입니다. 이 형식으로 복잡한 연쇄 방정식을 쓰는 방법에 대한 더 나은 아이디어가 필요합니다. 감사! –
문제는 아마도 방정식에 SAT 해결사가 직접 지원하지 않는 연산자가있을 것입니다. 예를 들어 XOR을 추측 할 수 있습니까? 방정식을 변환하는 프로그램을 작성해야 할 수도 있지만, 누군가가 암호 분석의 필요성에 맞게 조정 된 SAT 해결자를 알고있을 수도 있습니다 ... – Tilo
아니요, 방정식은 모두 cnf 형식입니다. 그러나 오류 및 암호 해독을 방정식으로 표현해야합니다. 예를 들어, 결함에 대한 방정식은 다음과 같습니다. Z = z1 | z2 | ... | z16, 1 <= i <= 16 ui = (1 + z (4i-3))^((1 + z (4i-1))^(1 + i (4i)), 1 <= i <= 4 그리고 내가 질문에서 설명한 마지막 방정식. 내가 지금 나 자신을 더 잘 설명하기를 바란다. –