Merge pull request #12 from Barkhausen-Institut/rsa-signatures

Rsa signatures

Makefile.coq.conf

@@ -0,0 +1,71 @@
+# This configuration file was generated by running:
+# coq_makefile -f _CoqProject -o Makefile.coq
+
+COQBIN?=
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+endif
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_CMDLINE_VFILES := 
+COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
+COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
+COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
+COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES))
+COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES))
+COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES))
+COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES))
+COQMF_METAFILE = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = 
+COQMF_SRC_SUBDIRS = 
+COQMF_COQLIBS =  -Q theories vRATLS 
+COQMF_COQLIBS_NOML = -Q theories vRATLS 
+COQMF_CMDLINE_COQLIBS =   
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_COQLIB=/nix/store/51fqh0dc78ggqqy0vp6hhkq242jprpqf-coq-8.18.0/lib/coq/
+COQMF_COQCORELIB=/nix/store/51fqh0dc78ggqqy0vp6hhkq242jprpqf-coq-8.18.0/lib/coq/../coq-core/
+COQMF_DOCDIR=/nix/store/51fqh0dc78ggqqy0vp6hhkq242jprpqf-coq-8.18.0/share/doc/
+COQMF_OCAMLFIND=/nix/store/jfhjb6dlfsyvybzrcr432d7hlvpqngvv-ocaml4.14.2-findlib-1.9.6/bin/ocamlfind
+COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
+COQMF_WARN=-warn-error +a-3
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
+COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Native compiler.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_COQPROJECTNATIVEFLAG = 
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = vRATLS

theories/examples/Conversions.v

@@ -54,7 +54,6 @@ Proof.
   rewrite /intoZp'/fromZp => x.
   rewrite /eq_rect_r/eq_rect //=.
   case: x => m m_lt_p //=.
-  Check Zp_cast.
   case: (Zp_cast (p:=p) p_gt1); rewrite /Zp_trunc => Zp_eq_p //=.
   Fail rewrite Zp_eq_p.
 Abort.
@@ -73,10 +72,6 @@ Definition intoZp'' (q:nat) : 'I_q.+2 -> 'Z_q.+2 := fun x => x.
 Definition z (q:nat) : 'Z_q -> 'Z_q.-2.+2 := fun x => x.
 Definition y (q:nat) : 'Z_q -> 'I_q.-2.+2 := fun x => x.
 
-Check False_rect.
-Check False_rec.
-Check Bool.diff_false_true.
-
 (* This fails because it requires a rewrite of [H]. *)
 Fail Definition into (q:nat) (H: (1 < q)%N) : 'I_q -> 'I_q.-2.+2 :=
   match q with
@@ -90,16 +85,12 @@ Definition into {q:nat} : (1 < q)%N -> 'I_q -> 'I_q.-2.+2 :=
   | _ => fun H => False_rect _ (Bool.diff_false_true H)
   end.
 
-Print into.
-
 Definition into' {q:nat} : (1 < q)%N -> 'I_q -> 'I_q.-2.+2.
 Proof.
   case: q => //=.
   case => //=.
 Defined.
 
-Print into'.
-
 Definition into'' {q:nat} : (1 < q)%N -> 'I_q -> 'I_q.-2.+2.
 Proof.
   case: q.
@@ -109,8 +100,6 @@ Proof.
     + move => n H. exact id.
 Defined.
 
