Commit 83d980f6 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

started euf-cma implementation. Not done

parent a876fa3e
Pipeline #1672 passed with stage
in 1 minute and 30 seconds
......@@ -790,6 +790,130 @@ let rec guard_goal_list state g_data_list f sk fk =
fk
(*********************)
(* Euf-CMA Functions *)
(*********************)
exception Bad_euf of string
let euf_get_check_cnt b =
let (m,s,pk) = match b.content with
| EQ (l,r) -> begin match l.content,r.content with
| Fun ("check",[m;s;pk]), Fun ("sigok",[])
| Fun ("sigok",[]), Fun ("check",[m;s;pk]) -> (m,s,pk)
| _ -> raise (Bad_euf "Bad conditional shape") end
| _ -> raise (Bad_euf "Conditional should be of the form EQ(_,_)") in
match pk.content with
| Fun ("pks",[n_s]) -> begin match n_s.content with
| Name (n,Msg) -> (m,s,n)
| _ -> raise (Bad_euf "Bad key name shape") end
| _ -> raise (Bad_euf "Bad key shape")
(* euf_synt_cst n t : Return true iff the euf-cma syntactic constraints for n
holds in t. *)
let rec euf_synt_cst : type a. name_string -> a term -> bool =
fun n t -> match t.content with
| True -> true
| False -> false
| Name (s,_) ->
if s = n then
false
else
true
| Fun ("pks", [pk]) -> begin match pk.content with
| Name (_,Msg) -> true
| _ -> euf_synt_cst n pk end
| Fun ("sign", [m;sk]) -> begin match sk.content with
| Fun ("sks", [sk_name]) -> begin match sk_name.content with
| Name (_,Msg) -> true
| _ -> List.for_all (euf_synt_cst n) [m;sk] end
| _ -> List.for_all (euf_synt_cst n) [m;sk] end
| Fun (_,l) -> List.for_all (euf_synt_cst n) l
| If (b,u,v) -> (euf_synt_cst n b)
&& (euf_synt_cst n u)
&& (euf_synt_cst n v)
| EQ (u,v) -> (euf_synt_cst n u)
&& (euf_synt_cst n v)
(* euf_make_guard_side b : Build a guard_data_side element for b. Raise
Bad_euf if some side conditions of the Euf-CMA axiom do not hold. *)
let euf_make_guard_side b =
let (m,s,n) = euf_get_check_cnt b in
if not (euf_synt_cst n b) then
raise (Bad_euf "Syntactic conditions do not hold");
let is_sign t = match t.content with
| Fun ("sign",[m;sk]) -> begin match sk.content with
| Fun ("sks",[n']) -> t_equal n' (t_name n Msg)
| _ -> false end
| _ -> false in
let sigs = all_subterms b Msg is_sign (fun _ -> false) in
let honest_sigs = List.map (fun t -> match t.content with
| Fun ("sign",[m;_]) -> m
| _ -> assert false) sigs in
let uniq_honest_sigs = List.sort_uniq t_compare honest_sigs in
(* We compute the g_data_side element *)
let g_data_side =
{ term = b;
term_content = m;
honest_list = uniq_honest_sigs;
guarded_term = t_false () } in
g_data_side
(* euf_need_to_guard env t t' g_data : Return true iff g_data_side needs to be
applied to t. *)
let euf_need_to_guard t t' g_data =
(subterm g_data.left_guard.term t)
|| (subterm g_data.right_guard.term t')
(* auto_guard state sk fk : Try to guard all decryption pairs possible. *)
let euf_auto_guard side b state sk fk =
let goal = state.c_proof.goal in
let env = goal.env in
try
let g_data_side = euf_make_guard_side b in
let state = add_error_fun (fun () ->
let open Fmt in
pf stdout "@[<v>Guarding %a in %a.@; Adding guards for the following \
signatures:@;@[<v 0>%a@]@;@]%!"
(print_term env) g_data_side.term_content
(print_term env) g_data_side.term
(list ~sep:(fun ppf () -> pf ppf "@;")
(print_term env))
g_data_side.honest_list) state in
let sk' state fk = sk (simplify state) fk in
(* TODO : this should be done similarly to cca_auto_guard_data!
get the matching pairs of check(_),check(_), deduce a list of g_data,
apply etc ..*)
assert false
with
| Bad_euf s -> sk (add_error ("Bad Euf : " ^ s) state) fk
(*****************)
(* CCA Functions *)
(*****************)
......@@ -1637,7 +1761,35 @@ add_c_action
);;
add_c_action
"euf guard"
(fun ppf () -> pr_name ppf "cca2")
(fun ppf () -> Fmt.pf ppf "applies the cca2 axiom")
default_exn_handler
(fun y state sk fk -> Scanf.sscanf y "%s %s@!"
(fun side_s u ->
match parse_b_terms state u with
| [b] ->
let side =
if String.contains side_s 'l' then
Left
else if String.contains side_s 'r' then
Right
else
raise Bad_argument in
tact_andthen (euf_auto_guard side b) try_cca sk fk state
| l ->
raise (Term_badly_formed
(Printf.sprintf
"Wanted to parse 1 boolean term and got %d"
(List.length l))))
);;
......
......@@ -14,6 +14,7 @@ type rule =
| If_intro of boole term * boole term
| CS of boole term * boole term
| Cond_fresh of side * boole term
| Euf of side * boole term
exception Bad_rule of string * rule
exception Rule_not_applicable
......@@ -46,6 +47,9 @@ let rule_to_string r = match r with
| Cond_fresh (side,_) ->
Printf.sprintf "Cond_fresh %s" (side_to_string side)
| Euf (side,_) ->
Printf.sprintf "Euf %s" (side_to_string side)
let print_rule_long : env -> Format.formatter -> rule -> unit =
fun env ppf r ->
let open Fmt in
......@@ -82,6 +86,10 @@ let print_rule_long : env -> Format.formatter -> rule -> unit =
(side_to_string side)
(print_term env) b
| Euf (side,b) ->
pf ppf "%s Euf %a"
(side_to_string side)
(print_term env) b
(* new_formula_element ancestor term_pair : Create a new formula element for
term_pair, inheriting some attributes from ancestor. *)
......@@ -354,6 +362,7 @@ let rule_apply formula r (t, t') = match r with
| Restr -> failwith "rule_apply: no possible Restr here"
| Euf (side,b) -> assert false
(* Apply the rule r to boolean terms (b,b'),
and return a list with the new terms *)
......@@ -383,6 +392,7 @@ let rule_b_apply formula r (b,b') = match r with
| Restr -> failwith "rule_apply: no possible Restr here"
| Euf (side,b) -> assert false
(*********************)
(* Rule Applications *)
......
......@@ -13,7 +13,7 @@ type rule =
| If_intro of boole term * boole term
| CS of boole term * boole term
| Cond_fresh of side * boole term
| Euf of side * boole term
exception Bad_rule of string * rule
exception Rule_not_applicable
......
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