Elgamal暗号でSSReflectのトライアル

# 目的

CoqのSSReflectの入門・演習として、Elgamal暗号の証明します。環境構築、定式化、証明を順に行います。

Elgamal暗号の本定式化はまったく高速ではありませんし、未だにSSReflectを使いこなせていませんので内容についてご了承ください。

[RSAの証明のブログ](http://blog.garillot.net/post/9454837194/certifying-rsa-correct-for-breakfast)を参考に作っています。作成した証明は[こちら](https://github.com/junjihashimoto/coq-elgamal/blob/master/Elgamal.v)です。

# 環境構築

今回windowsで行った。手順は下記であるが、注意点はmath-compが要求するcoqのバージョンを確認してインストールします。
単純に最新版をいれるとバージョンの不一致が起こり動作しないです。

1. [math-comp](https://github.com/math-comp/math-comp/releases)をインストール
2. [coqのリリース一覧](https://github.com/coq/coq/tags)から上記のmath-compの要求するバージョン（今回は8.7.0）をインストール

参考までに、linuxならopamを使った[こちら](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html)の手順があります。

# Elgamal暗号の定式化

Elgamal暗号の暗号化と復号化は下記のように定式化しました。
[Wikipedia](https://ja.wikipedia.org/wiki/ElGamal%E6%9A%97%E5%8F%B7)のものを参考に、逆元はフェルマーの小定理から$p-1$乗が単位元になるので$p-2$乗を逆元に使って計算しています。

```coq
Section Elgamal.
Variable p g : nat.
Variable prime_p : prime p.
Variable prime_g : prime g.

Variable pri : nat.
Hypothesis pri_lt_p : pri < p.
Hypothesis g_lt_p : g < p.

Variable r : nat.
Hypothesis r_lt_p : r < p.

Definition pub := (g ^ pri) %% p.

Definition enc1 := g ^ r %% p.
Definition enc2 (m : nat) := (pub ^ r * m) %% p.

Definition dec (e1 : nat) (e2 : nat) := e2 * ((e1 ^ (p - 2)) ^ pri) %% p.

Theorem elgamal_correct1 :
 forall w : nat, w < p -> dec enc1 (enc2 w) = w %[mod p].
Proof.
Admitted.

End Elgamal.
```

# 証明の構築のながれ

証明は下記のように行いました。

1. math-compのライブラリのオイラーの定理を元にフェルマーの小定理を構築
    * RSAの証明のブログのほぼコピペ
2. 上記のelgamal_correct1の定理のdec,enc1,enc2をすべて展開。
3. SSReflectのlemmaの[ssrnat](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v),[div](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/div.v)を参考に式の変形。
    * modnMml, expnM, mulnCとかは式の変形につかったLemmaです。
    * 式変形に必要なLemmaはgrepで調べました。
4. 変形した式にフェルマーの小定理(ex5のところ)を適用。

下記は実際のコードです。

```coq
Lemma ex1 : (g ^ pri %% p) ^ r = g ^ (pri * r) %[mod p].
Proof.
by rewrite modnXm expnM.
Qed.

Lemma ex2 : (g ^ r %% p) ^ ((p - 2) * pri) = g ^ (r *(p - 2) * pri) %[mod p].
Proof.
rewrite modnXm !expnM //.
Qed.

Lemma ex3: pri * r * (p - 2) + pri * r = pri * r * (p - 1).
Proof.
rewrite -{2}[pri * r]muln1.
rewrite -mulnDr.
have pluslemma : (p - 2) +1 = p - 1.
- rewrite addn1.
  apply subnSK.
  by rewrite prime_gt1.
rewrite pluslemma //.
Qed.

Lemma phi_prime : forall x, prime x -> totient x = x.-1.
Proof.
move=> x; move/totient_pfactor; move/(_ _ (ltn0Sn 0)).
by rewrite expn1 expn0 muln1.
Qed.

Lemma gp_coprime: coprime g p.
Proof.
rewrite prime_coprime //.
rewrite dvdn_prime2 //.
rewrite neq_ltn.
rewrite g_lt_p.
by [].
Qed.

Lemma ex5: g ^ (p - 1) %% p = 1.
Proof.
rewrite subn1.
rewrite -phi_prime.
rewrite Euler_exp_totient.
- rewrite modn_small //.
- rewrite prime_gt1 //.
- rewrite gp_coprime //.
- rewrite prime_p //.
Qed.

Theorem elgamal_correct1 :
 forall w : nat, w < p -> dec enc1 (enc2 w) = w %[mod p].
Proof.
move => w w_le_p.
rewrite /dec.
rewrite modn_mod.
rewrite /enc1 /enc2 /pub.
rewrite modnMml.
rewrite -expnM.
rewrite -modnMm.
rewrite -[((g ^ pri %% p) ^ r * w) %% p ]modnMm.
rewrite ex1.

rewrite [(g ^ (pri * r) %% p * (w %% p)) %% p]modnMm.
rewrite ex2.

rewrite modnMm.
rewrite mulnC.
rewrite mulnA.
rewrite -expnD.
rewrite -[_ * pri]mulnC. 
rewrite [pri * _]mulnA.
rewrite ex3.

rewrite -[pri * r * (p - 1)]mulnC expnM.
rewrite -modnMml.
rewrite -modnXm.
rewrite ex5.

rewrite exp1n.
rewrite modnMml.
rewrite mul1n.
by [].
Qed.
```

# まとめ

Coqの初心者なので、証明の良し悪しもわからないですが、SSReflectとmath-compを使ってなんとかElgamal暗号の復号で戻る証明ができました。

# 参考資料

* [affeldtさんの資料](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/)
* [math-comp book](https://math-comp.github.io/mcb/)
* [math-compのトップページ](http://math-comp.github.io/math-comp/)の[SSReflectの資料](https://hal.inria.fr/inria-00258384/en)
* [RSAの証明のブログ](http://blog.garillot.net/post/9454837194/certifying-rsa-correct-for-breakfast)