SHARE
TWEET

Untitled

a guest Feb 20th, 2019 66 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. from z3 import *
  2.  
  3. s = Solver()
  4. char1 = BitVec('char1', 8)
  5. char2 = BitVec('char2', 8)
  6. char3 = BitVec('char3', 8)
  7. char4 = BitVec('char4', 8)
  8. char5 = BitVec('char5', 8)
  9. char6 = BitVec('char6', 8)
  10. char7 = BitVec('char7', 8)
  11. char8 = BitVec('char8', 8)
  12. char9 = BitVec('char9', 8)
  13. char10 = BitVec('char10', 8)
  14. char11 = BitVec('char11', 8)
  15. char12 = BitVec('char12', 8)
  16. char13 = BitVec('char13', 8)
  17. char14 = BitVec('char14', 8)
  18. char15 = BitVec('char15', 8)
  19. char16 = BitVec('char16', 8)
  20. char = [char1, char2, char3, char4, char5, char6, char7, char8, char9, char10, char11, char12, char13, char14, char15, char16]
  21. s.add(char1 >= 32, char1 <= 127)
  22. s.add(char2 >= 32, char2 <= 127)
  23. s.add(char3 >= 32, char3 <= 127)
  24. s.add(char4 >= 32, char4 <= 127)
  25. s.add(char5 >= 32, char5 <= 127)
  26. s.add(char6 >= 32, char6 <= 127)
  27. s.add(char7 >= 32, char7 <= 127)
  28. s.add(char8 >= 32, char8 <= 127)
  29. s.add(char9 >= 32, char9 <= 127)
  30. s.add(char10 >= 32, char10 <= 127)
  31. s.add(char11 >= 32, char11 <= 127)
  32. s.add(char12 >= 32, char12 <= 127)
  33. s.add(char13 >= 32, char13 <= 127)
  34. s.add(char14 >= 32, char14 <= 127)
  35. s.add(char15 >= 32, char15 <= 127)
  36. s.add(char16 >= 32, char16 <= 127)
  37. s.add(((char1 * 10) + (char2 * 12) + (char7 * 62) + (char4 * 15) + (char11 * 95) + (char10 << 1) + (char14 * 38) + (char13 * 17) + (char16 * 25) + (char15 * 67)) == 0x8120)
  38. s.add(((char3 * 15) + (char1 << 3) + (char8 * 50) + (char6 * 25) + (char13 << 6) + (char9 * 13) + (char14 * 85)) == 0x6002)
  39. s.add(((char1 * 58) + (char6 * 55) + (char3 * 25) + (char10 * 12) + (char15 * 86) + (char14 * 57)) == 0x7C2D)
  40. s.add(((char1 * 67) + (char4 * 71) + (char8 * 97) + (char6 * 39) + (char12 * 10) + (char11 * 60)) == 0x6D22)
  41. s.add(((char1 * 85) + (char3 * 5) + (char5 * 25) + (char4 * 38) + (char12 << 4) + (char11 * 83) + (char14 * 53) + (char13 * 29)) == 0x7550)
  42. s.add(((char2 * 28) + (char9 * 3) + (char5 * 65) + (char11 * 81) + (char10 * 6) + (char15 * 78) + (char13 * 62)) == 0x85F9)
  43. s.add(((char2 * 51) + (char3 * 66) + (char7 * 80) + (char4 * 63) + (char14 * 93) + (char10 * 23)) == 0x842C)
  44. s.add(((char4 * 19) + (char6 * 94) + (char8 * 90) + (char7 * 30) + (char11 * 89) + (char10 * 9) + (char15 * 26) + (char12 << 3) + (char16 * 10)) == 0x7C9E)
  45. s.add(((char1 * 72) + (char3 * 7) + (char5 * 59) + (char4 * 65) + (char7 * 22) + (char6 * 50) + (char15 * 68) + (char9 * 74) + (char16 * 41)) == 0x8E1C)
  46. s.add(((char13 * 13) + (char1 * 13) + (char6 * 11) + (char9 * 50) + (char8 * 84) + (char12 * 52) + (char11 * 57) + (char15 * 60)) == 0x7733)
  47. s.add(((char1 * 31) + (char3 * 93) + (char7 * 56) + (char5 * 57) + (char13 * 96) + (char10 * 37) + (char15 * 97)) == 0xB050)
  48. s.add(((char1 * 18) + (char3 * 17) + (char5 * 12) + (char4 * 58) + (char7 * 14) + (char6 * 71) + (char12 * 46) + (char11 << 2) + (char10 << 3)) == 0x5A4C)
  49. s.add(((char1 * 75) + (char4 * 62) + (char8 * 85) + (char12 * 44) + (char10 * 59) + (char15 * 12)) == 0x924E)
  50. # s.add(((char5 * 36) + (char12 * 86)) == 0x1D7C)
  51. # s.add(((char4 * 55) + (char7 * 36) + (char6 * 79) + (char9 * 94) + (char8 * 88) + (char11 * 34) + (char10 * 20) + (char12 * 65) + (char14 * 19)) == 0xC1F0)
  52. # s.add(((char2 * 56) + (char3 * 36) + (char6 * 19) + (char5 << 3) + (char9 * 57) + (char8 * 71) + (char14 * 6) + (char12 * 99)) == 0x60A0)
  53. if str(s.check()) == 'sat':
  54.     input = ''.join(chr(int(str(s.model()[i]))) for i in char)
  55.     count = 1
  56.     for i in input:
  57.         print 'char' + str(count) + ' = ' + (hex(ord(i)))
  58.         count += 1
  59.     print input
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top