Commit 5e23731c authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

corrected a bug when computing the set of encryptions that need to be guarded

parent 705d7b54
Pipeline #1639 failed with stage
in 19 seconds
......@@ -444,7 +444,11 @@ let subterm_encryptions :
| Fun (s,l) -> List.fold_left aux acc l
| If (b,u,v) -> aux (aux (aux acc v) u) b
| EQ (u,v) -> aux (aux acc v) u
| _ -> acc in
| Var _ -> assert false
| Name _ -> acc
| True -> acc
| False -> acc
| Bot -> acc in
List.sort_uniq Pervasives.compare (aux [] t)
......@@ -560,9 +564,15 @@ let get_missing_superfl_guards env cca_const side t =
| None -> assert false
| Some (m,sk) ->
(* We compute the list of encryption oracle calls appearing in m. *)
let (left_encs,right_encs) = List.split cca_const.encryptions in
let side_encs = match side with
| Left -> left_encs
| Right -> right_encs in
let subterm_enc_calls =
List.filter
(fun x -> list_mem_side side x cca_const.encryptions)
(fun x -> List.exists (syntactic_equal env x) side_encs)
(subterm_encryptions env m sk)
(* We compute the list of encryptions appearing in guards. *)
......@@ -715,18 +725,6 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
let (c,c') = build_ctxt t t' in
let test = match t,t' with
| Var ("dec__0",Msg),Var ("dec__0",Msg) -> true
| _ -> false in
if test then
begin
Fmt.pf Fmt.stderr "@[<v>@[%a@]@;@]%!" (* @;@[%a@]@;@[%a@] *)
print_cca_constraints_long (!current_cca_constraints)
(* print_term c *)
(* print_term c' *)
end;
(c,c',!current_cca_constraints)
......@@ -1015,7 +1013,7 @@ let extend_cca_dec_case env constraints t t' =
(* get_keys acc env t : Return the set of keys appearing in t @ acc. *)
let rec get_keys : type a. name_string list -> environement -> a term
-> name_string list = fun acc env t ->
match eiv env t with
match eiv_i env t 2 with
| False -> acc
| True -> acc
| Bot -> acc
......@@ -1076,16 +1074,16 @@ let rec apply_cca formula option_constraints =
type a. a term -> a term -> (cca_constraints * axiom_result list) =
fun t t' -> try match enc_oracle_call_case env cca_const t t' with
| cca_const ->
(cca_const, Success CCA :: res_list)
(cca_const, Success Encryption :: res_list)
| exception (Case_fail (No_cca_hint)) ->
match dec_oracle_call_case env cca_const t t' with
| cca_const ->
(cca_const, Success CCA :: res_list)
(cca_const, Success Decryption :: res_list)
| exception (Case_fail (No_cca_hint)) ->
let cca_const = symmetrical_part_case env cca_const t t' in
(cca_const, Success CCA :: res_list)
(cca_const, Success Symmetric :: res_list)
with
| Case_fail (No_cca_hint) ->
......
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