Skip to content

Key schedule security proofs -- fork #144

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 10 commits into from
Closed

Key schedule security proofs -- fork #144

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
291243a
Fixing proofs
cmester0 Feb 12, 2025
453aef8
Re-index key packages, so GET is prev and SET is next
cmester0 Feb 19, 2025
9f4be82
Back to core theorem
cmester0 Feb 20, 2025
6f50450
Fixed structure all the way through
cmester0 Feb 21, 2025
2a109ea
Core package finally defined
cmester0 Feb 25, 2025
a53ad00
Most of setup done for core theorem
cmester0 Mar 3, 2025
4a3b513
Core theorem fully stated, missing lemmas and package definitions
cmester0 Mar 4, 2025
5eee2e9
Move definitions to Core.v
cmester0 Mar 11, 2025
6c4093d
Last couple of sub-theorem remain of core theorem
cmester0 Mar 17, 2025
7b24520
Another sub-theorem (d6) done
cmester0 Mar 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions proofs/ssprove/_CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,12 @@

# PROOF

./handwritten/ssp_helper.v

./handwritten/Types.v
./handwritten/ExtraTypes.v
./handwritten/Utility.v

./handwritten/ssp_helper.v

./handwritten/Dependencies.v

./handwritten/BasePackages.v
Expand All @@ -39,10 +39,12 @@

./handwritten/Core.v
./handwritten/KeySchedulePackages.v
./handwritten/MapPackage.v

./handwritten/CoreTheorem.v
# ./handwritten/ModularTheorem.v
./handwritten/MainTheorem.v

./handwritten/BertieResult.v
# ./handwritten/MapPackage.v

# # ./handwritten/ModularTheorem.v
# ./handwritten/MainTheorem.v

# ./handwritten/BertieResult.v
32 changes: 31 additions & 1 deletion proofs/ssprove/handwritten/BasePackages.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,19 @@ Notation " 'chHASHinp' " :=
Notation " 'chHASHout' " :=
(bitvec)
(in custom pack_type at level 2).
Definition HASH := 1%nat.
(* Definition HASH := 1%nat. *)

Inductive HashFunction :=
| f_hash
| f_xtr
| f_xpd.

Definition HASH (f : HashFunction) : nat :=
22%nat + match f with
| f_hash => 0
| f_xtr => 1
| f_xpd => 2
end.

Notation " 'chUNQinp' " :=
(chHandle × 'bool × chKey)
Expand Down Expand Up @@ -124,3 +136,21 @@ Notation " 'chDHEXPout' " :=
Definition DHEXP : nat := 12.

(* Definition SET_DH : nat := 13. *)

(* Definition SET_ℓ_f d n ℓ := [interface #val #[ SET n ℓ d ] : chSETinp → chSETout]. *)

Definition SET_ℓ Names d ℓ : Interface :=
interface_foreach (fun n => [interface #val #[ SET n ℓ d ] : chSETinp → chSETout]) Names.
(* SET_ℓ_f d n ℓ *)

Definition SET_n Names d k : Interface :=
interface_hierarchy (SET_ℓ Names k) d.

(* Definition GET_ℓ_f d n ℓ := [interface #val #[ GET n ℓ d ] : chGETinp → chGETout]. *)

Definition GET_ℓ Names d ℓ : Interface :=
interface_foreach (fun n => [interface #val #[ GET n ℓ d ] : chGETinp → chGETout]) Names.
(* GET_ℓ_f d n ℓ *)

Definition GET_n Names d k : Interface :=
interface_hierarchy (GET_ℓ Names k) d.
20 changes: 14 additions & 6 deletions proofs/ssprove/handwritten/BertieResult.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -275,6 +275,10 @@ Section BertieKeySchedule.
Definition Bertie_K_table : chHandle -> nat. Admitted.
Definition Bertie_in_K_table : forall x, ('option chK_table; Bertie_K_table x) \in Bertie_L_K. Admitted.

Definition Bertie_L_L : {fset Location}. Admitted.
Definition Bertie_L_table : chHandle -> nat. Admitted.
Definition Bertie_in_L_table : forall x, ('option chL_table; Bertie_L_table x) \in Bertie_L_L. Admitted.

Definition Bertie_L_M : {fset Location}. Admitted.
Definition Bertie_M : chHandle -> nat. Admitted.
Definition Bertie_H : name → ∀ s : chHandle, ('option ('fin #|fin_handle|); Bertie_M s) \in Bertie_L_M. Admitted.
Expand All @@ -284,7 +288,7 @@ Section BertieKeySchedule.

End BertieKeySchedule.

Instance BertieKeySchedule (d : nat) : Dependencies :=
(* Program *) Instance BertieKeySchedule (d : nat) : Dependencies :=
(* Proof. *)
(* econstructor. *)
(* - refine (Bertie_PrntN). *)
Expand All @@ -304,9 +308,9 @@ Instance BertieKeySchedule (d : nat) : Dependencies :=
(* - refine (Bertie_DHEXP_function). *)

{
PrntN := Bertie_PrntN;
(* PrntN := Bertie_PrntN; *)
Labels := Bertie_Labels ;

xpd := Bertie_xpd ;
xtr := Bertie_xtr ;
xtr_angle := Bertie_xtr_angle ;
Expand All @@ -315,6 +319,10 @@ Instance BertieKeySchedule (d : nat) : Dependencies :=
ord := Bertie_ord ;
E := Bertie_E ;

L_L := Bertie_L_L ;
L_table := Bertie_L_table ;
in_L_table := Bertie_in_L_table ;

L_K := Bertie_L_K ;
K_table := Bertie_K_table ;
in_K_table := Bertie_in_K_table ;
Expand All @@ -329,6 +337,6 @@ Instance BertieKeySchedule (d : nat) : Dependencies :=
DHEXP_function := Bertie_DHEXP_function ;
}.

Definition BertieKeyScheduleCoreSimulator (d : nat) : Simulator (DepInstance := BertieKeySchedule d). Admitted.
Definition BertieKeyScheduleCoreTheorem (d : nat) :=
core_theorem (DepInstance := BertieKeySchedule d) (BertieKeyScheduleCoreSimulator d).
Definition BertieKeyScheduleCoreSimulator (d k : nat) : Simulator d k. Admitted.
Definition BertieKeyScheduleCoreTheorem (d k : nat) (H_lt : (d < k)%nat) :=
core_theorem (DepInstance := BertieKeySchedule d) d k H_lt (BertieKeyScheduleCoreSimulator d k).
Loading
Loading