full-disclosure - help fuzzing/finding Horn CNF formula

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [thread-next>] [day] [month] [year] [list]

Message-ID: <20100219085620.GA5908@sivokote.iziade.m$>
Date: Fri, 19 Feb 2010 10:56:20 +0200
From: Georgi Guninski <guninski@...inski.com>
To: full-disclosure@...ts.grok.org.uk
Subject: help fuzzing/finding Horn CNF formula

i know i am dumb.

i am looking for a HORN CNF that is SAT if and only if |x != y| ($x \ne y$) for boolean x,y.

using the Horn constraints in [1] (at most k '1's) + the sought inequality/negation, it might be possible to encode Exact Sat (XSAT) to fast Horn CNF (md5 preimage falls in this case)

i am not sure if such CNF formula exists though current academics claim Horn Sat is "P-complete", i.e. powerful enough for the formula.

note that the size of the CNF doesn't matter much (it cares about just 2 variables, the other vars are temp).

i failed fuzzing it :)

[1] Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
C Sinz
http://www-sr.informatik.uni-tuebingen.de/~sinz/CardConstraints/cp2005.pdf

_______________________________________________
Full-Disclosure - We believe in it.
Charter: http://lists.grok.org.uk/full-disclosure-charter.html
Hosted and sponsored by Secunia - http://secunia.com/