rps-casino
problem
#!/usr/local/bin/python
import os
from Crypto.Util.number import bytes_to_long
def LFSR():
state = bytes_to_long(os.urandom(8))
while 1:
yield state & 0xf
for i in range(4):
bit = (state ^ (state >> 1) ^ (state >> 3) ^ (state >> 4)) & 1
state = (state >> 1) | (bit << 63)
rng = LFSR()
n = 56
print(f"Let's play rock-paper-scissors! We'll give you {n} free games, but after that you'll have to beat me 50 times in a row to win. Good luck!")
rps = ["rock", "paper", "scissors", "rock"]
nums = []
for i in range(n):
choice = next(rng) % 3
inp = input("Choose rock, paper, or scissors: ")
if inp not in rps:
print("Invalid choice")
exit(0)
if inp == rps[choice]:
print("Tie!")
elif rps.index(inp, 1) - 1 == choice:
print("You win!")
else:
print("You lose!")
for i in range(50):
choice = next(rng) % 3
inp = input("Choose rock, paper, or scissors: ")
if inp not in rps:
print("Invalid choice")
break
if rps.index(inp, 1) - 1 != choice:
print("Better luck next time!")
break
else:
print("You win!")
else:
print(open("flag.txt").read())
solution
this is an LFSR where each rock paper scissors game gives the information of what the last 4 bits mod 3 of the state of the lfsr is
after each game, the LFSR is shifted right by 4 every time, and each time it shifts the new left most bit is the xor of the 0th, 1st, 3rd, and 4th right most bits
i just put it into z3
i for some reason couldn’t use a bitvec idk why it just wasn’t working but the booleans seemed to work
from z3 import *
from pwn import *
# p = process(["python3", "rps-casino.py"])
p = remote("mc.ax", 31234)
p.recvline()
s = Solver()
state = [Bool(f"b{_}") for _ in range(424)]
for a in range(424-64):
s.add(state[a+64] == Xor(state[a], Xor(state[a+1], Xor(state[a+3], state[a+4]))))
print("xors added")
for i in range(56):
p.sendline(b'rock')
line = p.recvline()
mod3 = 0
lsb0 = state[i*4]
lsb1 = state[i*4+1]
lsb2 = state[i*4+2]
lsb3 = state[i*4+3]
if b'win' in line: # mod 3 == 2
mod3 = 2
is_two = And(lsb1, And(Not(lsb0), And(Not(lsb2), Not(lsb3))))
is_five = And(lsb0, And(lsb2, And(Not(lsb1), Not(lsb3))))
is_eight = And(lsb3, And(Not(lsb0), And(Not(lsb1), Not(lsb2))))
is_eleven = And(lsb1, And(lsb0, And(lsb3, Not(lsb2))))
is_fourteen = And(lsb1, And(lsb2, And(lsb3, Not(lsb0))))
s.add(Or(is_two, Or(is_five, Or(is_eight, Or(is_eleven, is_fourteen)))))
elif b'lose' in line: # mod 3 == 1
mod3 = 1
is_one = And(Not(lsb1), And(lsb0, And(Not(lsb2), Not(lsb3))))
is_four = And(lsb2, And(Not(lsb0), And(Not(lsb1), Not(lsb3))))
is_seven = And(lsb0, And(lsb1, And(lsb2, Not(lsb3))))
is_ten = And(lsb3, And(lsb1, And(Not(lsb0), Not(lsb2))))
is_thirteen = And(lsb3, And(lsb2, And(Not(lsb1), lsb0)))
s.add(Or(is_one, Or(is_four, Or(is_seven, Or(is_ten, is_thirteen)))))
elif b'Tie' in line: # mod 3 == 0
mod3 = 0
is_zero = And(And(Not(lsb0), Not(lsb1)), And(Not(lsb2), Not(lsb3)))
is_three = And(And(lsb0, lsb1), And(Not(lsb2), Not(lsb3)))
is_six = And(And(lsb1, lsb2), And(Not(lsb0), Not(lsb3)))
is_nine = And(And(lsb0, lsb3), And(Not(lsb1), Not(lsb2)))
is_twelve = And(And(lsb3, lsb2), And(Not(lsb1), Not(lsb0)))
is_fifteen = And(And(lsb0, lsb1), And(lsb2, lsb3))
s.add(Or(is_zero, Or(is_three, Or(is_six, Or(is_nine, Or(is_twelve, is_fifteen))))))
print(f"#{i}, mod 3 == {mod3}, {line}")
print(s.check())
total = ""
solved = s.model()
for i in range(424):
total = ("1" if str(s.model()[state[i]]) == "True" else "0") + total
print(total)
def LFSR():
state = int(total[-64:], 2)
while 1:
yield state & 0xf
for i in range(4):
bit = (state ^ (state >> 1) ^ (state >> 3) ^ (state >> 4)) & 1
state = (state >> 1) | (bit << 63)
rng = LFSR()
for _ in range(56):
selected = next(rng) % 3
print(["rock", "paper", "scissors"][(selected+1) % 3])
for _ in range(50):
selected = next(rng) % 3
choice = ["rock", "paper", "scissors"][(selected+1) % 3]
p.sendline(choice.encode('ascii'))
p.interactive()
also making the is_one
, is_two
was so boring