I think that’s the “You simply model the PRNG in Z3” part.
Whether that’s simple depends is debatable, but for example would be if somebody open-sourced the server-side of their poker dealing site.
Whether that’s simple depends is debatable, but for example would be if somebody open-sourced the server-side of their poker dealing site.
I doubt any poker site uses anything other than a crypto rand for deals because the technique I just explained would eat them alive. They can use fast and insecure PRNG for doing Monte Carlo hand evaluation, though, since that doesn't give you any advantage.
Since getting a truly random shuffle would take too long, this is a poor method of getting random results. Would it be possible to, at least to some degree, predict the order of the cards using one of these models, given the order of the cards prior to shuffling? I'm thinking something along the lines of being able to say that the odds of a given card being the next one are higher than they should be, not outright predicting the full order of the cards.
It's absolutely trivial, taking a few lines of code.
I've broken all sorts of code using similar tools.
// Code to demonstrate finding the hidden seed of a PRNG with Z3
// Chris Lomont Oct 2021
// Answering this comment on Hacker News https://news.ycombinator.com/item?id=28886698
// Start by getting Z3, a theorem prover from Microsoft, via nuget. See https://github.com/Z3Prover/z3
using Microsoft.Z3;
using System;
// get a solution
ulong Solution(Context ctx, BoolExpr f, BitVecExpr seed)
{
Solver s = ctx.MkSolver();
s.Assert(f); // assert constraint into solver
if (s.Check() == Status.SATISFIABLE)
{
var m = s.Model;
Expr e = m.Evaluate(seed);
return ulong.Parse(e.ToString());
}
else
throw new Exception("Fatal error");
}
// simple PRNG, used in many old C libs
UInt32 next = 0x1234;
UInt32 rand()
{
next = next \* 214013 + 2531011;
return (next / 65536) % 32768;
}
void Test()
{
var R = new Random();
next = (uint)R.Next();
var start = next;
Console.WriteLine($"Starting seed {next:X8}");
using (var ctx = new Context())
{
// 32 bit vector type
Sort bv_type = ctx.MkBitVecSort(32);
// unknown seed - we will solve for this
BitVecExpr seed = ctx.MkBVConst("seed", 32);
// constants used in the PRNG
BitVecExpr c214 = (BitVecNum)ctx.MkNumeral("214013", bv_type);
BitVecExpr c253 = (BitVecNum)ctx.MkNumeral("2531011", bv_type);
BitVecExpr c65536 = (BitVecNum)ctx.MkNumeral("65536", bv_type);
BitVecExpr c32768 = (BitVecNum)ctx.MkNumeral("32768", bv_type);
// track the boolean to satisfy
BoolExpr be = ctx.MkTrue();
var next = seed; // start here
int pass = 0;
while(true)
{
++pass;
if (pass > 10) break;
// the sampled random
var r = rand();
BitVecExpr rndBV = (BitVecNum)ctx.MkNumeral(r, bv_type);
// make this code using Z3 variables
//next = next * 214013 + 2531011;
//return (next / 65536) % 32768;
next = ctx.MkBVAdd(ctx.MkBVMul(next, c214), c253);
var ret = ctx.MkBVURem(ctx.MkBVUDiv(next, c65536), c32768);
// add a constraint boolean for this "Z3 ret = returned value"
be = ctx.MkAnd(be, ctx.MkEq(ret, rndBV));
// get solution
var val = Solution(ctx, be, seed);
// todo - can check unique by adding "seed != soln" to the boolean and checking
Console.WriteLine($"{pass} : 0x{val:X8}");
if (val == start)
break; // done - can also break when shown unique
}
}
}
Test();