SHA-256 충돌 공격을 위한 프로그래밍 SAT

암호 해시 함수는 데이터 보안을 보장하는 데 중요한 역할을 하며, 가변 길이 입력에서 고정 길이 해시를 생성합니다. SHA-256 해시 함수는 20년 이상의 치열한 검토 후에도 데이터 보안에 대한 신뢰성을 보유하고 있습니다. 이 함수의 중요한 속성 중 하나는 충돌 저항성으로, 동일한 해시를 가진 두 개의 서로 다른 입력을 찾는 것이 불가능함을 의미합니다. 현재 가장 좋은 SHA-256 충돌 공격은 차별적 암호 분석을 사용하여 단계가 줄어든 SHA-256의 단순화된 버전에서 충돌을 찾고 있으며, 이를 통해 충돌을 찾는 것이 가능해졌습니다. 본 논문에서는 단계가 줄어든 SHA-256 충돌을 검색하기 위한 도구로 만족 가능성(SAT) 해결기를 사용하고, 일관성을 감지하고 해결기가 스스로 발견하지 못하는 정보를 유추하기 위해 컴퓨터 대수 시스템(CAS)의 도움으로 해결기를 동적으로 안내합니다. 우리의 하이브리드 SAT + CAS 해결기는 순수 SAT 접근 방식보다 훨씬 우수하여 더 많은 단계를 포함하는 단계가 줄어든 SHA-256의 충돌을 찾는 데 성공했습니다. SAT + CAS를 사용하여 우리는 수정된 초기화 벡터를 가진 SHA-256의 38단계 충돌을 발견했습니다. 이는 Mendel, Nad, Schl\"affer의 고도로 정교한 탐색 도구에 의해 처음 발견된 것입니다. 반면, 순수 SAT 접근 방식은 28단계를 초과하는 충돌을 찾는 데 실패했습니다. 하지만 저희의 작업은 SAT 해결기 CaDiCaL과 그 프로그래밍 인터페이스 IPASIR-UP만을 사용합니다.