diff --git a/writeups/symbolic/kuudos/flag b/writeups/symbolic/kuudos/flag new file mode 100644 index 0000000..569c4cd --- /dev/null +++ b/writeups/symbolic/kuudos/flag @@ -0,0 +1 @@ +flag{FLAG_HERE_EHEH} \ No newline at end of file diff --git a/writeups/symbolic/kuudos/kuudos.py b/writeups/symbolic/kuudos/kuudos.py new file mode 100644 index 0000000..0f89cc9 --- /dev/null +++ b/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") \ No newline at end of file diff --git a/writeups/symbolic/kuudos/script.py b/writeups/symbolic/kuudos/script.py new file mode 100644 index 0000000..fe7d4fa --- /dev/null +++ b/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)