Certifying RSA correct for breakfast

Reasoning on the correctness of the RSA cryptosystem is much easier with a little bit of algebra: this is a perfect example of a case where the ``practical’’ applications of proof assistants can be helped with libraries dealing with abstract algebra, including SSReflect. The proof we are going to build in the present post is based on a stock SSReflect version 1.3pl1, and is available on github. It can be compared with the RSA contribution to Coq, made on the basis of the standard library (note this is not a code golf, but rather a tentative to demonstrate that a big mathematical library helps).

Let us look at the encryption and decryption primitives of RSA: given a message, $M$, represented as a number, the cypher text $C$ is given by $C \equiv M^e \pmod n$. Likewise the decryption is defined as $M = C^d \pmod n$. The public key is the pair $(e,n)$ and the private key is the pair $(d,n)$, with the message $M$ chunked and padded appropriately so that $M \leq n$. In SSReflect:

Definition encrypt (w : nat) := (w ^ e) %% n.

Definition decrypt (w : nat) := (w ^ d) %% n.

The correctness property verifies that the cypher text allows us to recover the original message, i.e.:

For that, it suffices to choose $e,d$ so that :

where $\Phi$ designates Euler’s totient function : $\Phi(n)$ is the number of integers $1 \leq m phi x = x.-1. Proof. move=> x; move/phi_pfactor; move/(_ _ (ltn0Sn 0)). by rewrite expn1 expn0 muln1. Qed.

Lemma pq_phi: phi(n) = p.-1 * q.-1.
Proof.
rewrite phi_coprime; last by rewrite pq_coprime.
by rewrite !phi_prime //.
Qed.

(*  We pick an exponent e coprime to phi(n) *)

Variable e : nat.
Hypothesis e_phin_coprime: coprime (phi n) e.

Definition d := (fst (egcdn e (phi n))).

(* We check that ed is 1 modulo (phi n) *)

Lemma ed_1_mod_phin: e * d = 1 %[mod (phi n)].
Proof.
by  rewrite -(chinese_modl e_phin_coprime 1 0) /chinese
  addn0 mul1n.
Qed.

In this introduction of basic lemmas, we noticed that the value of $\Phi$ for a prime wasn’t included in the library. However, the Search tool of SSReflect allowed us to quickly find a more general lemma on the value of $\Phi$ based on the prime decomposition of a number (phi_pfactor above).

And finally, the value of $ed \pmod{\Phi(n)}$ leads to correctness thanks to Euler’s theorem:

For all $n$ and $a$ coprime to $n$, $a^{\Phi(n)} \equiv 1 \pmod n$

Hence, $\exists k$ such that $ed = k \Phi(n)+1$, so that \(M^{ed} = M^{k \Phi(n)+1} = M^{k \Phi(n)} M \equiv M \pmod n\) is a consequence of Euler’s theorem if $M$ and $n$ are coprime.

The bane of working with a proof assistant is that we can’t ignore an often-overlooked detail: if $M$ and $n$ are not coprime (and if $M \neq n$, otherwise this is trivially true), we can assume, without loss of generality that $p | M$ and $q$ and $M$ are coprime. Indeed:

Lemma notcoprime: forall x, 0  ~~ (coprime x n) ->
  ((p %| x) && coprime x q) || ((q %| x) && coprime x p).
Proof.
move=> x; case/andP=>[x_gt0 x_lt_n]; rewrite coprime_mulr; move/nandP.
move/orP; rewrite coprime_sym [coprime _ q]coprime_sym 2?prime_coprime //.
case Hdvdn: (p %| x) =>/=; rewrite ?negbK ?andbF ?andbT // orbF=>_.
have xdpp_x: (x %/p) * p = x by move: (Hdvdn); rewrite dvdn_eq; move/eqP.
rewrite -xdpp_x; apply/negP=> H; move:H; rewrite (euclid _ _ prime_q).
rewrite [ _ %| p]dvdn_prime2 // eq_sym; move/negbTE: neq_pq=>->.
rewrite orbF=>H; move: (dvdn_mul (dvdnn p) H).
rewrite [_ * (_ %/ _)]mulnC xdpp_x; move/(dvdn_leq x_gt0).
by rewrite leqNgt x_lt_n.
Qed.

