Indistinguishability and non-derivability are fundamental security notions for cryptographic protocols. Formal indistinguishabilityrelations (FIR) and formal non-derivability relations (FNDR) provide a framework for automated security analysis that is cryptographically sound: proofs in the FIR/FNDR system imply security against probabilistic polynomial-time adversaries. Existing automated provers either lack computational soundness or rely on hand-crafted heuristics, limiting scalability.We present CryptoRL, a reinforcement learning-based prover for FIR/FNDR problems. Our approach combines: (1) a canonicallanguage encoding structural information into symbol names, enabling neural networks to learn generalizable proof strategies; (2) a two-phase architecture separating procedural hash removal from learned frame transformation; and (3) curriculum learning with 2D difficulty progression, realized through delegation-chain training.We evaluate CryptoRL on 12 real-world cryptographic protocols, proving 11 fully automatically—including Schnorr signatures(previously unprovable due to non-convergent AC equations) and Paillier encryption (requiring multi-assumption chaining). Alldeployed models achieve over 90% success on held-out test problems. Compared to breadth-first enumeration, RL-guided search requires 10× fewer search nodes. All generated proofs are checked by a replay-based verifier.To our knowledge, this is the first application of deep reinforcement learning to cryptographic indistinguishability proofs. CryptoRL achieves what no prior tool offers: fully automated proofs with cryptographic soundness—security guarantees against probabilistic polynomial-time adversaries, not merely symbolic attackers.
Long NGO (Sat,) studied this question.