kuudos

writeups/symbolic/kuudos/flag

@@ -0,0 +1 @@
+flag{FLAG_HERE_EHEH}

writeups/symbolic/kuudos/kuudos.py

@@ -0,0 +1,75 @@
+n = 5
+
+def repeated_entry(vector):
+    set_ = set()
+    for i in range(len(vector)):
+        set_.add(vector[i])
+    if len(set_) == len(vector):
+        return 0
+    else:
+        return 1
+
+def activation_check(serial_code):
+    entries = serial_code.split("-")
+    if len(entries) != n:
+        return 2
+
+    matrix = [[0]*n for _ in range(n)]
+
+    for i in range(n):
+        if len(entries[i]) != n:
+            return 2
+        for j in range(n):
+            if entries[i][j] < '1' or entries[i][j] > str(n):
+                return 2
+            matrix[i][j] = entries[i][j]
+
+    for i in range(n):
+        vector = [matrix[i][j] for j in range(n)]
+        if repeated_entry(vector):
+            return 0
+
+    for j in range(n):
+        vector = [matrix[i][j] for i in range(n)]
+        if repeated_entry(vector):
+            return 0
+
+    vector = [matrix[i][i] for i in range(n)]
+    if repeated_entry(vector):
+        return 0
+
+    vector = [matrix[i][n-1-i] for i in range(n)]
+    if repeated_entry(vector):
+        return 0
+
+    sum__ =  0
+    for i in range(n):
+        for j in range(n):
+            sum__ += int(matrix[i][j])
+
+    if not (sum__ % 96 == 75):
+        return 0
+
+    return 1
+
+if __name__ == '__main__':
+    print("""██╗  ██╗██╗   ██╗██╗   ██╗██████╗  ██████╗ ███████╗
+██║ ██╔╝██║   ██║██║   ██║██╔══██╗██╔═══██╗██╔════╝
+█████╔╝ ██║   ██║██║   ██║██║  ██║██║   ██║███████╗
+██╔═██╗ ██║   ██║██║   ██║██║  ██║██║   ██║╚════██║
+██║  ██╗╚██████╔╝╚██████╔╝██████╔╝╚██████╔╝███████║
+╚═╝  ╚═╝ ╚═════╝  ╚═════╝ ╚═════╝  ╚═════╝ ╚══════╝
+                                                   
+    """)
+    serial_code = input("Input your activation code: ")
+
+    result = activation_check(serial_code)
+    print()
+    if result > 1:
+        print("Your serial has an incorrect format, look at the back of your CD.\n")
+    elif result:
+        with open("flag", "r") as f:
+            flag = f.read()
+            print(flag)
+    else:
+        print("Stop trying, buy the license :)\n")

writeups/symbolic/kuudos/script.py

@@ -0,0 +1,51 @@
+from z3 import *
+import time
+
+n = 5
+
+## Return Must Be 1: key like this xyzwk-xyzwk-xyzwk-xyzwk-xyzwk
+
+s = Solver()
+
+key = [[Int("key_%d_%d" % (i,j)) for i in range(n)] for j in range(n)]
+
+# Only numbers in [1, 5]
+for i in range(n):
+    for j in range(n):
+        s.add(key[i][j] >= 1, key[i][j] <= 5)
+
+# No reapeted on each column
+for j in range(n):
+    distinct = [key[i][j] for i in range(n)]
+    s.add(Distinct(distinct))
+
+# No repeated on each row
+for i in range(n):
+    distinct = [key[i][j] for j in range(n)]
+    s.add(Distinct(distinct))
+
+# No repeated on diagonal
+s.add(Distinct([key[i][i] for i in range(n)]))
+
+# No repeated on the other diagonal
+s.add(Distinct([key[i][n-i-1] for i in range(n)]))
+
+# Sum % 96 == 75
+_sum = 0
+for i in range(n):
+    for j in range(n):
+        _sum += key[i][j]
+s.add(_sum % 96 == 75)
+
+print(s.check())
+m = s.model()
+# print(m)
+
+key_str = ''
+for i in range(n):
+    for j in range(n):
+        key_str += "" + m[key[i][j]].as_string()
+    if(i != n-1):    
+        key_str += '-'
+
+print('Key:', key_str)