Guest User

Untitled

a guest
Jan 26th, 2020
147
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. from z3 import *
  2.  
  3. ALPHABET = "SDHACENOIFKXQLBMPJTZURWVGY"
  4.  
  5. KEY1_INDEXES = [ 3,  4, 28, 29,  6,  7,  8,  9, 10, 11, 12, 13, 14, 15,  5, 17, 18, 19, 20, 21, 22]
  6. KEY2_INDEXES = [ 3,  4,  1,  2, 29, 30, 15, 16, 31, 32, 33, 34, 35, 36, 28, 17, 18, 19, 20, 21, 22]
  7.  
  8. def encodeString(s):
  9.     result = s[0]
  10.     lastLetterIdx = ALPHABET.index(s[0])
  11.  
  12.     for i in range(len(s) - 1):
  13.         thisLetterIdx = ALPHABET.index(s[i + 1])
  14.         cypherNum = thisLetterIdx - lastLetterIdx - i
  15.         cypherNum += 284
  16.         modNum = cypherNum % 26
  17.         encChar = chr(modNum + 48)
  18.  
  19.         result += encChar
  20.  
  21.         lastLetterIdx = thisLetterIdx
  22.  
  23.     return result
  24.  
  25. def encodedStringToNumber(s):
  26.     number = 0
  27.     letterMulti = 1
  28.     for i in range(len(s), 0, -1):
  29.         if(i < len(s)):
  30.             letterMulti = letterMulti * 19
  31.  
  32.         letter = ord(s[i-1])
  33.         letter -= 48
  34.         letter *= letterMulti
  35.  
  36.         number += letter
  37.    
  38.     return number
  39.  
  40. def is_checksum_valid(s):
  41.     sum_val = sum([ord(c) for c in s[1:]])
  42.     mod_val = sum_val % 25
  43.     return ALPHABET[mod_val] == s[0]
  44.  
  45. def pad(val, pad_num):
  46.     return str(val).rjust(pad_num, '0')
  47.  
  48. def get_key1(s):
  49.     res = encodeString(s)
  50.     if not is_checksum_valid(res):
  51.         raise Exception("Invalid checksum for key {}".format(s))
  52.     p1 = pad(encodedStringToNumber(res[1:13]), 15)
  53.     p2 = pad(encodedStringToNumber(res[13:]), 15)
  54.     return p1 + p2
  55.  
  56. def get_key2(s):
  57.     res = encodeString(s)
  58.     if not is_checksum_valid(res):
  59.         raise Exception("Invalid checksum for key {}".format(s))
  60.     p1 = pad(encodedStringToNumber(res[1:12]), 14)
  61.     p2 = pad(encodedStringToNumber(res[12:23]), 14)
  62.     p3 = pad(encodedStringToNumber(res[23:]), 7)
  63.     return p1 + p2 + p3
  64.  
  65. def extract_indexes_from_key(k, indexes):
  66.     res = ""
  67.     for index in indexes:
  68.         res += k[index - 1]
  69.     return res
  70.  
  71. def is_valid(key1, key2):
  72.     a = extract_indexes_from_key(key1, KEY1_INDEXES)
  73.     b = extract_indexes_from_key(key2, KEY2_INDEXES)
  74.     if a != b:
  75.         return False
  76.     if key2[5:8] != "999":
  77.         return False
  78.     return True
  79.  
  80. if __name__ == "__main__":
  81.     initial1 = "ALVMGRCTQQEYMNAHDANKPGKPO"
  82.     res = encodeString(initial1)
  83.     assert(res == "A87>4A26;@8833898:::;<?8B")
  84.     assert(is_checksum_valid(res) == True)
  85.     p1 = pad(encodedStringToNumber(res[1:13]), 15)
  86.     assert(p1 == "979440403325666")
  87.     p2 = pad(encodedStringToNumber(res[13:]), 15)
  88.     assert(p2 == "401568800000018")
  89.     key1 = p1 + p2
  90.     assert(key1 == "979440403325666401568800000018")
  91.     assert(key1 == get_key1(initial1))
  92.     assert(extract_indexes_from_key(key1, KEY1_INDEXES) == "940104033256664015688")
  93.  
  94.     initial2 = "VABCDEFGHIJKLMNOPQRSTUVWXYZABK"
  95.     res = encodeString(initial2)
  96.     assert(res == "V48<BHG7EFH7@>2;B4@;G661@>C88B")
  97.     assert(is_checksum_valid(res) == True)
  98.     p1 = pad(encodedStringToNumber(res[1:12]), 14)
  99.     assert(p1 == "27326846177342")
  100.     p2 = pad(encodedStringToNumber(res[12:23]), 14)
  101.     assert(p2 == "102659346508195")
  102.     p3 = pad(encodedStringToNumber(res[23:]), 7)
  103.     assert(p3 == "88621338")
  104.     key2 = p1 + p2 + p3
  105.     assert(key2 == "2732684617734210265934650819588621338")
  106.     assert(key2 == get_key2(initial2))
  107.     assert(extract_indexes_from_key(key2, KEY2_INDEXES) == "322758108621339265934")
  108.  
  109.  
  110.     INPUT_LEN = 30
  111.     user_input = [BitVec("{}".format(i), 8) for i in range(INPUT_LEN)]
  112.     solver = Solver()
  113.     for i in range(INPUT_LEN):
  114.         solver.add(user_input[i] >= ord('0'))
  115.         solver.add(user_input[i] <= ord('~'))
  116.     solver.add(is_valid(get_key1(initial1), get_key2(user_input)) == True)
  117.  
  118.     if solver.check() == sat:
  119.         res = ""
  120.         m = solver.model()
  121.         print(m)
RAW Paste Data