Looks like there is cryptography based on NP-hard problem, e.g. McEliece cryptosystem. The algorithm is an asymmetric encryption algorithm and is based on the hardness of decoding a general linear code (which is known to be NP-hard)
We are trying to strengthen this result.
Q1: Is strictly harder than NP-hard cryptography encryption or signature algorithm possible?
We don't allow One-Time Pads (OTP) and similar external secrets.
Conjecture J1: the answer is negative via generic attack of symbolic execution and then solve SAT with NP-oracle.
J1 implies that if a C language program implements some cryptographic algorithm and runs in time $X$ milliseconds, then the symbolic execution size of the CNF formula that breaks the algorithm is polynomial in $X$. XXX make this more rigorous.
It may be a good idea to unroll the loops by hand and ask about loopless programs.
Counterexample to J1 might be candidate for hard cryptography.
The main problem with J1 is that the resulting CNF might be of exponential size. We did some experiments with CBMC: Bounded Model Checker with factorization and the hash function SHA256 and the CNF were small enough.
Here is toy RSA example with zero knowledge of integer factorization:
void main() {
int nondetint();/* can be anything */
int p,q,n;
p=nondetint();
q=nondetint();
n=p*q;
__CPROVER_assert(!(n==13*17 && 1 <p && p <n && 1 < q && q <n),"factor");
}
$cbmc --trace factor1.c
This approach might be used to mine bitcoins SAT solving - An alternative to brute force bitcoin mining.
Also this appears consistent with the fact that if P=NP all crypto will break.
Potential candidates are $\Sigma_2^p$-hard problems.