# Tough

This is a simple java program:

```java
import java.util.*;

public class tough
{
public static int[] realflag = {9,4,23,8,17,1,18,0,13,7,2,20,16,10,22,12,19,6,15,21,3,14,5,11};
public static int[] therealflag = {20,16,12,9,6,15,21,3,18,0,13,7,1,4,23,8,17,2,10,22,19,11,14,5};
public static HashMap<Integer, Character> theflags = new HashMap<>();
public static HashMap<Integer, Character> theflags0 = new HashMap<>();
public static HashMap<Integer, Character> theflags1 = new HashMap<>();
public static HashMap<Integer, Character> theflags2 = new HashMap<>();
public static boolean m = true;
public static boolean g = false;

public static void main(String args[]) {
Scanner scanner = new Scanner(System.in);
System.out.print("Enter flag: ");
String userInput = scanner.next();
String input = userInput.substring("rtcp{".length(),userInput.length()-1);
if (check(input)) {
System.out.println("Access granted.");
} else {
System.out.println("Access denied!");
}
}

public static boolean check(String input){
boolean h = false;
String flag = "ow0_wh4t_4_h4ckr_y0u_4r3";
// realflag
createMap(theflags, input, m);
// therealflag
createMap(theflags0, flag, g);
// therealflag
createMap(theflags1, input, g);
// realflag
createMap(theflags2, flag, m);
String theflag = "";
String thefinalflag = "";
int i = 0;
System.out.println(input.length());
System.out.println(flag.length());
if(input.length() != flag.length()){
return h;
}
if(input.charAt(input.length()-2) != 'o'){
return false;
}
if(!input.substring(2,4).equals("r3") || input.charAt(5) != '_' || input.charAt(7) != '_'){
return false;
}
System.out.println("arrived here");
//rtcp{h3r3s_a_fr33_fl4g!}
for(; i < input.length()-3; i++){
theflag += theflags.get(i);
}
for(; i < input.length();i++){
theflag += theflags1.get(i);
}
for(int p = 0; p < theflag.length(); p++){
thefinalflag += (char)((int)(theflags0.get(p)) + (int)(theflag.charAt(p)));
}
for(int p = 0; p < theflag.length(); p++){
if((int)(thefinalflag.charAt(p)) > 146 && (int)(thefinalflag.charAt(p)) < 157){
// thefinalflag = thefinalflag[0:p] + chr(thefinalflag[p] + 10) + thefinalflag[p+1:]
// thefinalflag[p] = thefinalflag[p] + 10
thefinalflag = thefinalflag.substring(0,p) + (char)((int)(thefinalflag.charAt(p)+10)) + thefinalflag.substring(p+1);
}
}
return thefinalflag.equals("ì¨ ¢«¢¥Ç©© ÂëÏãҝËãhÔÊ");
}
public static void createMap(HashMap owo, String input, boolean uwu){
if(uwu){
for(int i = 0; i < input.length(); i++){
owo.put(realflag[i], input.charAt(i));
}
} else{
for(int i = 0; i < input.length(); i++){
owo.put(therealflag[i], input.charAt(i));
}
}
}
}
```

We can crack it using z3:

```py
#!/usr/bin/env python3

from z3 import *
import sys

s = Solver()
realflag = [9,4,23,8,17,1,18,0,13,7,2,20,16,10,22,12,19,6,15,21,3,14,5,11]
therealflag = [20,16,12,9,6,15,21,3,18,0,13,7,1,4,23,8,17,2,10,22,19,11,14,5]
flag = "ow0_wh4t_4_h4ckr_y0u_4r3"
my_input = [BitVec(f"a_{i:2}", 8) for i in range(len(flag))]
theflag = [BitVec(f"c_{i}", 8) for i in range(len(flag) * 2)]
thefinalflag = [BitVec(f"f_{i}", 8) for i in range(len(flag) * 2)]
definitive = [BitVec(f"s_{i}", 8) for i in range(len(flag) * 2)]

theflags = {}
theflags0 = {}
theflags1 = {}
theflags2 = {}
for i in range(len(my_input)):
theflags[realflag[i]] = my_input[i]
theflags0[therealflag[i]] = flag[i]
theflags1[therealflag[i]] = my_input[i]
theflags2[realflag[i]] = flag[i]

for m in my_input:
s.add(m >= 0x20, m < 0x7f)

s.add(my_input[-2] == ord('o'))
for i in range(2):
s.add(my_input[i + 2] != ord("re"[i]))
s.add(my_input[5] == ord('_'))
s.add(my_input[7] == ord('_'))

k = 0
z = 0
for i in range(len(my_input) - 3):
s.add(theflag[k] == theflags.get(i))
k += 1

for i in range(len(my_input) - 3, len(my_input)):
s.add(theflag[k] == theflags1.get(i))
k += 1

for i in range(k):
s.add(thefinalflag[z] == ord(theflags0.get(i)) + theflag[i])
z += 1

# x == 5
# x == x + 5
for i in range(k):
x = If(And(thefinalflag[i] > 146, thefinalflag[i] < 157), 10, 0)
s.add(definitive[i] == thefinalflag[i] + Int2BV(x, 8))

final_check = [157, 157, 236, 168, 160, 162, 171, 162, 165, 199, 169, 169, 160, 194, 235, 207, 227, 210, 157, 203, 227, 104, 212, 202]
for f, c in zip(definitive, final_check):
s.add(f == c)

print(s.check())
m = s.model()
#print(m)
model = sorted([(d, m[d]) for d in m], key = lambda x: str(x[0]))
for m in model:
if "a" in str(m[0]):
print(chr(m[1].as_long()), end='')
print()
```

Flag:

rtcp{h3r3s_4_c0stly_fl4g_4you}