techvoltage · August 27, 2017 09:18 · Aug 27, 2017 · Aug 27, 2017 · Aug 27, 2017 · Aug 27, 2017
diff --git a/Keygen-2.py b/Keygen-2.py
@@ -17,6 +17,7 @@ def netcat(hostname, port, content):
     s.close()
 
 # Return the first "M" models of formula list of formulas F 
+# https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
 def get_models(s, M,password):
     result = []
     #s = Solver()

diff --git a/Keygen-2.py b/Keygen-2.py
@@ -76,5 +76,5 @@ def verify(l,s):
 #print s.check()
 p=get_models(s, 10,password)
 #result=get_models(s, 10,password)
-print p
+#print p
 netcat("defcon.org.in",8083,p)
diff --git a/Keygen-2.py b/Keygen-2.py
@@ -1,10 +1,21 @@
 import string
 import random
 from z3 import *
+import socket
+
+def netcat(hostname, port, content):
+    s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+    s.connect((hostname, port))
+    s.sendall(content)
+    s.shutdown(socket.SHUT_WR)
+    while 1:
+        data = s.recv(1024)
+        if data == "":
+            break
+        print "Received:", repr(data)
+    print "Connection closed."
+    s.close()
 
-s = Solver()
-str_="firhfgferfibbqlkdfhh"
-password = [BitVec('b%d' % i, 40) for i in range(20)]
 # Return the first "M" models of formula list of formulas F 
 def get_models(s, M,password):
     result = []
@@ -36,7 +47,7 @@ def get_models(s, M,password):
     return p
 
 
-def verify(l,s,password):
+def verify(l,s):
     str_="firhfgferfibbqlkdfhh"
     for x in xrange(0,len(l)):
         rcx=l[x]
@@ -54,34 +65,16 @@ def verify(l,s,password):
         q=q_bar>>0x1f
         res=diff-((p-q) * 0x1a)   +0x61
         s.add(res==ord(str_[x]))
-
-verify(password,s,password)
-
-for x in xrange(0,20):
-    #s.add(password[x]>0x21)
-    s.add(password[x]<0xff)
-    pass
-
+        s.add(l[x]<0xff)
+
+s = Solver()
+str_="firhfgferfibbqlkdfhh"
+password = [BitVec('b%d' % i, 40) for i in range(20)]
+verify(password,s)
 #print str(s)
 #print f.sexpr()
 #print s.check()
 p=get_models(s, 10,password)
 #result=get_models(s, 10,password)
-
-
-import socket
-
-def netcat(hostname, port, content):
-    s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
-    s.connect((hostname, port))
-    s.sendall(content)
-    s.shutdown(socket.SHUT_WR)
-    while 1:
-        data = s.recv(1024)
-        if data == "":
-            break
-        print "Received:", repr(data)
-    print "Connection closed."
-    s.close()
 print p
 netcat("defcon.org.in",8083,p)
diff --git a/Keygen-2.py b/Keygen-2.py
@@ -0,0 +1,87 @@
+import string
+import random
+from z3 import *
+
+s = Solver()
+str_="firhfgferfibbqlkdfhh"
+password = [BitVec('b%d' % i, 40) for i in range(20)]
+# Return the first "M" models of formula list of formulas F 
+def get_models(s, M,password):
+    result = []
+    #s = Solver()
+    #s.add(F)
+    p=[]
+    while len(result) < M and s.check() == sat:
+        m = s.model()
+        k=''.join(hex(m[i].as_long()) for i in password if m[i] is not None)
+        q = k.replace("0x", "")
+        print q
+        p.append(q+"\n")
+
+        result.append(m)
+        # Create a new constraint the blocks the current model
+        block = []
+        for d in m:
+            # d is a declaration
+            if d.arity() > 0:
+                raise Z3Exception("uninterpreted functions are not supported")
+            # create a constant from declaration
+            c = d()
+            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
+                raise Z3Exception("arrays and uninterpreted sorts are not supported")
+            block.append(c != m[d])
+        s.add(Or(block))
+    #return result
+    p=''.join(p)
+    return p
+
+
+def verify(l,s,password):
+    str_="firhfgferfibbqlkdfhh"
+    for x in xrange(0,len(l)):
+        rcx=l[x]
+        #print l[x],"-0x54 = ",hex(rcx-0x54)
+        diff=rcx-0x54
+        #s.add(diff==0x5)
+        p_bar=((diff * 0x4ec4ec4f)/0xffffffff)
+        #p_bar=((diff * 79)/255)
+        #s.add(p_bar==9)
+        q_bar=diff
+        #s.add(Or(p_bar<=20))
+        #print "(",diff," * 0x4ec4ec4f)/0xffffffff)",p_bar
+        #print "(",diff," * 79)/255)",p_bar
+        p=p_bar>>0x3
+        q=q_bar>>0x1f
+        res=diff-((p-q) * 0x1a)   +0x61
+        s.add(res==ord(str_[x]))
+
+verify(password,s,password)
+
+for x in xrange(0,20):
+    #s.add(password[x]>0x21)
+    s.add(password[x]<0xff)
+    pass
+
+#print str(s)
+#print f.sexpr()
+#print s.check()
+p=get_models(s, 10,password)
+#result=get_models(s, 10,password)
+
+
+import socket
+
+def netcat(hostname, port, content):
+    s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+    s.connect((hostname, port))
+    s.sendall(content)
+    s.shutdown(socket.SHUT_WR)
+    while 1:
+        data = s.recv(1024)
+        if data == "":
+            break
+        print "Received:", repr(data)
+    print "Connection closed."
+    s.close()
+print p
+netcat("defcon.org.in",8083,p)
No results found