Commit 66ccc0e4 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

started adding euf-cma axiom support

removed lots of useless env arguments
parent 4d4889b5
Pipeline #1670 passed with stage
in 1 minute and 29 seconds
This diff is collapsed.
......@@ -136,7 +136,7 @@ let init_cca_constraints key_pairs =
encryptions = [];
decryptions = [] };;
let test_cca_case env cca_fun_name cca_fun cca_constraints
let test_cca_case cca_fun_name cca_fun cca_constraints
left_term right_term axiom_res =
let expect_success = match axiom_res with
| Success _ -> true
......@@ -154,12 +154,12 @@ let test_cca_case env cca_fun_name cca_fun cca_constraints
Printf.eprintf "\n ~ \n";
Term.print_term_stderr env right_term;);
match cca_fun env cca_constraints left_term right_term with
match cca_fun cca_constraints left_term right_term with
| exception (Case_fail hint) ->
print_result "\nCCA2 Failed (1st)";
assert (hint_same_shape axiom_res (Failure_hint hint))
| const -> match cca_fun env const left_term right_term with
| const -> match cca_fun const left_term right_term with
| exception (Case_fail hint) ->
print_result "\nCCA2 Failed (2st)";
assert (hint_same_shape axiom_res (Failure_hint hint))
......@@ -167,10 +167,10 @@ let test_cca_case env cca_fun_name cca_fun cca_constraints
| const -> print_result "\nCCA2 Success"; assert (expect_success);;
let test_dec_oracle_call =
fun x -> test_cca_case env "decryption oracle" Cca.dec_oracle_call_case x
fun x -> test_cca_case "decryption oracle" Cca.dec_oracle_call_case x
let test_enc_oracle_call =
fun x -> test_cca_case env "encryption oracle" Cca.enc_oracle_call_case x
fun x -> test_cca_case "encryption oracle" Cca.enc_oracle_call_case x
let unit_test_decryption_oracle = fun () ->
(* 0: Simple decryptions (Success). *)
......
......@@ -807,44 +807,44 @@ let env_remove_binding env s =
(********************)
(* subterm env s t : Return true iff s is a subterm of t in env *)
let rec subterm : type a b. env -> a term -> b term -> bool =
fun env s t -> match get_sort s, get_sort t with
let rec subterm : type a b. a term -> b term -> bool =
fun s t -> match get_sort s, get_sort t with
| Msg,Msg ->
if t_equal s t then
true
else
aux_subterm env s t
aux_subterm s t
| Bool,Bool ->
if t_equal s t then
true
else
aux_subterm env s t
aux_subterm s t
| _ -> aux_subterm env s t
| _ -> aux_subterm s t
and aux_subterm : type a b. env -> a term -> b term -> bool =
fun env s t -> match t.content with
| True -> false
| False -> false
| Name _ -> false
and aux_subterm : type a b. a term -> b term -> bool =
fun s t -> match t.content with
| True -> false
| False -> false
| Name _ -> false
| EQ (u,v) -> (subterm env s u) || (subterm env s v)
| EQ (u,v) -> (subterm s u) || (subterm s v)
| If (b,u,v) -> (subterm env s b) || (subterm env s u) || (subterm env s v)
| If (b,u,v) -> (subterm s b) || (subterm s u) || (subterm s v)
| Fun (_,l) -> List.exists (subterm env s) l
| Fun (_,l) -> List.exists (subterm s) l
(* Type of auxilliary function in all_subterms definition. *)
type ('a,'b) all_subterm_partial_type = 'a term -> 'b sort ->
('b term -> bool) -> ('b term -> bool) -> 'b term list -> 'b term list
(* all_subterms env a sort f : Return every subterms x of a of sort 'sort' such
(* all_subterms env a sort f g : Return every subterms x of a of sort 'sort' such
that f x holds and g y does not hold for every ancestor y of x (including x).
Can contain duplicates. *)
let all_subterms : type a b. env -> a term -> b sort ->
(b term -> bool) -> (b term -> bool) -> b term list = fun env a sort f g ->
let all_subterms : type a b. a term -> b sort ->
(b term -> bool) -> (b term -> bool) -> b term list = fun a sort f g ->
let add_if_conds : type a b. (a,b) all_subterm_partial_type =
fun x sort f g acc -> match get_sort x, sort with
......@@ -901,7 +901,7 @@ let all_subterms : type a b. env -> a term -> b sort ->
(* constrained_subterm env s t t_list : Return true iff s is a subterm of t, but
not in a term of t_list. *)
let const_subterm env (s : msg term) (t : msg term) (t_list : msg term list) =
let const_subterm (s : msg term) (t : msg term) (t_list : msg term list) =
let rec cst : type a. a term -> bool =
fun t -> match get_sort t with
......
......@@ -202,17 +202,17 @@ val env_remove_binding : env -> variable_string -> env
(********************)
(* subterm env s t : Return true iff s is a subterm of t in env *)
val subterm : env -> 'a term -> 'b term -> bool
val subterm : 'a term -> 'b term -> bool
(* all_subterms env a sort f : Return every subterms x of a of sort 'sort' such
that f x holds and g y does not hold for every ancestor y of x (including x).
Can contain duplicates. *)
val all_subterms : env -> 'a term -> 'b sort -> ('b term -> bool)
val all_subterms : 'a term -> 'b sort -> ('b term -> bool)
-> ('b term -> bool) -> 'b term list
(* constrained_subterm env s t t_list : Return true iff s is a subterm of t, but
not in a term of t_list. *)
val const_subterm : env -> msg term -> msg term -> msg term list
val const_subterm : msg term -> msg term -> msg term list
-> bool
......
......@@ -92,9 +92,8 @@ let name_alpha_equal : type a.
of sort 'sort' under the constraints alpha_const. Raise Alpha_conflict _
if they are not alpha-equal, and new_constraints if they are alpha-equal
under new_constraints (which extend alpha_const). *)
let rec alpha_rename :
type a. env -> alpha_const -> a term -> a term -> alpha_const =
fun env alpha_const t t' ->
let rec alpha_rename : type a. alpha_const -> a term -> a term -> alpha_const =
fun alpha_const t t' ->
match t.content, t'.content with
| True,True -> alpha_const
| False,False -> alpha_const
......@@ -107,17 +106,17 @@ let rec alpha_rename :
| Fun (s,l), Fun (s',l') when s = s' ->
List.fold_left2
(fun acc_alpha_const u u' -> alpha_rename env acc_alpha_const u u')
(fun acc_alpha_const u u' -> alpha_rename acc_alpha_const u u')
alpha_const l l'
| If (b, u, v), If (b', u', v') ->
let new_alpha_const = alpha_rename env alpha_const b b' in
let new_alpha_const' = alpha_rename env new_alpha_const u u' in
alpha_rename env new_alpha_const' v v'
let new_alpha_const = alpha_rename alpha_const b b' in
let new_alpha_const' = alpha_rename new_alpha_const u u' in
alpha_rename new_alpha_const' v v'
| EQ (u, v), EQ (u', v') ->
begin
let new_alpha_const = alpha_rename env alpha_const u u' in
alpha_rename env new_alpha_const v v'
let new_alpha_const = alpha_rename alpha_const u u' in
alpha_rename new_alpha_const v v'
end
| _ -> raise Shape_no_match
......@@ -26,5 +26,4 @@ val name_alpha_equal : alpha_const -> name_string -> name_string -> 'a sort
-> alpha_const
(* Raises Shape_no_match if the terms are not alpha-equal. *)
val alpha_rename : env -> alpha_const -> 'a term -> 'a term
-> alpha_const
val alpha_rename : alpha_const -> 'a term -> 'a term -> alpha_const
This diff is collapsed.
......@@ -36,40 +36,38 @@ val print_cca_constraints : env -> Format.formatter -> cca_constraints -> unit
(* CCA2 Cases *)
(**************)
(* subterm_encryptions enc t n: Return the list of encryptions under key sk(n)
(* subterm_encryptions t n: Return the list of encryptions under key sk(n)
appearing in the term t, in the environment env. *)
val subterm_encryptions :
env -> 'a term -> name_string -> msg term list
val subterm_encryptions : 'a term -> name_string -> msg term list
exception Case_fail of cca axiom_hint
(* Return the message and the key used in a decryption oracle call.
Return None if the shape of the term is wrong. *)
val get_m_dec_oracle : env -> msg term
-> (msg term * name_string) option
val get_m_dec_oracle : msg term -> (msg term * name_string) option
(* enc_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
(* enc_oracle_call_case cca_constraints t t' : Check whether t \sim t'
is a valid encryption oracle call. *)
val enc_oracle_call_case : env -> cca_constraints
-> 'a term -> 'a term -> cca_constraints
val enc_oracle_call_case : cca_constraints -> 'a term -> 'a term
-> cca_constraints
exception Contexts_do_not_exist
(* equal_up_to_oracle_calls env cca_constraints t t' : Return true iff t and t'
(* equal_up_to_oracle_calls cca_constraints t t' : Return true iff t and t'
are syntactically equal up-to encryption and decryption oracle calls. *)
val equal_up_to_oracle_calls : env -> cca_constraints -> msg term
-> msg term -> bool
val equal_up_to_oracle_calls : cca_constraints -> msg term -> msg term
-> bool
(* equal_up_to_oracle_calls_strict env cca_constraints t t' : Like the function
(* equal_up_to_oracle_calls_strict cca_constraints t t' : Like the function
equal_up_to_oracle_calls, with the extra constraint that the context does not
contain secret key material. *)
val equal_up_to_oracle_calls_strict : env -> cca_constraints -> msg term
-> msg term -> bool
val equal_up_to_oracle_calls_strict : cca_constraints -> msg term -> msg term
-> bool
(* dec_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
(* dec_oracle_call_case cca_constraints t t' : Check whether t \sim t'
is a valid decryption oracle call. *)
val dec_oracle_call_case : env -> cca_constraints
-> 'a term -> 'a term -> cca_constraints
val dec_oracle_call_case : cca_constraints -> 'a term -> 'a term
-> cca_constraints
(*************)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment