Theory Algebraic_Group_Model
theory Algebraic_Group_Model
imports CryptHOL.CryptHOL Restrictive_Comp
keywords
"lift_to_algebraicT" :: thy_decl
begin
section ‹The Algebraic Group Model›
text ‹This theory extends CryptHOL for the Algebraic Group Model according to
Fuchsbauer, Kiltz, and Loss' ``The Algebraic Group Model and its Applications'' \<^cite>‹FKL18›.
Adversaries in CryptHOL are modelled as uninitialized parameters (arbitrary functions), thus we
cannot ensure that the adversary algorithm itself is algebraic. Instead we enforce the algebraic
rules on the outputs of the adversary, counting rule breaking as losing the game. Hence, every
adversary with non-negligible advantage has to be an algebraic algorithm.
We formalize this relaxed notion of an algebraic algorithm as a sub case of Restrictive\_Comp, i.e.
we define the AGM in terms of a RCM.
We provide group specific records groupS and groupC for Select and constrain. Furthermore,
we define some automation and sanity check functions in Isabelle/ML›
context cyclic_group
begin
text ‹group elements are the single important type we want to select.›
definition groupS :: "('a,'a) Select"
where "groupS ≡ ⦇select = (λx. [x])⦈"
text ‹The above definitions can be composed with the existing data structure extensions from
Restrictive\_Comp and should cover a wide range of possible inputs. In case some case is missing,
the Restrictive\_Comp records can be extended to more data structures (see Restrictive\_Comp for
examples) and this locale can be extended for more atomic type definitions.›
text ‹check the rules of an algebraic algorithm i.e. given the elements g, a group element,
and the vector vec=[c\_0,...c\_n] from the algorithm ensure that g=s\_0 [\textasciicircum{}] c\_0 $\otimes$ ... $\otimes$
s\_n [\textasciicircum{}] c\_n, where [s\_0,...,s\_n]=seen are the group values the algorithm was supplied with.
›
definition constrain_grp :: "'a list ⇒ ('a × int list) ⇒ bool"
where "constrain_grp seen_vec res ≡
let (g,c_vec) = res in
(length seen_vec = length c_vec
∧ g = fold (λ i acc. acc ⊗⇘G⇙ seen_vec!i [^]⇘G⇙ (c_vec!i)) [0..<length seen_vec] 𝟭⇘G⇙)"
definition groupC :: "('a, ('a × int list)) Constrain"
where "groupC ≡ ⦇constrain = (λip op. constrain_grp ip op)⦈"
text ‹group values that follow the rules of an algebraic algorithm are actually in the group›
lemma constrain_grp_is_in_carrier:
assumes "∀g ∈ set seen_vec. g ∈ carrier G"
and "constrain_grp seen_vec (g,c_vec)"
shows "g ∈ carrier G"
proof -
have "g = fold (λ i acc. acc ⊗ seen_vec!i [^] (c_vec!i)) [0..<length seen_vec] 𝟭"
using assms(2) constrain_grp_def by auto
also have "length seen_vec = length c_vec"
using assms(2) constrain_grp_def by fastforce
then have "fold (λ i acc. acc ⊗ seen_vec!i [^] (c_vec!i)) [0..<length seen_vec] 𝟭 ∈ carrier G"
using assms(1)
proof (induct seen_vec c_vec rule: rev_induct2)
case (4 x xs y ys)
then have fold_xs_carrier: "fold (λi acc. acc ⊗ xs ! i [^] ys ! i) [0..<length xs] 𝟭 ∈ carrier G"
by fastforce
moreover have "x [^] y ∈ carrier G"
by (simp add: 4(3))
moreover have "fold (λi acc. acc ⊗ (xs @ [x]) ! i [^] (ys @ [y]) ! i) [0..<length (xs @ [x])] 𝟭
= (fold (λi acc. acc ⊗ xs ! i [^] ys ! i) [0..<length xs] 𝟭) ⊗ x [^] y"
proof -
let ?fyys = "λxs::'a list. (λi acc. acc ⊗ xs ! i [^] (ys @ [y]) ! i)"
have "fold (λi acc. acc ⊗ (xs @ [x]) ! i [^] (ys @ [y]) ! i) [0..<length (xs @ [x])] 𝟭
= fold (?fyys (xs@[x])) [0..<length (xs @ [x])] 𝟭" by blast
moreover have "… = (fold (?fyys (xs@[x])) [length (xs @ [x]) - 1] ∘ fold (?fyys (xs@[x])) [0..<length (xs)]) 𝟭"
by auto
moreover have "… = ((λacc. acc ⊗ x [^] y) ∘ fold (?fyys (xs@[x])) [0..<length (xs)]) 𝟭"
by (smt (verit, del_insts) "4"(2) One_nat_def add_Suc_right append.right_neutral diff_Suc_Suc diff_zero fold.simps(1) fold_Cons id_comp
length_append list.size(3,4) nth_append_length o_apply)
moreover have "… = (fold (?fyys (xs@[x])) [0..<length (xs)] 𝟭) ⊗ x [^] y"
by force
moreover have "… = (fold (λi acc. acc ⊗ xs ! i [^] ys ! i) [0..<length (xs)] 𝟭) ⊗ x [^] y"
proof -
have "fold (?fyys (xs@[x])) [0..<length (xs)] 𝟭
= fold (λi acc. acc ⊗ xs ! i [^] ys ! i) [0..<length xs] 𝟭"
proof(rule fold_cong)
fix i
assume "i ∈ set [0..<length xs]"
then have xs_le_xs: "i < length xs"
by force
then have "(xs @ [x]) ! i = xs ! i"
using nth_append_left by blast
moreover have "(ys @ [y]) ! i = ys ! i"
using 4(2) nth_append_left xs_le_xs by auto
ultimately show "(λacc. acc ⊗ (xs @ [x]) ! i [^] (ys @ [y]) ! i) = (λacc. acc ⊗ xs ! i [^] ys ! i)"
by presburger
qed force+
then show ?thesis by presburger
qed
ultimately show ?thesis by argo
qed
ultimately show ?case
by auto
qed force+
finally show "g ∈ carrier G" by blast
qed
end
locale Algebraic_Algorithm = G : cyclic_group G
for G :: "('a, 'b) cyclic_group_scheme" (structure)
+
fixes sel :: "('x,'a) Select"
and con :: "('a,'y) Constrain"
sublocale Algebraic_Algorithm ⊆ Restrictive_Comp sel con .
locale algebraic_algorithm_examples = cyclic_group
begin
text ‹To obtain an algebraic algorithm one needs to simply instantiate the restrictive\_comp locale
with the record composition that one needs and apply the non-algebraic algorithm to the obtained
restrictive\_comp.restrict.›
text‹The trivial example of only one group element as in and output.›
text ‹For simplicity let the adversary be id›
definition 𝒜_id :: "'a ⇒ ('a × int list) spmf"
where "𝒜_id = (λx. return_spmf (x, [1::int]))"
interpretation Algebraic_Algorithm G "groupS" "groupC"
by (unfold_locales)
lemma
assumes "g ∈ carrier G"
shows "restrict 𝒜_id g
= 𝒜_id g"
unfolding 𝒜_id_def Restrictive_Comp.restrict_def
unfolding groupS_def groupC_def constrain_grp_def
by (simp add: assms)
text ‹Now the same for a list of input elements and and output elements›
definition 𝒜_list_fst :: "'a list ⇒ ('a × int list) list spmf"
where "𝒜_list_fst = (λx. return_spmf (map (λ_. (x!0, [1::int,0,0])) x))"
interpretation list_id: Restrictive_Comp "(listS groupS)" "listC groupC" .
lemma
assumes "g1 ∈ carrier G ∧ g2 ∈ carrier G ∧ g3 ∈ carrier G"
shows "list_id.restrict 𝒜_list_fst [g1,g2,g3]
= 𝒜_list_fst [g1,g2,g3]"
unfolding 𝒜_list_fst_def Restrictive_Comp.restrict_def
unfolding listS_def groupS_def listC_def groupC_def
unfolding constrain_grp_def
by (simp add: assms)
text ‹We define some useful ML functions for the AGM.
lift\_to\_algebraicT operates on the type level, lifting standard model function types into their
corresponding type as an algebraic algorithm. I.e. extend the outputs that are group elements
with a vector.
›
text ‹This takes any algorithm/function type and lifts it to the algebraic algorithm equivalent type.
For examples take a look at the end of this file.›
ML ‹
local
fun rcodomain_transf f (Type ("fun", [T, U])) = (Type ("fun", [T, rcodomain_transf f U]))
| rcodomain_transf f T = f T;
fun adjoin t vec = fn T => if T = t then Type ("Product_Type.prod", [T, vec]) else T
fun decurry (Type ("fun", [T1, Type ("fun", [T2, T3])])) =
decurry (Type ("fun", [Type ("Product_Type.prod", [T1, T2]), T3]))
| decurry T = T
fun extract_type_params t = Term.add_tfree_namesT t []
fun lift_to_algebraicT grpT vec = (rcodomain_transf (Term.map_atyps (adjoin grpT vec))) o decurry
in
val _ =
Outer_Syntax.local_theory \<^command_keyword>‹lift_to_algebraicT› "lift to algebraic type"
(Parse.typ -- (Parse.term -- (\<^keyword>‹=>› |--Parse.binding)) >>
(fn (alg,(grp,b)) => fn lthy => Local_Theory.raw_theory (fn thy =>
let
val algT = Syntax.read_typ lthy alg;
val grp_desc = Syntax.read_term lthy grp;
val grpT = Term.fastype_of grp_desc |> Term.dest_Type_args |> hd;
val agmT = lift_to_algebraicT grpT @{typ "int list"} algT;
val tps = extract_type_params agmT;
val thy' = Sign.add_type_abbrev lthy (b, tps, agmT) thy
in thy' end) lthy));
end;
›
subsection ‹Example for the ML function›
text ‹We define a standard model adversary with group ‹G› of type ‹'a››
type_synonym ('a')adv = "'a' list ⇒ 'a' ⇒ nat ⇒ ('a' * int * nat) spmf"
text ‹We lift the type into the AGM (its algebraic algorithm pendant):›
lift_to_algebraicT "('a) adv" "G" => algebraic_adv
end
end