In that case $M^{k \Phi(n)} M \equiv M \pmod q$ is a consequence of Euler’s theorem, and $M^{k \Phi(n)} M \equiv M \pmod p$ is trivially true, which allows us to conclude using a Chinese lemma. Most presentations of RSA cop out of treating this case, but it makes the encoding no less correct. We can now prove the theorem:

Theorem rsa_correct1 :
 forall w : nat, w  (decrypt (encrypt w)) = w %[mod n].
Proof.
move=> w w_leq_n; rewrite modn_mod modn_exp -expn_mulr.

This simplifies the goal to w ^ (e * d) = w %[mod n]. Then we are going to want to treat the case where w = 0 first. Since this is a decidable property, we proceed by making a case on `0 ->.

We are brought to 0 ^ (e * d) = 0 %[mod n]. The left part forces us to check that `0 ->.

We are left with ` 0 0$ ! Simplifying our goal a little further:

have:= (divn_eq (e*d) (phi n)); rewrite ed_1_mod_phin modn_small // =>->.

We get : w ^ ((e * d) %/ phi n * phi n + 1) = w %[mod n], and we are ready to conclude for the case where message and modulus are coprime ! This is the core of the proof : a simple use of Euler’s theorem and a few helper lemma on moduli.

case cp_w_n : (coprime w n).
  rewrite expn_add [_ * phi n]mulnC expn_mulr -modn_mul2m; move: cp_w_n.
  by move/Euler=>E; rewrite -modn_exp E modn_exp exp1n modn_mul2m mul1n.

Now, in the case where modulus and message are not coprime, we are going to want to use the notcoprime lemma above, for which we also require them not to be equal, so we quickly eliminate that case.

case w_eq_n: (w == n).
   by move/eqP: w_eq_n =>->; rewrite -modn_exp modnn exp0n ?mod0n ?addn1.

Finally, we apply the chinese lemma, to separate our requirements on $w \pmod{\Phi(n)}$ into requirements on $w \pmod{\Phi(p)}$ and $w \pmod{\Phi(q)}$:

move: w_leq_n; rewrite leq_eqVlt {}w_eq_n orFb; move=> w_lt_n.
apply/eqP; rewrite chinese_remainder; last first.
  by rewrite prime_coprime // dvdn_prime2.

The goal at this stage is

 (w ^ ((e * d) %/ phi n * phi n + 1) == w %[mod p]) &&
   (w ^ ((e * d) %/ phi n * phi n + 1) == w %[mod q])

We want to rewrite this a little further to make the prime $w$ is not divisible by more prominent.

rewrite mulnC {1 3}pq_phi {2}[_ * q.-1]mulnC -2!mulnA 2!expn_add expn_mulr.
rewrite [w ^ ( q.-1 * _ )]expn_mulr expn1 -modn_mul2m -(modn_mul2m _ _ q).
rewrite -modn_exp -(modn_exp _ q).

This gives us the goal:

 ((w ^ p.-1 %% p) ^ (q.-1 * ((e * d) %/ phi n)) %% p * (w %% p) == w %[mod p]) &&
   ((w ^ q.-1 %% q) ^ (p.-1 * ((e * d) %/ phi n)) %% q * (w %% q) == w %[mod q])

We can now use notcoprime above, apply Euler’s theorem in each case, and conclude !

move/andP: (conj (idP w_gt0) w_lt_n).
move/notcoprime; move/(_ (negbT cp_w_n)); case/orP; move/andP=> [Hdvdn Hncp].
  move: Hdvdn; rewrite /dvdn; move/eqP=>->; rewrite muln0 mod0n /=.
  move/Euler:Hncp; rewrite (phi_prime prime_q)=>->.
  by rewrite modn_exp exp1n modn_mul2m mul1n.
move: Hdvdn; rewrite /dvdn; move/eqP=>->; rewrite muln0 mod0n /= andbT.
move/Euler:Hncp; rewrite (phi_prime prime_p)=>->.
by rewrite modn_exp exp1n modn_mul2m mul1n.
Qed.

This concludes our certification of RSA’s correctness, in itself 30 lines of proof script. Note we have never used any automated tactic database such as auto, which confers our proof script a particularly deterministic nature (but it’s not a requirement, of course). Here’s a run of coqwc, the coq line-count utility, on our final file:

   spec    proof comments
     28       53       17         RSA.v

The final file is 126 lines.