More than 5 years have passed since last update.
Elgamal暗号でSSReflectのトライアル
6
Last updated at Posted at 2018-02-04
目的
CoqのSSReflectの入門・演習として、Elgamal暗号の証明します。環境構築、定式化、証明を順に行います。
Elgamal暗号の本定式化はまったく高速ではありませんし、未だにSSReflectを使いこなせていませんので内容についてご了承ください。
RSAの証明のブログを参考に作っています。作成した証明はこちらです。
環境構築
今回windowsで行った。手順は下記であるが、注意点はmath-compが要求するcoqのバージョンを確認してインストールします。
単純に最新版をいれるとバージョンの不一致が起こり動作しないです。
- math-compをインストール
- coqのリリース一覧から上記のmath-compの要求するバージョン（今回は8.7.0）をインストール
参考までに、linuxならopamを使ったこちらの手順があります。
Elgamal暗号の定式化
Elgamal暗号の暗号化と復号化は下記のように定式化しました。
Wikipediaのものを参考に、逆元はフェルマーの小定理から$p-1$乗が単位元になるので$p-2$乗を逆元に使って計算しています。
SectionElgamal.Variablepg:nat.Variableprime_p:primep.Variableprime_g:primeg.Variablepri:nat.Hypothesispri_lt_p:pri<p.Hypothesisg_lt_p:g<p.Variabler:nat.Hypothesisr_lt_p:r<p.Definitionpub:=(g^pri)%%p.Definitionenc1:=g^r%%p.Definitionenc2(m:nat):=(pub^r*m)%%p.Definitiondec(e1:nat)(e2:nat):=e2*((e1^(p-2))^pri)%%p.Theoremelgamal_correct1:forallw:nat,w<p->decenc1(enc2w)=w%[modp].Proof.Admitted.EndElgamal.証明の構築のながれ
証明は下記のように行いました。
- math-compのライブラリのオイラーの定理を元にフェルマーの小定理を構築
- RSAの証明のブログのほぼコピペ
- 上記のelgamal_correct1の定理のdec,enc1,enc2をすべて展開。
- SSReflectのlemmaのssrnat,divを参考に式の変形。
- modnMml, expnM, mulnCとかは式の変形につかったLemmaです。
- 式変形に必要なLemmaはgrepで調べました。
- 変形した式にフェルマーの小定理(ex5のところ)を適用。
下記は実際のコードです。
Lemmaex1:(g^pri%%p)^r=g^(pri*r)%[modp].Proof.byrewritemodnXmexpnM.Qed.Lemmaex2:(g^r%%p)^((p-2)*pri)=g^(r*(p-2)*pri)%[modp].Proof.rewritemodnXm!expnM//.Qed.Lemmaex3:pri*r*(p-2)+pri*r=pri*r*(p-1).Proof.rewrite-{2}[pri*r]muln1.rewrite-mulnDr.havepluslemma:(p-2)+1=p-1.-rewriteaddn1.applysubnSK.byrewriteprime_gt1.rewritepluslemma//.Qed.Lemmaphi_prime:forallx,primex->totientx=x.-1.Proof.move=>x;move/totient_pfactor;move/(__(ltn0Sn0)).byrewriteexpn1expn0muln1.Qed.Lemmagp_coprime:coprimegp.Proof.rewriteprime_coprime//.rewritedvdn_prime2//.rewriteneq_ltn.rewriteg_lt_p.by[].Qed.Lemmaex5:g^(p-1)%%p=1.Proof.rewritesubn1.rewrite-phi_prime.rewriteEuler_exp_totient.-rewritemodn_small//.-rewriteprime_gt1//.-rewritegp_coprime//.-rewriteprime_p//.Qed.Theoremelgamal_correct1:forallw:nat,w<p->decenc1(enc2w)=w%[modp].Proof.move=>ww_le_p.rewrite/dec.rewritemodn_mod.rewrite/enc1/enc2/pub.rewritemodnMml.rewrite-expnM.rewrite-modnMm.rewrite-[((g^pri%%p)^r*w)%%p]modnMm.rewriteex1.rewrite[(g^(pri*r)%%p*(w%%p))%%p]modnMm.rewriteex2.rewritemodnMm.rewritemulnC.rewritemulnA.rewrite-expnD.rewrite-[_*pri]mulnC.rewrite[pri*_]mulnA.rewriteex3.rewrite-[pri*r*(p-1)]mulnCexpnM.rewrite-modnMml.rewrite-modnXm.rewriteex5.rewriteexp1n.rewritemodnMml.rewritemul1n.by[].Qed.まとめ
Coqの初心者なので、証明の良し悪しもわからないですが、SSReflectとmath-compを使ってなんとかElgamal暗号の復号で戻る証明ができました。
参考資料
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme