LoginSignup
2

More than 5 years have passed since last update.

Elgamal暗号でSSReflectのトライアル

Last updated at Posted at 2018-02-04

目的

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

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

RSAの証明のブログを参考に作っています。作成した証明はこちらです。

環境構築

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

  1. math-compをインストール
  2. coqのリリース一覧から上記のmath-compの要求するバージョン(今回は8.7.0)をインストール

参考までに、linuxならopamを使ったこちらの手順があります。

Elgamal暗号の定式化

Elgamal暗号の暗号化と復号化は下記のように定式化しました。
Wikipediaのものを参考に、逆元はフェルマーの小定理から$p-1$乗が単位元になるので$p-2$乗を逆元に使って計算しています。

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,divを参考に式の変形。
    • modnMml, expnM, mulnCとかは式の変形につかったLemmaです。
    • 式変形に必要なLemmaはgrepで調べました。
  4. 変形した式にフェルマーの小定理(ex5のところ)を適用。

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

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暗号の復号で戻る証明ができました。

参考資料

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
2