Skip to main content
added 66 characters in body
Source Link
:sat \s i -> lcg s i knownXor knownMult == knownOutput
(\s i -> lcg s i knownXor knownMult ==
     knownOutput) 0x48f0d1a37afa2b670x48f0d1a3afc9565e 0x25eff26152b834d10x2f21de6409b2bc69 = True 

SoSo the seed is 0x48f0d1a37afa2b67 and increment is 0x25eff26152b834d1.

... so the real seed is 0x48f0d1a37afa2b670x48f0d1a3afc9565e and increment is 0x25eff26152b834d10x2f21de6409b2bc69. Would case 3 be broken in a similar time frame? (unless I don't know!typoed something).

:sat \s i -> lcg s i knownXor knownMult == knownOutput
(\s i -> lcg s i knownXor knownMult ==
     knownOutput) 0x48f0d1a37afa2b67 0x25eff26152b834d1 = True

So the seed is 0x48f0d1a37afa2b67 and increment is 0x25eff26152b834d1. Would case 3 be broken in a similar time frame? I don't know!

:sat \s i -> lcg s i knownXor knownMult == knownOutput
(\s i -> lcg s i knownXor knownMult ==
     knownOutput) 0x48f0d1a3afc9565e 0x2f21de6409b2bc69 = True 

So the seed is 0x48f0d1a37afa2b67 and increment is 0x25eff26152b834d1.

... so the real seed is 0x48f0d1a3afc9565e and increment 0x2f21de6409b2bc69 (unless I typoed something).

added 398 characters in body
Source Link

EDIT: And one of my stupidly-long running SAT sessions, case 2 running for just under two weeks, finished with

:sat \s i -> lcg s i knownXor knownMult == knownOutput
(\s i -> lcg s i knownXor knownMult ==
     knownOutput) 0x48f0d1a37afa2b67 0x25eff26152b834d1 = True

So the seed is 0x48f0d1a37afa2b67 and increment is 0x25eff26152b834d1. Would case 3 be broken in a similar time frame? I don't know!

EDIT: And one of my stupidly-long running SAT sessions, case 2 running for just under two weeks, finished with

:sat \s i -> lcg s i knownXor knownMult == knownOutput
(\s i -> lcg s i knownXor knownMult ==
     knownOutput) 0x48f0d1a37afa2b67 0x25eff26152b834d1 = True

So the seed is 0x48f0d1a37afa2b67 and increment is 0x25eff26152b834d1. Would case 3 be broken in a similar time frame? I don't know!

Source Link

Putting some of my comments into writing. This is less than an answer but too much for a comment. In the comments I had claimed to apply SMT to solve case 1 - this is false, I was mistaken. I have had cases 2 and 3 running SMT (boolector, Z3, CVC4, yices) for some time without success. The closest thing to success is the identification of seeds that produce matching output for the first ~96 bits. Past that point the solvers appear to take geometrically (or worse) more time matching seed per additional bit of matching output. The formulation is a naive use of Cryptol:

lcg : {n} (fin n) => [64] -> [64] -> [64] -> [64] -> [n][32]
lcg seed inc ex mult =
    [rand | (_,rand) <- take`{n} (drop`{1} seq) ]
 where
 seq = [(seed,0)] # [(st * mult + inc, drop (((st * mult + inc) >> 32) ^ ex)) | (st,_) <- seq]

harderOutput : [4][32]
harderOutput = [0x5e3af925, 0x1b7f8e1a, 0x268c64d1, 0x4b614b92]

harderMult : [64]
harderMult   = 0xc278c0d1c04a88d9

knownMult : [64]
knownMult = 0xc278c0d1c04a88d9

knownXor : [64]
knownXor = `0x0

knownOutput : [4][32]
knownOutput = [0x8c005b3e, 0x27e3338e, 0x1bb199bb, 0x46449299]

trivialMult : [64]
trivialMult = 0xc278c0d1c04a88d9

trivialOutput : [4][32]
trivialOutput = [0x8b1294a5, 0xae5cbf0d, 0x2da164bd, 0xcbe27c6d]

doneSeed : [64]
doneSeed = 0x35e647cfd3423fd0

doneMult : [64]
doneMult = 0xc278c0d1c04a88d9

doneOutput : [4][32]
doneOutput = [0x59502137, 0xb6152ece, 0xbbd2cb88, 0xef05249f]

// case 1:
// :sat \s -> lcg s zero zero trivialMult == trivialOutput

// case 2:
// :sat \s i -> lcg s i knownXor knownMult == knownOutput

// case 3:
// :sat \s i x -> lcg s i x harderMult == harderOutput

And an example, which terminates quite quickly, in which we find initial values producing an identical first 3 words (96 bits) includes:

Main> :sat \s i x -> lcg s i x harderMult == take `{3} harderOutput
(\s i x -> lcg s i x harderMult ==
       take`{3} harderOutput) 0x897c9820380325ef 0xa75286c029abc35f 
                  0x00000000dd1aa469 = True

Notice it is actually harder (well, slower) for this method to obtain a solution in which the only unknown is the seed:

Main> :sat \s -> lcg s zero zero trivialMult == take `{3} trivialOutput
... still waiting after many minutes ...

So contrary to my earlier comment it appears a @Charphacy's mental power plus Mathematica has done better on this problem than the typical SMTs.