-Print into''.
-
 (** Lesson learned
     Creating functions with tactics results in really complex terms.
     Those are hard to handle when using these functions in lemmas.

theories/examples/More_props.v

@@ -0,0 +1,132 @@
+From Relational Require Import OrderEnrichedCategory GenericRulesSimple.
+
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From mathcomp Require Import all_ssreflect all_algebra reals distr realsum
+  fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum
+  eqtype choice seq.
+Set Warnings "notation-overridden,ambiguous-paths".
+
+From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings
+  UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb
+  pkg_core_definition choice_type pkg_composition pkg_rhl
+  Package Prelude RandomOracle.
+
+From Coq Require Import Utf8.
+From extructures Require Import ord fset fmap.
+
+From Equations Require Import Equations.
+Require Equations.Prop.DepElim.
+Require Import Coq.Init.Logic.
+Require Import List.
+
+Set Equations With UIP.
+
+(*
+The paper:
+https://web.archive.org/web/20220121005133id_/https://eprint.iacr.org/2019/779.pdf
+*)
+
+(*
+  This is needed to make definitions with Equations transparent.
+  Otherwise they are opaque and code simplifications in the
+  proofs with [ssprove_code_simpl] does not resolve properly.
+ *)
+Set Equations Transparent.
+
+Set Bullet Behavior "Strict Subproofs".
+Set Default Goal Selector "!".
+Set Primitive Projections.
+
+Import Num.Def.
+Import Num.Theory.
+Import Order.POrderTheory.
+
+From vRATLS Require Import examples.Signature.
+
+Import PackageNotation.
+
+Obligation Tactic := idtac.
+
+
+Print Run_aux.
+
+(* TODO new run function needed: [evalState] *)
+Fail Theorem CEO seed :
+  forall pk sk,
+    Some (pk,sk) = Run sampler KeyGen seed ->
+    forall msg sig,
+      Some sig = Run_aux sampler (Sign msg) (λ l, if l == sk_loc then Some sk else Some NSUnit) ->
+      forall pk',
+        Some true = Run_aux sampler (Verify sig msg) (λ l, if l == pk_loc then Some pk' else Some NSUnit) ->
+        pk = pk'.
+
+Fail Definition Sign_me : package Sig_locs_real Sig_ifce Sig_prot_ifce
+  := [package
+        #def  #[sign_me] (msg : 'message) : 'pubkey × 'signature
+        {
+           #import {sig #[get_pk] : 'unit → 'pubkey } as get_pk ;;
+           #import {sig #[sign] : 'message → 'signature  } as sign ;;
+
+           pk ← get_pk tt ;;
+           sig ← sign msg ;;
+
+           ret (pk, sig)
+        }
+  ].
+
+Fail Definition Verify_me : package Sig_locs_real Sig_ifce Sig_prot_ifce
+  := [package
+        #def  #[verify_me] (sig : 'signature) (msg : 'message) : 'pubkey × 'bool
+        {
+           #import {sig #[get_pk] : 'unit → 'pubkey } as get_pk ;;
+           #import {sig #[sign] : 'message → 'signature  } as sign ;;
+
+           pk ← get_pk tt ;;
+           b ← verify msg sig ;;
+           ret (pk, b)
+        }
+  ].
+
+
+Fail Theorem CEO seed seed':
+  forall pk pk' msg sig,
+    Some (pk , sig ) = Run sampler (Sign_me msg)       seed ->
+    Some (pk', true) = Run sampler (Verify_me sig msg) seed ->
+    pk = pk'.
+
+(* The below version holds for [KeyGen] implementations
+   that dependent on the seed.
+   That is, we need an additional property for [KeyGen]:
+   [
+     Some pk  = Run sampler KeyGen seed  ->
+     Some pk' = Run sampler KeyGen seed' ->
+     seed = seed' ->
+     pk = pk'
+   ]
+ *)
+Fail Theorem CEO' seed seed':
+  forall pk pk' msg sig,
+    Some (pk , sig ) = Run sampler (Sign_me msg)       seed  ->
+    Some (pk', true) = Run sampler (Verify_me sig msg) seed' ->
+    pk = pk' ->
+    seed = seed'.
+(*
+  The proof is by case on [seed == seed'].
+  The [true] case is straight-forward.
+  The [false] case leads to a contradiction in the hypotheses because
+  then [pk = pk'] does not hold anymore.
+ *)
+
+
+Fail Theorem DEO seed seed':
+  forall pk pk' msg msg' sig,
+    Some (pk, sig ) = Run sampler (Sign_me msg)        seed  ->
+    Some (pk, true) = Run sampler (Verify_me sig msg') seed' ->
+    seed != seed' ->
+    pk = pk' ∧ msg = msg'.
+
+Theorem Consistency_verify:
+  forall pk seed sig msg r r',
+    Some (pk, r ) = Run sampler (Verify_me sig msg) seed' ->
+    Some (pk, r') = Run sampler (Verify_me sig msg) seed' ->
+    r = r'.