[Link to original writeup](https://wrecktheline.com/writeups/imaginary-2021/#password%20checker)
# Password Checker (15 solves, 450 points)by JaGoTu
## Description```I seem to have forgotten my password. Before I lock myself out, I immediately went to my password checker that I coded, but it amounted to no avail. I guess I will leave it to the experts.
Wrap your flag in ictf before submitting.
Attachmentshttp://password-checker.chal.imaginaryctf.org
AuthorZyphen
Points450```
## Obfuscated JavaScript
The site has a single textbox to input the password, and after pressing the button it is checked in JavaScript.The relevant part of the JavaScript after deobfuscation is this:
```JS	order = "3|2|0|1|4"["split"]("|"),	current_step = 0x0;	while ( !! []) {		switch (order[current_step++]) {		case 0:			var checksum = 0x0;			continue;		case 1:			for (var index = 0x0; index < password["length"]; index++) {				summed += password["charCodeAt"](index),				xored ^= password["charCodeAt"](index),				checksum = (checksum << 0x5) - checksum + password["charCodeAt"](index)			};			continue;		case 2:			var xored = 0x0;			continue;		case 3:			var summed = 0x0;			continue;		case 4:			console["log"](summed, xored, checksum); ! /[^ZYPH3NAFUR1GT_BMKLE.0]/ ["test"](password) &&			summed == 0x7e8 &&			xored == 0x7e &&			checksum == -0x28dd475e &&			password["charCodeAt"](0x0) - password["charCodeAt"](0x1) == 0x1 &&			Math["floor"](password["charCodeAt"](0x1) * password["charCodeAt"](0x2) * password["charCodeAt"](0x3) / 0x736) == 0x115 &&			password["charCodeAt"](0x4) + password["charCodeAt"](0x5) - password["charCodeAt"](0x6) + password["charCodeAt"](0x7) == 0x72 &&			Math["floor"](password["charCodeAt"](0x8) * password["charCodeAt"](0x9) / password["charCodeAt"](0xa) * password["charCodeAt"](0xb)) == 0xcb1 &&			Math["floor"](password["charCodeAt"](0xd) / password["charCodeAt"](0xc) / password["charCodeAt"](0xe) * password["charCodeAt"](0xf)) == 0x1 &&			(password["charCodeAt"](0x10) &&			password["charCodeAt"](0x12) == "ZYPH3NAFUR1GT_BMKLE.0"["length"] << 0x2) &&			password["charCodeAt"](0x6) == password["charCodeAt"](0x11) &&			Math["floor"](password["charCodeAt"](0x13) * password["charCodeAt"](0x14) / password["charCodeAt"](0x15)) == 0x2e &&			password["charCodeAt"](0x16) + password["charCodeAt"](0x17) - password["charCodeAt"](0x18) == 0x74 &&			password["charCodeAt"](0x19) + password["charCodeAt"](0x1a) + password["charCodeAt"](0x1b) == 0x8a &&			alert("Congrats!!!");			continue		};		break	}```
The steps are in order 3-2-0-1-4, so first `summed`, `xored` and `checksum` are inited to zero, then in #1 the values of them are calculated, and then in #4 the actual checking takes place. The conditions mostly just take triplets of characters and check some conditions on them.
## Z3 and guessingThis looks like a task for z3, so we implement all the conditions:
```pyfrom z3 import *
chars = []sum = 0xored = 0checksum = 0
s = SolverFor("QF_BV")for i in range(28):    curr = BitVec('c' + str(i), 32)    chars.append(curr)    sum += curr    xored ^= curr    checksum = 31*checksum + curr    lol = (curr == ord('Z'))    for c in "YPH3NAFUR1GT_BMKLE.0":        lol = Or(lol, curr == ord(c))    s.add(lol)
def floor_div(top, bottom, res):    s.add(top > bottom*res)    s.add(top < bottom*res+bottom)
password = chars
s.add(sum==0x7e8)s.add(xored == 0x7e)s.add(checksum == 0xD722B8A2)s.add(password[0x0] - password[0x1] == 0x1)floor_div(password[0x1] * password[0x2] * password[0x3], 0x736, 0x115)s.add(password[0x4] + password[0x5] - password[0x6] + password[0x7] == 0x72)floor_div(password[0x8] * password[0x9] * password[0xb], password[0xa], 0xcb1)floor_div(password[0xd]*password[0xf], password[0xc] * password[0xe],1 )s.add(password[0x12] == 84)s.add(password[0x6] == password[0x11])floor_div(password[0x13] * password[0x14], password[0x15], 0x2e)s.add(password[0x16] + password[0x17] - password[0x18] == 0x74)s.add(password[0x19] + password[0x1a] + password[0x1b] == 0x8a)
print(s.check())m = s.model()
out = ''for i in range(28):    out += chr(m[password[i]].as_long())
print(out)```
However, the search space is too large even when using the parallel evaluator ☹. As we mentioned earlier, the characters are mostly conditioned in triplets. So let's try to go fora more guessy approach, just see all the possible triplets and guess the ones that look the most english-y.
The last triplet is easy:
```py$ cat test.pyimport syslol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:    for b in lol:        for c in lol:            if ((ord(a)+ord(b)+ord(c))) == 0x8a:                print(a+b+c)
$ python3 test.py...```
For the second to last triplet we get multiple options:```py$ cat test.pyimport syslol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:    for b in lol:        for c in lol:            if ((ord(a)+ord(b)-ord(c))) == 0x74:                print(a+b+c+"...")
$ python3 test.pyZH....Z_E...ZM3...ZK1...YN3...YK0...YL1...PU1...PR....PT0...HZ....H_3...NY3...NT....F_1...UP1...UR3...UM....RP....RU3...RR0...TP0...TN...._ZE..._H3..._F1..._E0...MZ3...MU....KZ1...KY0...LY1...E_0...```
After looking at this, the most english-like options are the `RU3...` and `UR3...`. So let's try the previous triplet with both of these:
```pyimport syslol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:    for b in lol:        for c in lol:            if (ord(a)*ord(b)//ord(c)) == 0x2e:                print(a+b+c+"UR3...")                print(a+b+c+"RU3...")```
Not gonna include the full output, but one of them was `0RTUR3...`, which looks a lot like torture :) so we also guess `_T` before that.
Now let's try from the other side: the first three characters are actually a bit special, as the second character is in two conditions, `password["charCodeAt"](0x0) - password["charCodeAt"](0x1) == 0x1` and `Math["floor"](password["charCodeAt"](0x1) * password["charCodeAt"](0x2) * password["charCodeAt"](0x3) / 0x736) == 0x115`. Let's bruteforce both of them at once:
```py$ cat test.pyimport syslol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:    if chr(ord(a)-1) in lol:        for b in lol:            for c in lol:                if ((ord(a)-1)*ord(b)*ord(c))//0x736== 0x115:                        print(a+chr(ord(a)-1)+b+c)$ python3 test.pyZYPHZYHPHGUUHG_LHGL_NMF_NM_FGF_MGFM_MLZKMLG_ML_GMLKZLKZLLKH_LK_HLKLZ```
Hm, one of them is ZYPH, and the author of this challenge is... Zyphen. :) Also, as `password[0x6] == password[0x11]`, we know the 7th character will be '_':
```pyimport syslol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:    for b in lol:        for c in ['_']:            for d in lol:                if ((ord(a)+ord(b)-ord(c))+ord(d)) == 0x72:                    print("ZYPH" + a+b+c+d)```
There's only one result containing ZYPHEN or ZYPH3N, and that is `ZYPH3N_P`.To sum it all up, we know the password looks like the following:
`ZYPH3N_P?????????_T0RTUR3...`
That should be enough for our Z3 :) Let's add the following to the original script:
```pys.add(password[27] == ord('.'))s.add(password[26] == ord('.'))s.add(password[25] == ord('.'))s.add(password[24] == ord('3'))s.add(password[23] == ord('R'))s.add(password[22] == ord('U'))s.add(password[21] == ord('T'))s.add(password[20] == ord('R'))s.add(password[19] == ord('0'))s.add(password[18] == ord('T'))s.add(password[17] == ord('_'))
s.add(password[0] == ord('Z'))s.add(password[1] == ord('Y'))s.add(password[2] == ord('P'))s.add(password[3] == ord('H'))s.add(password[4] == ord('3'))s.add(password[5] == ord('N'))s.add(password[6] == ord('_'))s.add(password[7] == ord('P'))```
And after a while we get the result:
```$ python3 checker.pysatZYPH3N_P1Z_F0RG3T_T0RTUR3..```
The flag is `ictf{ZYPH3N_P1Z_F0RG3T_T0RTUR3...}`.