Skip to content

Instantly share code, notes, and snippets.

@Nicholaz99

Nicholaz99/jrappy-solver.py

Created September 30, 2019 08:52
Show Gist options
  • Save Nicholaz99/0e55e45393c3144d7d09eb82b1c3ba92 to your computer and use it in GitHub Desktop.
Save Nicholaz99/0e55e45393c3144d7d09eb82b1c3ba92 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
jrappy-solver.py
from z3 import *
# buf = [
# '\xa9', '\x91', '\xd7', '\xce', 'i', 'l', 'e', 'E', 's', '*', 'k', 'r', '\x7f', 'X', 'C', 'e', 'r', 'G', 'X', 'I', 'i', 'o', 'O', 'p', 'Y', 'd', 'e', 'C', 'y', 'X', 'x', 'r', 'W', '_', 'm', '\\', '{', 'e', 'l', 'f', 'V', 'e', 'm', 'v', 'i', 'Z', 'l', 'r', 'G', 'X', 'V', 'z', 'e', '`', 'g', 'o', 'K', 'e', 'b', 'l', 'c', 'i', 'm', 'K', 'c', 'l', '|', 'r', 'O', 'P', 'a', 'O', 'm', 'X', 'S', 'h', 'r', 'Z', 'R', 'f', 'z', 'o', '-', 'z', 'i', 'N', 'e', '3', 'y', 'X', 'x', 'r', "'", 'P', 'm', ',', '`', 'e', 'X', 'f', '$', '}', 'm', 'q', 'i', '%', 'm', 'r', '9', 'R', 'a', 'P', 'e', '\x13', 'j', 'o', '>', 'b', 'X', '+', 'b', 'o', 'k', 'L', '\x00', '\x02', '\x0c', '\x06', 'M', 'Y', 'a', 'q', 'M', 'q', ';', 'n', 'r', 'a', '\x1b', '\t', '\x07', '\n', 'l', 'p', 'f', ' ', '\x0c', '\x1c', '\x16', '\x16', '\x14', '\x1f', '\x07', '=', '\x1f', ';', '\x13', '\x07', '4', '\x03', 'b', 'o', '`', '#', '\x1d', '\x1e', '\x0c', '\x1c', '\x14', '\x1b', '\x0e', '\x1f', '\x15', '9', '\x1f', '\n', 's', 'e', 'M', 'N', '/', '\x05', '\x0c', '\x06', '\x08', 'C', '\t', '\x13', '\x1d', '?', 'N', '!', '\x11', '*', '\x04', '\x01', '\x15', '^', 'q', '/', 'b', 'o', '`', '#', '\x1d', '\r', '\x06', '\x19', '>', '9', '\x11', '&', '\x04', ':', '\x01', '\n', 'u', 'e', '\x16', 'a', 'c', ' ', 'l', 'p', 'm', '\x01', '\x04', '\x1b', '\x1d', 'Y', 'a', 'd', 'M', '\x03', '!', '\x05', '\x13', '\x13', '9', 'I', '\x0f', '\x0e', '\x03', '\x17', 'F', '?', '\x11', '\x00', '\x1a', '6', '\x06', 'I', 'L', '\x0e', 'l', 'o', '\x7f', ' ', '6', '\x05', '\x11', '\x16', '\x1d', '\x04', '\x04', '\t', '\x11', '\x1a', '\x1c', '<', '`', 'r', '}', 'p', '!', '\x05', '\x13', '\x13', '9', 'I', '\x0f', '\x0e', '\x03', '\x17', 'F', '?', '\x11', '\x00', '\x1a', '6', '\x06', 'I', '>', '\x03', '$', 'F', '$', 'd', 'X', 'a', '\x06', '\x01', '\x0e', '\x02', '\x10', '\x1c', '\x11', 's', 's', 'T', 'I', ')', '>', '\x11', '6', '4', ';', '>', '\x03', '/', 'J', '9', 'l', 'p', 'f', '*', '\x10', '\x1c', '\x10', ',', '\x08', '\x1d', '\x0b', '\x1d', '\x03', '\x0c', '\x00', '\x1c', '(', '\x12', 'b', 'o', 'J', 'X', '%', '\x06', '\x04', '\x04', '\x12', 'w', '\r', '\x13', '\x0b', '?', 'B', '<', '\x06', '\x17', '1', '\x08', '\x04', 'T', '!', '\x1a', '\x08', '\x1a', '\x04', ']', '\x1f', '9', '\x0f', '\x15', 'J', '\x0b', '\x19', '\x1d', '\x1b', '\x0b', '?', ']', 'J', '&', 'l', 'p', 'c', '?', '\n', '\x07', '\x01', ';', '\x04', '4', '\x0c', '4', '\x08', 'n', 'r', 'w', '\x1d', '\x08', '\x00', '\x1d', '\x14', '\x00', '\x1d', '\t', '\x01', '4', '\x1a', '4', '\x04', '\\', '\x0f', '9', '\x1b', '\x0e', '~', 'e', 'C', 'f', '\x7f', 'c', 'm', ' ', 'i', '=', 'i', 'r', '!', 'X', '2', 's', 'e', 'Q', '*', '6', '0', '+', '\t', '-', '6', '=', '=', '|', 'i', 'F', 'e', 'Y', 'r', 'X', 'p', '\x18', '\x04', '.', '\x0c', '@', '\x07', '\x11', '1', '\n', 'L', '<', '\x0e', '\x11', '\x07', '\x02', '\x00', '\x00', 't', 'X', '5', '~', 'e', '\r', 'm', '9', '~', 'e', 'C', 'f', '4', 'c', 'm', '(', 'i', '5', 'd', 'r', 'a', '\x1d', '\x0f', '\x06', '\x00', '*', 'M', '\x1b', '\x1a', '\x00', 'x', '\x15', '\x17', '\x1d', '\x04', '\x1e', '\x0e', 'V', 'E', 'u', 's', '\x02', 'm', 'r', '>', 'X', '1', 'c', 'r', '8', 'X', '8', 'o', 'o', 'r', 'p', 'I', 'm', 'e', 'f', '*', '=', '\x12', 'S', '\x1c', '7', '\x18', 'O', '\x13', '\x17', '=', 'F', '\x11', '\x06', '\n', '\x18', '\x1d', 'L', '_', '[', 'r', 'X', 'b', '<', '\n', 'y', 'l', 'o', 'q', '>', '\x03', '/', 'o', 'o', 'K', 'p', 'N', '`', 'e', '-', 's', '\x06', 'm', 'r', 'M', 'X', 'D', 'n', 'r', 'e', 'Y', 'f', 's', '-', '\x02', '\x1f', '\x1d', '\x1f', '\x11', '\x00', '\x12', '(', ',', '\x17', '\x11', '0', '\x02', '\x0b', '\x01', 'j', '^', 'f', '\x03', 'g', 'm', '\x11', 'e', 'l', '\x07', 'r', '\x10', 'P', 'a', '\x16', 'i', 'X', '\x0f', 'o', '\x17', 'd', 'X', 's', ';', '7', ';', '=', ' ', '"', '7', '*', '#', '\x02', ' ', '%', '0', '\x13', '#', '&', '9', '1', '\n', '-', '7', 'c', 'm', '\x16', 'i', '\x0b', 'd', 'r', '~', '\x1d', '\x0f', '\x11', '\x17', '!', '\x1d', '\x1b', '\x17', '\x01', '\x1e', '\x0f', '\x0f', '\n', 'l', 'p', 'y', '\x06', '\x04', '\x04', '\x12', 'w', '\r', '\x13', '\x0b', '?', 'B', ' ', '\x10', '\x0f', '=', '\x05', '\x17', 'n', 'm', '`', '\x03', '\r', '\x13', '\x13', '\\', '4', '\x00', '\x1c', '\x02', 'w', '>', '\x1b', '\x00', '\x0c', '6', '\x01', 'b', 'o', 'o', '+', ' ', 'm', 'e', 't', '\x1f', '=', '\x0f', '\x15', '\x11', '0', 'l', 'o', 'q', 'M', 'q', '/', 'b', 'o', 'k', '\x13', '\x01', '\r', '\x17', '3', '\x07', 'Y', 'a', 'v', 'M', '\x11', 'D', ',', 's', 'e', 'H', '\x0c', '\x02', '\x19', '\x0c', '_', '\x05', '\r', '\x0b', '\x15', '\\', '\x0b', '\x18', '\x01', '\x11', '=', '\x00', 'n', 'r', 'g', '1', '\x08', 'b', 'o', 'x', '<', '\x03', '\r', '\x13', '\x13', '\\', '1', '\x0e', ']', ',', '6', '\x1d', '\x1a', '\x06', '6', ',', '\x14', '\x06', '\x0e', '\x00', 'K', 'h', 'l', '}', 'Z', '?', '2', '\x00', '\x04', '\x04', 'w', '\x04', '\x00', ']', ',', '6', '\x16', '\x16', '\x1b', '>', '\x04', '\x1b', '\t', '\x04', '\x1f', 'H', 'q', '7', 's', 'e', '[', '\x02', '\x1a', '\x06', 'd', 'X', 's', '/', '\x05', '\x0c', '\x06', '\x08', 'C', '\x0c', '\x1d', '\\', '\x08', '\x13', '\x1b', '\x0b', ',', '>', '\x1b', '\x00', '\x00', '9', '\x0b', 'X', 'n', 'm', 'c', '\x03', '\r', '\x13', '\x13', '\\', '1', '\x0e', ']', '5', '*', '\x04', '\x01', '\x06', '6', ',', '\x14', '\x06', '\x0e', '\x00', 'q', 'i', 'k', '\x15', '\x00', '\x1a', '6', '\x15', '\x1e', '\x0b', 'Y', 'm', 'z', 'Z', ')', '2', '\x07', '\x15', '\x0e', 'B', '\x1c', '\x08', '\x02', '\x02', ']', ' ', ',', '\x13', '\x1b', '\x0b', '?', 'V', 'F', '$', 'd', 'X', 'n', '\r', '\n', '\x15', '\x04', '%', '\x05', '\x0b', '\x17', 'r', 'X', 'u', 'Z', 'L', '\x14', '\x07', '\x0e', '\x04', '\x04', 'w', '\n', '\x02', '\x01', '\n', '_', ':', '\x18', '\x17', '\x1b', '\x1d', '?', 'Z', 's', 'e', 'S', '\x19', '\x00', "'", '\x15', '(', '\x03', '\x11', ',', '\x0c', '\x03', '\x0c', 'f', 'e', '\x1a', 's', '1', '`', 'r', 'g', 'Y', 'l', 'n', 'r', 'r', '5', '\x07', '\x08', '\n', '.', '\x1f', '\x07', '\x0f', '\x04', '\x06', '$', '1', '\x15', '\x1a', '&', '7', '\x03', '\x1c', '\x06', '\x04', '6', '\x12', '\x10', 'n', 'm', 'W', 'A', ' ', '\x0f', '\x13', '\x05', '9', 'N', '\x1e', '\x04', '6', '\n', '@', '!', '\x11', '*', '\x0f', '\r', '\x08', 'V', '3', '@', ' ', '\x0f', '\x13', '\x05', '9', 'N', '\x1e', '\x04', '6', '\n', '@', '!', '\x11', '*', '\x0f', '\r', '\x08', 'V', 'q', 'i', 'k', 'd', 's', 'r', 'Y', '`', 's', 'd', 'Y', 'm', '\xfd', 'Z', ')', '2', '\x07', '\x15', '\x0e', 'B', '\x1c', '\x08', '\x02', '\x02', ']', ' ', ',', '\x13', '\x1b', '\x0b', '?', 'V', '#', '\x18', '\x04', '.', '\x07', 'L', '\x03', '\x0c', '\x1e', '\x0e', 'C', '6', '\x06', '\x01', '1', '\x0f', '\x15', '^', '\x14', '\x07', '\x0e', '\x04', '\x04', 'w', '\n', '\x02', '\x01', '\n', '_', ':', '\x18', '\x17', '\x1b', '\x1d', '?', 'Z', '>', '\x0f', '9', '\x1b', '\x0e', ']', '\t', '9', '\x08', '\x04', '@', '>', '\x04', '\x1b', '\x05', '\x0b', '\x15', 'H', '\x14', '\x0b', '\x13', '\x13', '9', 'B', '\x03', '\x13', '\x0b', '?', 'I', '0', '\x1b', '\x1f', '\x19', '\x07', '\x0b', '^', '>', '\x19', '9', '\x17', '\x13', 'J', '4', '\x0c', '\x01', '\x15', 'J', '\x0b', '\x12', '\x11', '\x06', '\x03', '\x17', 'R', ' ', '\x0f', '\x13', '\x05', '9', 'N', '\x1e', '\x04', '6', '\n', '@', '!', '\x11', '*', '\x0f', '\r', '\x08', 'V', 'Y', '%', '\x06', '\x04', '\x04', '\x12', 'w', '\r', '\x13', '\x0b', '?', 'B', '<', '\x06', '\x17', '1', '\x08', '\x04', 'T', 'l', 'p', 'o', '\t', '\x14', '\x07', '\x12', '4', '\x12', 's', 'e', 'M', 'E', '#', '\x18', '\x04', '.', '\x07', 'L', '\x03', '\x0c', '\x1e', '\x0e', 'C', '*', '\x10', '\x19', '=', '\x02', '\x06', '^', 'q', '7', 'h', 'r', '\x0f', 'T', 'f', '\x01', 'o', '\x03', 'q', 'i', 'H', '\x0f', '\x13', '\x05', '9', 'N', '\x1e', '\x04', '6', '\n', '@', '\x1b', '\x0b', '.', '\t', '\x08', '\n', 'B', '#', '\x1d', '\x1e', '\x0c', '\x1c', '\x14', '\x1b', '\x0e', '\x1c', '\x06', '9', '\x19', ')', '\x13', '\x06', ',', '\t', '\x11', '\x16', 'j', 'p', '\x19', 'm', 'e', 't', '?', '7', '\x0e', '\x19', '\x10', '(', 'l', 'o', '~', ',', '6', '\x08', '\x06', '\x1d', '.', '\x1c', '\x08', '\x1f', '\x16', '\x17', '\x00', 'Y', 'a', '\xea', 'M', '\x14', '\x07', '\x0e', '\x04', '\x04', 'w', '\n', '\x02', '\x01', '\n', '_', '\x00', '\x02', '\x13', '\x1d', '\x18', '=', 'N', '?', '\x00', ',', '\x05', '\x00', '\x16', '-', '9', '\x08', '\x07', '\x03', '\x08', '\x03', 'M', ' ', '\n', '\x1d', '\x18', '-', '\x11', 'I', ')', '2', '\x0c', '\x19', '\x13', 'J', '4', '\x07', '\r', '\x08', 'B', '#', '\x1d', '\x1e', '\x0c', '\x1c', '\x14', 'c', '-', '\x18', '\x04', '.', '\x0c', '@', '\x1e', '\x04', '6', '\x01', 'L', '\x06', '\x03', '\x06', '\x06', '\x07', '\x00', ']', '>', '=', '\x15', '\x1a', '\n', '<', '9', '\x16', '\x02', '\x00', 'c', '*', '\t', '\x0e', '\x1b', '\x11', 'F', '\x00', '\x04', '\x1c', '\x14', 'w', '2', '\x06', '\x17', '1', '\x03', '\x08', 'I', '>', '\x14', '\x0c', '\x02', '\x19', '\x0c', '_', '\x05', '\r', '\x0b', '\x15', '\\', '\x17', '\x03', '\x18', '\x00', ';', '\x19', 'T', '[', ')', '2', '\x07', '\x15', '\x0e', 'B', '\x1c', '\x08', '\x02', '\x02', ']', '\x1a', '6', '\x17', '\x1d', '\x0e', '=', 'B', ',', '\x13', '\t', '4', '5', '\n', '\x1b', '\x08', 'K', 'n', 'l', '\x14', 's', 's', '}', '\x0b', '\x13', '\x13', '9', 'B', '\x03', '\x13', '\x0b', '?', 'I', '\n', '\x01', '\x1b', '\x1f', '\x02', '\t', 'J', '?', '\x16', ',', '\t', '\x1d', '\x01', '\x10', '\x0c', '\x01', '\x16', '\t', '=', '\x15', 'G', '#', '\x02', '\x1f', '\x02', '\x19', '\x15', 's', 's', 'F', '\x0b', '\x13', '\x13', '9', 'B', '\x03', '\x13', '\x0b', '?', 'I', '\n', '\x01', '\x1b', '\x1f', '\x02', '\t', 'J', '?', '\x16', ',', '\t', '\x1d', '\x01', '\x10', '\x0c', '\x01', '\x16', '\t', '=', '\x15', 'c', 'N', 'm', 'i', 'i', 'v', 'e', 'r', 's', 'X', 'a', 't', 'e', 'Y', 'm', 't', 'r', 'y', 'X', 'g', 'c', 'r', 'm', 'p', 'i', 'q', 'e', 's', 's', 'Y', 'a', 'r', 'e', ']', 'G', '\xd8', 'r', 'd', '\xe9', 'f', 'c', 'o', 'l', 'p', 'w', 'l', 'e', 'r', 'u', 'X', '`', 'r', 'e', 'X', 'o', 'o', '{', 'e', 'G', 'f', 'C', 'o', 'l', 'p', 't', 'l', 'e', 'p', '\x18', 'X', 'd', 'r', 'l', 'X', 'm', 'n', '\xf2', 'O', '\xee', 'f', 'a', 'S', 'G', '=', 'r', '|', 'p', '\xed', 's', ']', 'e', '\xde', 'u', 'M', '\xd1', 'e', '+', 'f', '[', ')', ':', 'k', 'n', '?', '0', 'i', 'a', '=', '*', '^', 'b', '=', '<', '_', 'n', ' ', '+', 'm', '[', ')', ':', '\x7f', 'k', 's', '&', '5', 'u', 'u', 'w', '\x17', '8', 'b', 'm', '[', '"', '6', 'b', 'l', '[', ')', ':', '\x7f', 'g', 's', '&', '5', 'u', 'y', 'p', '\x17', '8', 'b', 'i', '[', '"', '6', 'b', 'h', '[', ')', ':', '\x7f', 'c', 's', '&', '5', 'u', '}', 'p', '\x17', '8', 'b', 'u', '[', '"', '6', 'b', 't', '[', ')', ':', '\x7f', '\x7f', 's', '&', '5', 'u', 'a', 'p', '\x17', '8', 'b', 'q', '\\', '"', '!', 'b', 'k', '\xe4', 'l', ':', 'l', '}', 'm', '&', '5', 'a', 'b', 'e', '\x17', '8', 'w', 'u', 'K', '"', '6', 't', 'u', '_', ')', ':', 'h', 'e', '?', '0', 'd', 'u', '\x9d', '<', '\x01', 'q', 't', 'u', 'Q', '"', '6', 'b', 'b', 'H', 'i', ',', '6', '}', 'x', 'j', '#', '<', 'b', 'z', 'H', '\x9f', '=', '<', 'H', 'g', '\x7f', '\x84', '*', '\x01', 'v', 'h', 'g', '"', ')', 'y', '`', 'u', 'h', '<', '\x01', 'q', '\x7f', 'u', 'C', '"', 'U', 'v', 'f', 'n', 'c', 'f', 'Y', 'k', 'e', 'o', 'w', '\xc7', 'r', '!', 'A', 'e', 'g', '`', 'v', 'A', 'z', 't', '`', '<', '\xd0', 'c', 'l', 'A', 'e', 'o', '\xda', 'e', 'q', '\x17', '\xc7', 'a', 'u', 'a', '\xff', 'm', 'k', 'q', '|', '\\', 's', 'f', 'k', '\r', '^', 'E', 'y', 'c', 'v', '\x17', '\xee', 'a', 'q', 'I', 'M', 'k', '\xd9', 'r', 'f', '<', '\xf9', 'c', 'h', 'i', '\xd7', 'i', 'h', 'f', '\x0c', '\xea', 'X', 'd', 'u', '\xc9', 'M', 'h', 'j', '\x12', 'S', ']', 's', 'e', 'i', '\r', 'F', 'o', '\xcb', '\x9a', '\xdc', 'a', '\\', '[', 't', 'I', 'A', 'k', '\xd7', 'r', '`', 'n', 'a', 'v', 'h', 'i', '\xef', 'i', 'j', 'u', 'y', '\xdf', '[', 'W', 'z', 'p', 'P', 'v', '\xcd', 'r', '%', 't', 's', 'k', '\xd9', 'm', 's', 'y', '\r', '\xc4', 'r', 't', '\\', '\xc6', 'r', 'a', '[', 'A', 'z', 'z', '\xd3', 'X', 'e', 's', '\x15', '\xce', 'p', 'n', 'h', '\xc2', 'r', 'w', '[', '\x1f', '\xeb', 'e', 'T', '@', 'z', 'z', 'K', '\xc1', 'f', 'l', 'k', '\xc1', ']', '|', 'd', 'K', 'v', '\xec', 'X', 'd', 'v', '\xc9', '\xdc', 'e', 'n', '\xd5', '\x9a', '\x98', 'e', '\xcf', 'o', 'm', 'p', 'k', 'l', '{', 'r', 's', 'X', '\x03', 'r', '}', 'X', 'm', 'o', 'w', 'e', ']', 'f', 'e', 'o', 'j', 'p', '`', 'l', 'h', 'r', 'y', 'X', 'n', 'r', 'i', 'X', '\x1a', 'o', '\x7f', 'e', '\x90', 'f', 'm', 'o', '\xa6', 'p', 'y', 'l', '\xb1', 'r', 'b', 'Y', 's', 'r', 'w', 'Y', 'y', 'o', 'a', 'd', 'B', 'f', 's', 'n', 'N', 'p', '\x7f', 'm', 'B', 'r', 'd', 'Y', 'N', 'r', '}', 'Y', 'X', 'o', 'k', 'd', '`', 'f', 'x', 'n', ',', 'p', 'u', 'm', '\x00', 'r', 'n', 'Y', '\r', 'r', '{', 'Y', '\x03', 'o', 'S', 'd', '.', 'f', 'A', 'n', '\x15', 'p', 'r', 'm', '\x1b', 'r', 'V', 'X', '@', 'r', 'e', 'X', '\x1c', 'o', 'c', '\x98', 'X', 'i', 'b', 'h', 'm', 'R', '\x96', 'l', '\xdb', 'r', 't', '_', 'a', 'P', 'd', '_', 'm', 'M', 'u', 'e', '{', 'a', 'c', 'L', 'l', 'q', 'i', 'l', 'E', '2', 'r', '\x04', '`', '\x8d', 'e', 'X', 'm', 'h', 'u', 'e', 'z', 'g', 'd', 'o', 'O', 'w', 'i', 'O', 'b', 'r', 'P', 'Y', '`', 'r', 'g', 'Y', 'l', 'j', '\x88', 'e', 'V', '\x9b', 'c', '{', 'j', 'p', 'K', 'm', '\x99', 'r', 'q', 'Y', 'u', '2', 'd', '\x16', 'l', '\x90', 'r', 'e', 'X', 'o', 'd', 'o', 'O', 'q', 'n', 'l', 'G', 'u', 's', '{', 'f', 'r', 'F', 'Y', 'j', 'o', 'P', 'd', 'Y', 'f', 'a', 'n', 'l', '|', '`', '\x96', 'e', 'w', 's', 'Q', 'a', 'V', 'e', '}', 'm', 'n', 'r', 'x', 'X', 'f', 'c', '\x1a', 'm', 's', 'i', 'o', 'e', 'r', 's', 'k', '\xda', 'r', 'c', '\x01', '\xdf', 'o', 'u', '\xd2', 'X', 'n', '.', '\xdd', 'm', 'y', '{', 'f', '\xd3', 'r', 'x', 't', '\xd7', 'r', 'i', '\x14', 'F', '\xd7', 'r', 'h', '\xc2', 'f', 'm', '\xdd', 'm', 'y', '{', 'b', '\xd3', 'r', 'x', '\xff', 'a', 'y', '\xd7', 'X', 'd', '}', '}', '\xd3', 'X', 'm', '\xd2', 'o', 'm', 'p', 'k', 'l', '{', 'r', 's', 'X', '\x7f', 'r', 'b', 'X', 'm', 'o', 'Y', 'e', 'S', 'f', 'N', 'o', '~', 'p', 'G', 'l', '}', 'r', 'C', 'X', '~', 'r', 'T', 'X', 'G', 'o', 'G', 'e', 'j', 'f', 'T', 'o', 'L', 'p', 'i', 'l', 'i', 'r', 'q', '\xa5', 'a', 'X', 'b', 'X', 'O', 'h', 'r', 'c', '_', 'f', 'k', 'o', 'K', 'p', 'N', 'l', 'd', 'r', 'n', 'X', 'a', 'r', '\x1e', 'X', 'i', 'o', 'w', 'e', 'X', 'f', 'S', 'l', 'P', 's', 'W', 'q', 'c', '\xd0', 's', 'q', 'b', 'D', 'a', 'M', 'i', 'i', '\xd0', 'e', 'B', 'M', '~', ']', 'x', 't', 'C', 'p', '\xd3', 'r', 'p', 'H', ' ', '\x02', '*', '\xdc', 'o', 'n', '\xf6', 'a', 'Y', '\xc1', '\x9c', '\x89', '\xe9', 's', 'h', '\xcb', '\x9a', '\xaa', '\xc2', 'X', 'a', 'r', 'g', 'X', 's', 'o', 'r', 'e', 'z', 'f', 'k', 'o', 'm', 'p', 'U', 'l', 'g', 'r', 'M', 'X', 'h', 'r', '%', 'X', '\x7f', 'o', '0', 'e', 'x', 'f', ' ', 'o', 'N', 'p', ')', 'l', 'L', 'r', 'M', 'X', 'N', 'r', '#', 'X', 'L', 'o', 'r', 'e', 'I', 'f', 'g', '\x92', 'm', 't', 'h', 'm', '\x99', 'r', 't', 'Y', '\x9b', 'r', 'y', '\xa2', 'm', 'j', 'r', 'm', 'X', 'N', 'c', 'F', 'm', 'q', 'i', 'q', 'e', 'r', 's', '\x8b', 'a', 't', 'e', '^', 'm', 'o', 'r', '9', '[', 'P', 'g', 'z', 'i', 'v', '\xcb', 'l', '0', 'q', 'E', ']', 't', 'w', 'a', '\xfa', 'm', ')', 'X', 'p', '\\', 'T', 'v', 'j', 'n', '?', 'j', 'R', 'x', 't', '\xd1', 'X', 'A', 'X', 'p', '\\', '_', 'z', 'w', '9', 'v', 'M', 'v', 'k', '_', 'm', 'G', '@', 'x', '@', 'f', ']', 'O', '\x1a', '\x05', '\x17', '\xe9', 'l', 's', '\xc2', '\xa7', '\x87', 'I', 'z', 'i', 'B', '|', 'i', 'O', 'g', 'w', 'j', 't', 'w', 'K', 'H', 'v', '\x1f', '=', '\xe1', ']', 'g', '\xc4', '\x90', '\xd7', '\xf4', 'm', 'm', '\xc2', '\x8d', '\xd8', '\xe9', 'a', 'r', 'e', 'Z', 'm', 'q', 'r', 'e', 'X', 'L', 'c', 'e', 'm', 'p', 'i', '!', 'e', '{', 's', '\x17', 'a', '`', 'e', '\t', 'm', 'u', 'r', '6', 'X', 'G', 'c', ':', 'm', 'H', 'i', '?', 'e', 'L', 's', '\x00', 'a', '=', 'e', '\x17', 'm', ':', 'r', '(', 'X', '=', 'c', '4', 'm', 'Q', 'i', 'l', 'e', 'G', 's', '^', '\x9c', 'r', 'f', 'X', 'l', '\x93', 'r', 'm', 'Y', '\x99', 'c', '`', 'm', 'v', 'n', 'l', 'u', 'u', 's', 'H', 'f', 'r', 'u', 'Y', 'l', 'n', 'r', 'e', 'y', '\x99', 'c', 'y', 'm', 'v', 'n', 'l', 'u', 'u', 's', 'H', 'f', 'r', 'u', 'X', 'l', 'n', 'r', 'e', '\xa2', 'f', 'f', 'o', 'e', 'p', 'C', 'l', 'N', 'r', 'r', 'X', '|', 'r', 'e', ']', '~', 'o', 'u', 'e', 'C', 'f', 'c', 'm', '\x8d', 'v', 'o', '\xa9', 'e', 'b', 'q', '\x15', 'J', '^', '\xdd', 'X', '|', 'i', 'v', '\xa0', 'X', 'v', 'a', '!', 'k', 't', '\xac', 'l', 'u', 'p', 'I', '\\', 'g', 'v', '\xa0', 'X', '}', 'm', 'H', '`', '^', 'b', '\xa6', 'o', '}', 'r', 'S', 'j', 'c', 'v', '\xb6', 'X', 'q', 'p', '_', '_', 'k', 'k', '\xb7', 'e', 'H', 'd', 'Y', 'g', 'k', 't', '\xac', 'l', 'u', 'p', 'I', 'Q', 'K', '\xc4', 'e', 'J', 'W', 'e', 'q', 'S', 'S', 's', 'h', 'i', '\xcf', 'p', 'p', 'A', 'p', 'y', 'A', '[', 'x', 'x', 'p', 'S', '\xdb', 'o', 'q', 'u', '\x19', '\x16', ',', '\xeb', 'f', 'q', '\xce', '\x93', '\x82', 'q', 'E', 'S', 't', 'y', 'c', '\xfa', 'm', 's', 'k', 'a', 'M', 'm', 'Q', 'l', 't', 'z', '|', 'g', 'c', '\x12', '\xc5', 'X', 'b', 'b', '$', '(', '"', '\xeb', 'y', 'd', '\xff', '\x99', '\x87', 'l', '[', '{', '|', 'g', 'c', '\xd0', 's', 'E', 'x', 'w', 'p', 'S', '_', 'l', 'k', 'o', 'M', 'm', 's', 'i', '\r', '\xc6', 'i', 'o', 'u', '3', '\x03', '\x17', '\xe5', 'y', 'd', '\xff', '\x92', '\x8c', 'q', 'S', 'S', 's', 'h', 'i', '\xcf', 'p', 't', 'u', 'c', 'g', 'x', 'j', 'b', 'k', 'o', 'M', 'f', '\x7f', '{', '\x05', '\xee', 'f', '`', '\x7f', ',', '\x00', '&', '\xe8', 'n', 's', '\xd4', '\xa7', '\x82', 'q', 'S', 'S', 'x', 'd', 't', '\xc7', 'X', '{', 'z', 'h', 'x', '{', '[', 'o', '|', 'x', 'f', 'S', 'q', '~', '\x05', '\xee', 'm', 'l', 'b', '$', '(', ')', '\xe7', 'd', 'l', '\xd7', '\x96', '\x8f', 'f', 'D', 'x', 'M', 'j', 't', '\xc7', 'X', 'p', 'v', 'z', 'p', 'S', 'T', '`', 'v', 'g', 'e', 'b', '|', 'j', '\x12', '\xc5', 'X', 'b', 'b', '$', '(', '"', '\xeb', 'y', 'd', '\xff', '\x99', '\x80', 'l', '[', '{', '|', 'g', 'c', '\xd0', 's', 'E', 'x', '{', 'p', 'S', '_', 'l', 'k', 'o', 'M', 'm', 's', '}', '\r', '\xc6', 'i', 'o', 'u', '3', '\x03', '\x17', '\xe5', 'y', 'd', '\xff', '\x92', '\x8c', 't', 'a', '\x9d', 'f', 's', 'm', 'W', '{', 'o', 'h', '\xa0', 'r', 'c', 'Z', '[', '~', 'c', '\\', '\xa8', 'o', 'b', 'g', 'b', 'k', 'e', 'k', '\xa8', 'p', 'y', 'n', '_', '|', 'u', '\\', '\xa4', 'r', 'u', 'Z', 'W', '`', 't', 'a', '\x9d', 'f', 's', 'm', 'W', '`', 'o', 'h', '\xa0', 'r', 'c', 'Z', '[', 'c', '|', 'S', 'A', 'B', '\xca', 'e', 'K', '\x7f', 'o', 'C', 't', 't', '\xd1', 'l', 'v', 'k', '~', 't', 'x', 'w', '\xdd', 'X', '~', 'v', '|', 'I', 'A', '`', '\xdb', 'o', '~', 'i', 'f', '@', '|', 'u', '\xcb', 'X', 'r', 'k', 'u', 't', 't', 'g', '\xca', 'e', 'K', '\x7f', 'r', 'C', 't', 'y', '\xd1', 'l', 'v', '`', 'g', 'b', 's', '`', 'q', 'b', '~', '}', 'f', '_', 'L', 't', 'w', 'U', 'x', 'b', '}', 'V', 's', '`', 'g', 'b', 'v', '`', 'q', 'b', 'u', 'l', 'D', '|', 'M', '\x7f', 'e', '\xcd', 'm', 'm', 'p', '~', '|', 'y', 'f', 'A', 'S', 'q', 'K', 'H', ',', '\x0f', '\xe0', '\xdf', 'X', 's', 'c', 'o', 'W', 'b', '\xed', 'u', 'd', '\xd5', '\x8c', '\xbb', 'b', 'D', '|', 'M', 't', 'i', '\xd0', 'e', 'E', '\x7f', 'p', 'v', 'a', 'e', 'p', '^', 'f', '\\', 'c', '\x19', '\x01', '\xe0', '\xdf', 'X', 'x', 'o', 'r', '_', 'K', '\xe2', 'z', 'n', '\xca', '\x8f', '\x8a', 'o', 'S', 'k', 'f', 'A', 'g', '\xd0', 'e', 'E', 't', '{', 'k', 'h', 'M', '\x7f', 'Q', 'l', 'C', '`', '(', '\x0c', '\xf7', '\xc8', 's', 'M', 'a', 'r', '_', 'L', '\xe9', 'v', 's', '\xc2', '\xa7', '\x85', '`', 'Y', 't', 'e', 'p', 'j', '\xc7', 'r', 'n', 'A', 't', 'k', 'k', 'M', 't', ']', 'q', 'K', 'H', "'", '\x03', '\xfd', '\xd7', 'p', '|', 'l', 'e', 'H', 'f', '\xdc', 'x', 's', '\xc2', '\xa7', '\x8e', 'l', 'D', '|', 'M', '\x7f', 'e', '\xcd', 'm', 'm', 'p', 'z', '|', '}', 'f', 'A', 'S', 'q', 'K', 'H', ',', '\x0f', '\xe0', '\xdf', 'X', 's', 'c', 'o', 'W', 'f', '\xed', 'u', 'd', '\xd5', '\x8c', '\xbb', 'b', 'D', '|', 'M', 't', 'i', '\xd0', 'e', 'E', '\x7f', 't', 'v', '}', 'e', 'p', '^', 'f', '\\', 'c', '\x19', '\x01', '\xe0', '\xdf', 'X', 'x', 'o', 'r', '_', 'O', '\xe2', 'z', 'n', '\xca', '\x8f', '\x8a', 'o', 'S', 'k', 'f', 'A', 'g', '\xd0', 'e', 'E', 't', 'w', 'k', 't', 'M', '\x7f', 'Q', 'l', 'C', '`', '(', '\x0c', '\xf7', '\xc8', 's', 'M', 'a', 'r', '_', '@', '\xe9', 'v', 's', '\xc2', '\xa7', '\x85', 'z', '}', 't', 'c', 'p', 'x', '|', 'g', 'j', 'N', 'x', 'e', '|', '@', '\xd7', 'o', 'd', 'e', 'X', '\\', 'z', '}', 'z', 'J', 's', 'u', '|', 'k', 'i', '\xee', 'a', 'j', '\xfc', 'X', 'h', 'k', '\xde', 'b', '\xf4', 'f', 'c', 'o', 'o', 'p', 'w', 'l', 'e', 's', 'I', 'X', '/', 'r', 'e', 'X', '2', 'o', 'u', 'e', '8', 'f', 'o', 'o', '\x0f', 'p', 'z', 'l', '\x06', 'r', 'h', 'X', '\x05', 'r', 'F', 'X', '\x08', 'o', 'Y', 'e', '>', 'f', 'P', 'o', '\n', 'p', 'R', 'l', '\r', 'r', '0', 'X', '\x0b', 'r', ',', 'X', '\x01', 'o', ' ', 'e', '5', 'f', '\x01', 'o', '\x01', 'p', '\x01', 'l', '\x0b', 'r', '\x02', 'X', '\x0e', 'r', '\xe1', 'X', '\x03', 'o', '\xf8', 'e', '(', 'f', '\xf0', 'o', '\x1c', 'p', '\xce', 'l', '\x15', 'r', '\xde', 'X', '\x13', 'r', '\xd3', 'X', '\x1e', 'o', '\xb8', 'e', '*', 'f', '\xb3', 'o', '\x19', 'p', '\xb0', 'l', '\x10', 'r', '\x9e', 'X', '\x15', 'r', '\x96', 'X', '\x1b', 'o', '\x8e', 'e', '/', 'g', 's', 'o', '\x1b', 'q', '\x7f', 'l', '\x1d', 's', 'l', 'X', '\x18', 's', 'V', 'X', '\x15', 'n', 'K', 'e', '#', 'g', '"', 'o', '\x11', 'q', ' ', 'l', '\x18', 's', '"', 'X', '\x1f', 's', '<', 'X', '\x12', 'n', '\x13', 'e', '\xd8', 'g', '\n', 'o', '\xec', 'q', '\x18', 'l', '\xe0', 's', '\x0b', 'X', '\xe7', 's', '\xe5', 'X', '\xea', 'n', '\xfa', 'e', '\xd0', 'g', '\xf3', 'o', '\xe4', 'q', '\xf1', 'l', '\xef', 's', '\xd3', 'X', '\xea', 's', '\xcd', 'X', '\xe2', 'n', '\xde', 'e', '\xc8', 'g', '\xd3', 'o', '\xfc', 'q', '\xdd', 'l', '\xf7', 's', '\xcb', 'X', '\xf2', 's', '\xd9', 'X', '\xf9', 'n', '\xb2', 'e', '\xcd', 'g', '\xa7', 'o', '\xf5', 'q', '\xa4', 'l', '\xfc', 's', '\x92', 'X', '\xf9', 's', '\x82', 'X', '\xf7', 'n', '\x82', 'e', '\xc3', 'd', 'g', 'o', '\xf7', 'r', 'c', 'l', '\xf9', 'p', '`', 'X', '\xfc', 'p', 'B', 'X', '\xf1', 'm', '_', 'e', '\xc6', 'd', 'U', 'o', '\xf2', 'r', '#', 'l', '\xfb', 'p', '#', 'X', '\xc1', 'p', '<', 'X', '\xcc', 'm', '\x1f', 'e', '\xf8', 'd', '\x10', 'o', '\xcf', 'r', '\x15', 'l', '\xc6', 'p', '\xe3', 'X', '\xc3', 'p', '\xf3', 'X', '\xc9', 'm', '\xed', 'e', '\xfd', 'd', '\xd0', 'o', '\xc9', 'r', '\xd0', 'l', '\xc2', 'p', '\xbd', 'X', '\xc9', 'p', '\xb7', 'X', '\xc4', 'm', '\xae', 'e', '\xf2', 'd', '\xbd', 'o', '\xc1', 'p', 'H', 'l', 'e', 'r', '\x92', 'X', '|', '\x8d', 'e', '\x14', 'm', 'c', 'u', 'e', 'z', 'a', 'c', 'M', 'j', 'p', 'y', 'k', 'e', 'b', 't', 'X', 'q', 'u', 'e', 'H', 'j', 'o', 'b', 'b', 'X', 'v', 'd', 'o', '}', 'w', 'i', '|', 'b', 'r', 'Q', 'Y', 'a', 'r', '\x9f', 'X', 'v', '\x93', 'r', 'g', 'Y', '\x9c', 'c', 'q', '\x91', 'p', 'k', 'm', '\x9f', 'r', 'l', '\xa4', 'a', 'p', 'd', '\xa2', 'm', 'p', '\x8e', 'e', 'Z', 'g', '\x99', 'o', 'r', '\x8c', 'i', 'n', 'd', '\x88', 's', 'G', '\x9d', 'r', 'g', 'Y', '\x97', 'o', 'm', '\x9a', 'X', '\xeb', 'c', 'u', 'j', 'p', 'K', 'k', 'e', 'P', 't', 'X', 'q', 'u', 'e', 'H', 'j', 'o', 'b', 'b', 'X', 'v', 'd', 'o', '}', 'w', 'i', '|', 'b', 'r', 'c', '_', 'a', 'b', 'b', 'X', 'O', 'h', 'r', 'u', '_', 'f', 's', 'h', 'm', '`', 'n', 'l', 'u', 'u', 's', 'H', 'f', 'r', 'u', '_', 'm', '\x7f', 'u', 'e', 'z', 'a', 'c', 'M', 'j', 'p', 'K', 'k', 'e', 'P', 't', 'X', 'C', 'u', 'e', 'z', 'j', 'o', 'P', 'd', 'X', 'f', '\x99', 'o', 'r', '\x8c', 'i', 'n', 'd', '\x88', 's', 'G', '\x9d', 'r', 'g', 'Y', '\x97', 'o', 'm', '\x99', 'X', 'd', 'b', '\x95', 'm', 'o', '\x95', 'l', 'g', 's', '\x89', 'X', '~', '\x8e', 'e', 'Z', 'l', '\x95', 'r', 'z', '\xa4', 'f', 'a', 'n', '\x97', 'p', 'v', '\x91', 'e', 'V', 't', 'X', 'C', 'u', 'e', 'z', 'm', 'l', 'r', 'I', 'X', 'f', 'c', 'm', 'm', ']', 'i', '\x01', 'e', 'r', 's', 'R', 'a', 's', 'e', '3', 'm', '\x00', 'r', '\t', 'X', '\x7f', 'c', '+', 'm', 'p', 'i', 'b', 'e', 'p', 's', '\x1d', 'a', 's', 'e', '\x1e', 'm', '*', 'r', 'd', 'X', '.']
def dump(buf2, s):
global buf
while buf:
for i in range(0, len(s)):
c = ord(s[i])
buf2 += chr(ord(buf[0]) ^ ord(s[i]))
if len(buf) == 1:
buf = ''
else:
buf = buf[1:]
open('dump', 'wb').write(buf2)
def firstKey():
s = Solver()
arr = []
arr.append(BitVec('s1', 32))
arr.append(BitVec('s2', 32))
arr.append(BitVec('s3', 32))
arr.append(BitVec('s4', 32))
arr.append(BitVec('s5', 32))
arr.append(BitVec('s6', 32))
arr.append(BitVec('s7', 32))
arr.append(BitVec('s8', 32))
arr.append(BitVec('s9', 32))
arr.append(BitVec('s10', 32))
arr.append(BitVec('s11', 32))
arr.append(BitVec('s12', 32))
arr.append(BitVec('s13', 32))
arr.append(BitVec('s14', 32))
arr.append(BitVec('s15', 32))
arr.append(BitVec('s16', 32))
arr.append(BitVec('s17', 32))
arr.append(BitVec('s18', 32))
arr.append(BitVec('s19', 32))
arr.append(BitVec('s20', 32))
ca = [196, 225, 210, 200, 214, 219, 215, 215, 203, 190]
cx = [2, 29, 8, 40, 4, 3, 23, 23, 43, 62]
caa = [210, 221, 213, 215, 203, 211, 189, 220, 215, 190]
caps = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0]
for i in range(20 / 2):
s.add(And(arr[i] + arr[(i + 10)] == ca[i], arr[i] ^ arr[(i + 10)] == cx[i]))
for i in range(0, 20, 2):
s.add(arr[i] + arr[i+1] == caa[(i/2)])
for i in range(20):
if (caps[i] == 0):
s.add(And(arr[i] >= 97, arr[i] <= 122))
else:
s.add(Or(arr[i] < 97, arr[i] > 122))
s.add(arr[7] ^ arr[8] == 1)
s.check()
keys = []
while s.check() == sat:
model = s.model()
key = ""
for i in range(20):
key += chr(model[arr[i]].as_long())
keys.append(key)
s.add(Or(arr[0] != model[arr[0]], arr[1] != model[arr[1]], arr[2] != model[arr[2]], arr[3] != model[arr[3]], arr[4] != model[arr[4]], arr[5] != model[arr[5]], arr[6] != model[arr[6]], arr[7] != model[arr[7]], arr[8] != model[arr[8]], arr[9] != model[arr[9]], arr[10] != model[arr[10]], arr[11] != model[arr[11]], arr[12] != model[arr[12]], arr[13] != model[arr[13]], arr[14] != model[arr[14]], arr[15] != model[arr[15]], arr[16] != model[arr[16]], arr[17] != model[arr[17]], arr[18] != model[arr[18]], arr[19] != model[arr[19]]))
return keys[2]
def encryptMethod(s2, arr):
index = 0
for i in range(3):
for j in range(3):
arr[i][j] = ord(s2[index]) % ord('A')
index += 1
def encrypt(array, array2, array3):
for i in range(3):
for j in range(1):
array[i][j] = 0
for k in range(3):
array4 = array[i]
n = j
array4[n] += (array2[i][k] * array3[k][j])
array[i][j] %= 27
def secondKey():
sol = Solver()
arr = []
arr.append(BitVec('s1', 32))
arr.append(BitVec('s2', 32))
arr.append(BitVec('s3', 32))
arr.append(BitVec('s4', 32))
arr.append(BitVec('s5', 32))
arr.append(BitVec('s6', 32))
arr.append(BitVec('s7', 32))
arr.append(BitVec('s8', 32))
arr.append(BitVec('s9', 32))
arr.append(BitVec('s10', 32))
arr.append(BitVec('s11', 32))
arr.append(BitVec('s12', 32))
arr.append(BitVec('s13', 32))
arr.append(BitVec('s14', 32))
arr.append(BitVec('s15', 32))
arr.append(BitVec('s16', 32))
arr.append(BitVec('s17', 32))
arr.append(BitVec('s18', 32))
arr.append(BitVec('s19', 32))
arr.append(BitVec('s20', 32))
arr.append(BitVec('s21', 32))
for i in range(21):
sol.add(arr[i] <= 255)
length = 21
array = [ 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1 ]
array2 = [ 29, 22, 19, 7, 5, -17, 9, 15, 0, -2, -10, 5, 26, 27 ]
n = 0
for i in range(2, length, 3):
sol.add(And(array2[n] == arr[i-2] - arr[i], array2[n+1] == arr[i-1] - arr[i]))
n += 2
arrayz = [[0 for j in range(3)] for i in range(3)]
arrayz = [[6, 24, 1], [13, 16, 10], [20, 17, 15]]
array2z = [[0 for j in range(1)] for i in range(3)]
array3 = [[0 for j in range(1)] for i in range(3)]
array4 = [[0 for j in range(1)] for i in range(3)]
array5 = [[0 for j in range(1)] for i in range(3)]
array6 = [[0 for j in range(1)] for i in range(3)]
array7 = [[0 for j in range(1)] for i in range(3)]
array8 = [[0 for j in range(1)] for i in range(3)]
array9 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array2z[i][0] = arr[i] % ord('A')
encrypt(array9, arrayz, array2z)
array9b = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = (arr[0] - 32) % ord('A')
array2z[1][0] = arr[1] % ord('A')
array2z[2][0] = arr[2] % ord('A')
encrypt(array9b, arrayz, array2z)
array9c = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = (arr[0] - 32) % ord('A')
array2z[1][0] = (arr[1] - 32) % ord('A')
array2z[2][0] = arr[2] % ord('A')
encrypt(array9c, arrayz, array2z)
array9d = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = (arr[0] - 32) % ord('A')
array2z[1][0] = (arr[1] - 32) % ord('A')
array2z[2][0] = (arr[2] - 32) % ord('A')
encrypt(array9d, arrayz, array2z)
array9e = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = arr[0] % ord('A')
array2z[1][0] = (arr[1] - 32) % ord('A')
array2z[2][0] = arr[2] % ord('A')
encrypt(array9e, arrayz, array2z)
array9f = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = arr[0] % ord('A')
array2z[1][0] = (arr[1] - 32) % ord('A')
array2z[2][0] = (arr[2] - 32) % ord('A')
encrypt(array9f, arrayz, array2z)
array9g = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = arr[0] % ord('A')
array2z[1][0] = arr[1] % ord('A')
array2z[2][0] = (arr[2] - 32) % ord('A')
encrypt(array9g, arrayz, array2z)
array9h = [[0 for j in range(1)] for i in range(3)]
array2z[0][0] = (arr[0] - 32) % ord('A')
array2z[1][0] = arr[1] % ord('A')
array2z[2][0] = (arr[2] - 32) % ord('A')
encrypt(array9h, arrayz, array2z)
sol.add(Or(And(array9[0][0] == 23, array9[1][0] == 23, array9[2][0] == 21), And(array9b[0][0] == 23, array9b[1][0] == 23, array9b[2][0] == 21), And(array9c[0][0] == 23, array9c[1][0] == 23, array9c[2][0] == 21), And(array9d[0][0] == 23, array9d[1][0] == 23, array9d[2][0] == 21), And(array9e[0][0] == 23, array9e[1][0] == 23, array9e[2][0] == 21), And(array9f[0][0] == 23, array9f[1][0] == 23, array9f[2][0] == 21), And(array9g[0][0] == 23, array9g[1][0] == 23, array9g[2][0] == 21), And(array9h[0][0] == 23, array9h[1][0] == 23, array9h[2][0] == 21)))
array10 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array3[i][0] = arr[i] % ord('A')
encrypt(array10, arrayz, array3)
array10b = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = (arr[0 + 3] - 32) % ord('A')
array3[1][0] = arr[1 + 3] % ord('A')
array3[2][0] = arr[2 + 3] % ord('A')
encrypt(array10b, arrayz, array3)
array10c = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = (arr[0 + 3] - 32) % ord('A')
array3[1][0] = (arr[1 + 3] - 32) % ord('A')
array3[2][0] = arr[2 + 3] % ord('A')
encrypt(array10c, arrayz, array3)
array10d = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = (arr[0 + 3] - 32) % ord('A')
array3[1][0] = (arr[1 + 3] - 32) % ord('A')
array3[2][0] = (arr[2 + 3] - 32) % ord('A')
encrypt(array10d, arrayz, array3)
array10e = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = arr[0 + 3] % ord('A')
array3[1][0] = (arr[1 + 3] - 32) % ord('A')
array3[2][0] = arr[2 + 3] % ord('A')
encrypt(array10e, arrayz, array3)
array10f = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = arr[0 + 3] % ord('A')
array3[1][0] = (arr[1 + 3] - 32) % ord('A')
array3[2][0] = (arr[2 + 3] - 32) % ord('A')
encrypt(array10f, arrayz, array3)
array10g = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = arr[0 + 3] % ord('A')
array3[1][0] = arr[1 + 3] % ord('A')
array3[2][0] = (arr[2 + 3] - 32) % ord('A')
encrypt(array10g, arrayz, array3)
array10h = [[0 for j in range(1)] for i in range(3)]
array3[0][0] = (arr[0 + 3] - 32) % ord('A')
array3[1][0] = arr[1 + 3] % ord('A')
array3[2][0] = (arr[2 + 3] - 32) % ord('A')
encrypt(array10h, arrayz, array3)
sol.add(Or(And(array10[0][0] == 12, array10[1][0] == 8, array10[2][0] == 13), And(array10b[0][0] == 12, array10b[1][0] == 8, array10b[2][0] == 13), And(array10c[0][0] == 12, array10c[1][0] == 8, array10c[2][0] == 13), And(array10d[0][0] == 12, array10d[1][0] == 8, array10d[2][0] == 13), And(array10e[0][0] == 12, array10e[1][0] == 8, array10e[2][0] == 13), And(array10f[0][0] == 12, array10f[1][0] == 8, array10f[2][0] == 13), And(array10g[0][0] == 12, array10g[1][0] == 8, array10g[2][0] == 13), And(array10h[0][0] == 12, array10h[1][0] == 8, array10h[2][0] == 13)))
array11 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array4[i][0] = arr[i + 6] % ord('A')
encrypt(array11, arrayz, array4)
array11b = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = (arr[0 + 6] - 32) % ord('A')
array4[1][0] = arr[1 + 6] % ord('A')
array4[2][0] = arr[2 + 6] % ord('A')
encrypt(array11b, arrayz, array4)
array11c = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = (arr[0 + 6] - 32) % ord('A')
array4[1][0] = (arr[1 + 6] - 32)% ord('A')
array4[2][0] = arr[2 + 6] % ord('A')
encrypt(array11c, arrayz, array4)
array11d = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = (arr[0 + 6] - 32) % ord('A')
array4[1][0] = (arr[1 + 6] - 32)% ord('A')
array4[2][0] = (arr[2 + 6] - 32) % ord('A')
encrypt(array11d, arrayz, array4)
array11e = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = arr[0 + 6] % ord('A')
array4[1][0] = (arr[1 + 6] - 32)% ord('A')
array4[2][0] = arr[2 + 6] % ord('A')
encrypt(array11e, arrayz, array4)
array11f = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = arr[0 + 6] % ord('A')
array4[1][0] = (arr[1 + 6] - 32)% ord('A')
array4[2][0] = (arr[2 + 6] - 32) % ord('A')
encrypt(array11f, arrayz, array4)
array11g = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = arr[0 + 6] % ord('A')
array4[1][0] = arr[1 + 6] % ord('A')
array4[2][0] = (arr[2 + 6] - 32) % ord('A')
encrypt(array11g, arrayz, array4)
array11h = [[0 for j in range(1)] for i in range(3)]
array4[0][0] = (arr[0 + 6] - 32) % ord('A')
array4[1][0] = arr[1 + 6] % ord('A')
array4[2][0] = (arr[2 + 6] - 32) % ord('A')
encrypt(array11h, arrayz, array4)
sol.add(Or(And(array11[0][0] == 17, array11[1][0] == 23, array11[2][0] == 15), And(array11b[0][0] == 17, array11b[1][0] == 23, array11b[2][0] == 15), And(array11c[0][0] == 17, array11c[1][0] == 23, array11c[2][0] == 15), And(array11d[0][0] == 17, array11d[1][0] == 23, array11d[2][0] == 15), And(array11e[0][0] == 17, array11e[1][0] == 23, array11e[2][0] == 15), And(array11f[0][0] == 17, array11f[1][0] == 23, array11f[2][0] == 15), And(array11g[0][0] == 17, array11g[1][0] == 23, array11g[2][0] == 15), And(array11h[0][0] == 17, array11h[1][0] == 23, array11h[2][0] == 15)))
array12 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array5[i][0] = arr[i + 9] % ord('A')
encrypt(array12, arrayz, array5)
array12b = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = (arr[0 + 9] - 32) % ord('A')
array5[1][0] = arr[1 + 9] % ord('A')
array5[2][0] = arr[2 + 9] % ord('A')
encrypt(array12b, arrayz, array5)
array12c = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = (arr[0 + 9] - 32) % ord('A')
array5[1][0] = (arr[1 + 9] - 32)% ord('A')
array5[2][0] = arr[2 + 9] % ord('A')
encrypt(array12c, arrayz, array5)
array12d = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = (arr[0 + 9] - 32) % ord('A')
array5[1][0] = (arr[1 + 9] - 32)% ord('A')
array5[2][0] = (arr[2 + 9] - 32) % ord('A')
encrypt(array12d, arrayz, array5)
array12e = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = arr[0 + 9] % ord('A')
array5[1][0] = (arr[1 + 9] - 32)% ord('A')
array5[2][0] = arr[2 + 9] % ord('A')
encrypt(array12e, arrayz, array5)
array12f = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = arr[0 + 9] % ord('A')
array5[1][0] = (arr[1 + 9] - 32)% ord('A')
array5[2][0] = (arr[2 + 9] - 32) % ord('A')
encrypt(array12f, arrayz, array5)
array12g = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = arr[0 + 9] % ord('A')
array5[1][0] = arr[1 + 9] % ord('A')
array5[2][0] = (arr[2 + 9] - 32) % ord('A')
encrypt(array12g, arrayz, array5)
array12h = [[0 for j in range(1)] for i in range(3)]
array5[0][0] = (arr[0 + 9] - 32) % ord('A')
array5[1][0] = arr[1 + 9] % ord('A')
array5[2][0] = (arr[2 + 9] - 32) % ord('A')
encrypt(array12h, arrayz, array5)
sol.add(Or(And(array12[0][0] == 25, array12[1][0] == 0, array12[2][0] == 22), And(array12b[0][0] == 25, array12b[1][0] == 0, array12b[2][0] == 22), And(array12c[0][0] == 25, array12c[1][0] == 0, array12c[2][0] == 22), And(array12d[0][0] == 25, array12d[1][0] == 0, array12d[2][0] == 22), And(array12e[0][0] == 25, array12e[1][0] == 0, array12e[2][0] == 22), And(array12f[0][0] == 25, array12f[1][0] == 0, array12f[2][0] == 22), And(array12g[0][0] == 25, array12g[1][0] == 0, array12g[2][0] == 22), And(array12h[0][0] == 25, array12h[1][0] == 0, array12h[2][0] == 22)))
array13 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array6[i][0] = arr[i + 12] % ord('A')
encrypt(array13, arrayz, array6)
array13b = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = (arr[0 + 12] - 32) % ord('A')
array6[1][0] = arr[1 + 12] % ord('A')
array6[2][0] = arr[2 + 12] % ord('A')
encrypt(array13b, arrayz, array6)
array13c = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = (arr[0 + 12] - 32) % ord('A')
array6[1][0] = (arr[1 + 12] - 32)% ord('A')
array6[2][0] = arr[2 + 12] % ord('A')
encrypt(array13c, arrayz, array6)
array13d = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = (arr[0 + 12] - 32) % ord('A')
array6[1][0] = (arr[1 + 12] - 32)% ord('A')
array6[2][0] = (arr[2 + 12] - 32) % ord('A')
encrypt(array13d, arrayz, array6)
array13e = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = arr[0 + 12] % ord('A')
array6[1][0] = (arr[1 + 12] - 32)% ord('A')
array6[2][0] = arr[2 + 12] % ord('A')
encrypt(array13e, arrayz, array6)
array13f = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = arr[0 + 12] % ord('A')
array6[1][0] = (arr[1 + 12] - 32)% ord('A')
array6[2][0] = (arr[2 + 12] - 32) % ord('A')
encrypt(array13f, arrayz, array6)
array13g = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = arr[0 + 12] % ord('A')
array6[1][0] = arr[1 + 12] % ord('A')
array6[2][0] = (arr[2 + 12] - 32) % ord('A')
encrypt(array13g, arrayz, array6)
array13h = [[0 for j in range(1)] for i in range(3)]
array6[0][0] = (arr[0 + 12] - 32) % ord('A')
array6[1][0] = arr[1 + 12] % ord('A')
array6[2][0] = (arr[2 + 12] - 32) % ord('A')
encrypt(array13h, arrayz, array6)
sol.add(Or(And(array13[0][0] == 20, array13[1][0] == 10, array13[2][0] == 13), And(array13b[0][0] == 20, array13b[1][0] == 10, array13b[2][0] == 13), And(array13c[0][0] == 20, array13c[1][0] == 10, array13c[2][0] == 13), And(array13d[0][0] == 20, array13d[1][0] == 10, array13d[2][0] == 13), And(array13e[0][0] == 20, array13e[1][0] == 10, array13e[2][0] == 13), And(array13f[0][0] == 20, array13f[1][0] == 10, array13f[2][0] == 13), And(array13g[0][0] == 20, array13g[1][0] == 10, array13g[2][0] == 13), And(array13h[0][0] == 20, array13h[1][0] == 10, array13h[2][0] == 13)))
array14 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array7[i][0] = arr[i + 15] % ord('A')
encrypt(array14, arrayz, array7)
array14b = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = (arr[0 + 15] - 32) % ord('A')
array7[1][0] = arr[1 + 15] % ord('A')
array7[2][0] = arr[2 + 15] % ord('A')
encrypt(array14b, arrayz, array7)
array14c = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = (arr[0 + 15] - 32) % ord('A')
array7[1][0] = (arr[1 + 15] - 32)% ord('A')
array7[2][0] = arr[2 + 15] % ord('A')
encrypt(array14c, arrayz, array7)
array14d = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = (arr[0 + 15] - 32) % ord('A')
array7[1][0] = (arr[1 + 15] - 32)% ord('A')
array7[2][0] = (arr[2 + 15] - 32) % ord('A')
encrypt(array14d, arrayz, array7)
array14e = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = arr[0 + 15] % ord('A')
array7[1][0] = (arr[1 + 15] - 32)% ord('A')
array7[2][0] = arr[2 + 15] % ord('A')
encrypt(array14e, arrayz, array7)
array14f = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = arr[0 + 15] % ord('A')
array7[1][0] = (arr[1 + 15] - 32)% ord('A')
array7[2][0] = (arr[2 + 15] - 32) % ord('A')
encrypt(array14f, arrayz, array7)
array14g = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = arr[0 + 15] % ord('A')
array7[1][0] = arr[1 + 15] % ord('A')
array7[2][0] = (arr[2 + 15] - 32) % ord('A')
encrypt(array14g, arrayz, array7)
array14h = [[0 for j in range(1)] for i in range(3)]
array7[0][0] = (arr[0 + 15] - 32) % ord('A')
array7[1][0] = arr[1 + 15] % ord('A')
array7[2][0] = (arr[2 + 15] - 32) % ord('A')
encrypt(array14h, arrayz, array7)
sol.add(Or(And(array14[0][0] == 8, array14[1][0] == 10, array14[2][0] == 19), And(array14b[0][0] == 8, array14b[1][0] == 10, array14b[2][0] == 19), And(array14c[0][0] == 8, array14c[1][0] == 10, array14c[2][0] == 19), And(array14d[0][0] == 8, array14d[1][0] == 10, array14d[2][0] == 19), And(array14e[0][0] == 8, array14e[1][0] == 10, array14e[2][0] == 19), And(array14f[0][0] == 8, array14f[1][0] == 10, array14f[2][0] == 19), And(array14g[0][0] == 8, array14g[1][0] == 10, array14g[2][0] == 19), And(array14h[0][0] == 8, array14h[1][0] == 10, array14h[2][0] == 19)))
array15 = [[0 for j in range(1)] for i in range(3)]
for i in range(3):
array8[i][0] = arr[i + 18] % ord('A')
encrypt(array15, arrayz, array8)
array15b = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = (arr[0 + 18] - 32) % ord('A')
array8[1][0] = arr[1 + 18] % ord('A')
array8[2][0] = arr[2 + 18] % ord('A')
encrypt(array15b, arrayz, array8)
array15c = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = (arr[0 + 18] - 32) % ord('A')
array8[1][0] = (arr[1 + 18] - 32)% ord('A')
array8[2][0] = arr[2 + 18] % ord('A')
encrypt(array15c, arrayz, array8)
array15d = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = (arr[0 + 18] - 32) % ord('A')
array8[1][0] = (arr[1 + 18] - 32)% ord('A')
array8[2][0] = (arr[2 + 18] - 32) % ord('A')
encrypt(array15d, arrayz, array8)
array15e = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = arr[0 + 18] % ord('A')
array8[1][0] = (arr[1 + 18] - 32)% ord('A')
array8[2][0] = arr[2 + 18] % ord('A')
encrypt(array15e, arrayz, array8)
array15f = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = arr[0 + 18] % ord('A')
array8[1][0] = (arr[1 + 18] - 32)% ord('A')
array8[2][0] = (arr[2 + 18] - 32) % ord('A')
encrypt(array15f, arrayz, array8)
array15g = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = arr[0 + 18] % ord('A')
array8[1][0] = arr[1 + 18] % ord('A')
array8[2][0] = (arr[2 + 18] - 32) % ord('A')
encrypt(array15g, arrayz, array8)
array15h = [[0 for j in range(1)] for i in range(3)]
array8[0][0] = (arr[0 + 18] - 32) % ord('A')
array8[1][0] = arr[1 + 18] % ord('A')
array8[2][0] = (arr[2 + 18] - 32) % ord('A')
encrypt(array15h, arrayz, array8)
sol.add(Or(And(array15[0][0] == 17, array15[1][0] == 10, array15[2][0] == 19), And(array15b[0][0] == 17, array15b[1][0] == 10, array15b[2][0] == 19), And(array15c[0][0] == 17, array15c[1][0] == 10, array15c[2][0] == 19), And(array15d[0][0] == 17, array15d[1][0] == 10, array15d[2][0] == 19), And(array15e[0][0] == 17, array15e[1][0] == 10, array15e[2][0] == 19), And(array15f[0][0] == 17, array15f[1][0] == 10, array15f[2][0] == 19), And(array15g[0][0] == 17, array15g[1][0] == 10, array15g[2][0] == 19), And(array15h[0][0] == 17, array15h[1][0] == 10, array15h[2][0] == 19)))
for j in range(0, length):
if (array[j] == 0):
sol.add(And(arr[j] >= ord('a'), arr[j] <= ord('z')))
else:
sol.add(Or(arr[j] < ord('a'), arr[j] > ord('z')))
sol.check()
model = sol.model()
key = ""
for i in range(21):
key += chr(model[arr[i]].as_long())
return key
key_1 = firstKey()
key_2 = secondKey()
print key_1, key_2
key = key_1 + key_2
flag = "bsides_delhi{%s}" % key
print "[+] Flag:", flag
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment