Commit deb4468e authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

- corrected a bug in term.ml: pseudo normalization was badly done, variables...

- corrected a bug in term.ml: pseudo normalization was badly done, variables must be collected in terms at each loop itaration to guarrantee that conditianal have a unique representation
- axiom_result type has been extended to include, in case of success, the information about was rule was used (symmetrical, encryption, decryption_
parent 048ada9b
Pipeline #1641 passed with stage
in 1 minute and 53 seconds
let VoterA sksig v pk =
let VoterA sks v pk =
new r.
let ballot = enc(v,r,pk) in
out(ca, <ballot,sign(ballot, sksig)>);
out(ca, <ballot,sign(ballot, sks)>);
let VoterB sksig v pk =
let VoterB sks v pk =
new r.
let ballot = enc(v,r,pk) in
out(cb, <ballot,sign(ballot, sksig)>);
out(cb, <ballot,sign(ballot, sks)>);
let Outcome v1 v2 v3 sk =
if EQ(v1,v2) then
......@@ -25,27 +24,36 @@ let Outcome v1 v2 v3 sk =
out(cres,<acount,bcount>);
let SubTally{i} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
let SubTally{i} v1 v2 v3 bv1 bv2 pks1 pks2 pks3 sk =
in(c, x).
if EQ(checksig(pi1(x),pi2(x),pksig1),sigok()) then
(SubTally{i-1}
(pi1(x)) v2 v3
(A()) bv2
pksig1 pksig2 pksig3 sk)
else if EQ(checksig(pi1(x),pi2(x),pksig2),sigok()) then
(SubTally{i-1}
v1 (pi1(x)) v3
bv1 (B())
pksig1 pksig2 pksig3 sk)
else if EQ(checksig(pi1(x),pi2(x),pksig3),sigok()) then
(SubTally{i-1}
v1 v2 (pi1(x))
bv1 bv2
pksig1 pksig2 pksig3 sk)
let v1p =
if EQ(check(pi1(x),pi2(x),pks1),sigok()) then
(pi1(x))
else
v1 in
let v2p =
if EQ(check(pi1(x),pi2(x),pks2),sigok()) then
(pi1(x))
else
v2 in
let v3p =
if EQ(check(pi1(x),pi2(x),pks3),sigok()) then
(pi1(x))
else
v3 in
let bv1p =
if EQ(check(pi1(x),pi2(x),pks1),sigok()) then
(A())
else
bv1 in
let bv2p =
if EQ(check(pi1(x),pi2(x),pks2),sigok()) then
(B())
else
(SubTally{i-1} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk);
bv2 in
SubTally{i-1} v1p v2p v3p bv1p bv2p pks1 pks2 pks3 sk;
let SubTally{0} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
let SubTally{0} v1 v2 v3 bv1 bv2 pks1 pks2 pks3 sk =
if EQ(bv1,A()) then
(if EQ(bv2,B()) then
(Outcome v1 v2 v3 sk)
......@@ -59,22 +67,22 @@ let P vc1 vc2 =
let pk = pk(n) in
let sk = sk(n) in
out(cinit,pk).
new nksig1.
new nksig2.
new nksig3.
let sksig1 = sksig(nksig1) in
let pksig1 = pksig(nksig1) in
out(cinit,pksig1).
let sksig2 = sksig(nksig2) in
let pksig2 = pksig(nksig2) in
out(cinit,pksig2).
let sksig3 = sksig(nksig3) in
let pksig3 = pksig(nksig3) in
out(cinit,pksig3).
new nks1.
new nks2.
new nks3.
let sks1 = sks(nks1) in
let pks1 = pks(nks1) in
out(cinit,pks1).
let sks2 = sks(nks2) in
let pks2 = pks(nks2) in
out(cinit,pks2).
let sks3 = sks(nks3) in
let pks3 = pks(nks3) in
out(cinit,pks3).
out(cinit,sksig3).
out(cinit,sks3).
((VoterA sksig1 vc1 pk) | (VoterB sksig2 vc2 pk)
| (SubTally{1} (N()) (N()) (N()) (C()) (C()) pksig1 pksig2 pksig3 sk));
((VoterA sks1 vc1 pk) | (VoterB sks2 vc2 pk)
| (SubTally{3} (N()) (N()) (N()) (C()) (C()) pks1 pks2 pks3 sk));
goal: P (A()) (B()) ~ P (B()) (A())
......@@ -36,13 +36,19 @@ type _ axiom_hint =
| No_alpha_renaming : name_string_pair *
name_string_pair -> cca axiom_hint
(* Unitary axiom feedback. *)
type _ axiom_success =
| Symmetric : cca axiom_success
| Encryption : cca axiom_success
| Decryption : cca axiom_success
(* Used to give feedback when trying to apply an unitary axiom:
- Success : sucessful application on this term.
- Failure_hint : failure with an indication to guide the proof search.
- Failure : failure without indication
- Unset : indicates that no feedback information exists for this term. *)
type axiom_result =
| Success : _ axiom_type -> axiom_result
| Success : _ axiom_success -> axiom_result
| Failure_hint : _ axiom_hint -> axiom_result
| Failure : _ axiom_type -> axiom_result
| Unset : axiom_result
......@@ -133,6 +139,13 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit =
pf ppf "Alpha-renaming conflict between (%s,%s) and (%s,%s)" n n' s s'
let print_axiom_success : type a. Format.formatter -> a axiom_success -> unit =
fun ppf ax_suc -> match ax_suc with
| Symmetric -> pf ppf "Sym"
| Encryption -> pf ppf "Enc"
| Decryption -> pf ppf "Dec"
let print_res_hint : type a. Format.formatter -> axiom_result -> unit =
fun ppf res ->
let open Fmt in
......@@ -140,6 +153,6 @@ let print_res_hint : type a. Format.formatter -> axiom_result -> unit =
match res with
| Unset -> assert false
| Success _ -> ident ppf "Success"
| Success ax_suc -> pf ppf "Success %a" print_axiom_success ax_suc
| Failure _ -> ident ppf "Failure"
| Failure_hint hint -> print_axiom_hint ppf hint
......@@ -327,7 +327,7 @@ let add_t_binding formula ?(collect = !default_collect) s t =
env'.bt_bindings;
Hashtbl.add env'.t_bindings s t;
Hashtbl.add env'.hide_bindings s false;
Hashtbl.add env'.hide_bindings s true;
let f' = List.map (fun entry ->
match entry.term_pair with
......@@ -373,7 +373,7 @@ let add_bt_binding formula ?(collect = !default_collect) s bt =
Hashtbl.add env'.bt_bindings s bt;
Hashtbl.add env'.hide_bindings s false;
Hashtbl.add env'.hide_bindings s true;
let f' = List.map (fun entry ->
match entry.term_pair with
......
......@@ -1698,7 +1698,9 @@ let pre_treatment state =
pf stderr "\n%!"
end;
let bool_res = apply_unitary_and_set_feedback state CCA in
let bool_res = apply_unitary_and_set_feedback ~print:true state CCA in
new_screen state;
if bool_res then
begin
state.c_proof.premises <- PAxiom CCA;
......@@ -2157,7 +2159,7 @@ let auto_guard state =
(* We try to add them to the current partial CCA application *)
let get_cca_res env constr t t' =
match dec_oracle_call_case env constr t t' with
| constr' -> Success CCA
| constr' -> Success Decryption
| exception (Case_fail No_cca_hint) -> Failure CCA
......@@ -2357,10 +2359,12 @@ let interactive_proof state =
with
| End_of_file ->
printf "Incorrect proof.\n"
in
printf "Incorrect proof.\n" in
try
ignore(apply_unitary_and_set_feedback ~print:true state CCA);
new_screen state;
pre_treatment state;
interactive_loop state
with
......
......@@ -135,7 +135,9 @@ let init_cca_constraints key_pairs =
let test_cca_case cca_fun_name cca_fun cca_constraints
left_term right_term axiom_res =
let expect_success = axiom_res = Success CCA in
let expect_success = match axiom_res with
| Success _ -> true
| _ -> false in
let print_result s =
debug (fun () -> if expect_success then
......@@ -152,10 +154,12 @@ let test_cca_case cca_fun_name cca_fun cca_constraints
| 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
| exception (Case_fail hint) ->
print_result "\nCCA2 Failed (2st)";
assert (hint_same_shape axiom_res (Failure_hint hint))
| const -> print_result "\nCCA2 Success"; assert (expect_success);;
let test_dec_oracle_call =
......@@ -207,24 +211,25 @@ let unit_test_decryption_oracle = fun () ->
dec_4; decp_4; dec_5; decp_5] ->
let const =
init_cca_constraints [("kA","kA_0"); ("kB","kB_0")] in
let dummy_suc = Success Symmetric in
test_dec_oracle_call
const dec_0 decp_0 (Success CCA);
const dec_0 decp_0 dummy_suc;
test_dec_oracle_call
const dec_1 decp_1 (Success CCA);
const dec_1 decp_1 dummy_suc;
test_dec_oracle_call
const dec_2 decp_2 (Failure_hint (Guard_problem ([],[],[])));
test_dec_oracle_call
const dec_3 decp_3 (Success CCA);
const dec_3 decp_3 dummy_suc;
test_dec_oracle_call
const dec_4 decp_4 (Failure_hint (No_alpha_renaming (("",""),("",""))));
test_dec_oracle_call
const dec_5 decp_5 (Success CCA);
const dec_5 decp_5 dummy_suc;
| _ -> assert (false);;
......@@ -260,15 +265,16 @@ let unit_test_encryption_oracle = fun () ->
enc_4; encp_4 ] ->
let const =
init_cca_constraints [("kA","kA_0"); ("kB","kB_0")] in
let dummy_suc = Success Symmetric in
test_enc_oracle_call
const enc_0 encp_0 (Success CCA);
const enc_0 encp_0 dummy_suc;
test_enc_oracle_call
const enc_1 encp_1 (Success CCA);
const enc_1 encp_1 dummy_suc;
test_enc_oracle_call
const enc_2 encp_2 (Success CCA);
const enc_2 encp_2 dummy_suc;
test_enc_oracle_call
const enc_3 encp_3 (Failure_hint (Bad_randomness ("",Left)));
......
......@@ -2,7 +2,6 @@
(* The parameters of the interactive loop state:
- shell_mode: if true, use the input box and history in the interactive
loop input. Set to false when used with emacs.
- hide_bindings: if true, prints the bindings at each interactive step.
- default_collect: if true, try to do automatic collection when adding
new bindings to the environement.
- force_color: force color using ANSI codes, in the case automatic detection
......
......@@ -413,13 +413,16 @@ let ireduce env map_fresh side gp_list =
| Loop (_,i) ->
let l_args = get_args (get_decl s) in
List.map2 (fun t arg ->
let (var, map_fresh') =
fresh_name env map_fresh side arg TVar in
List.map2 (fun t arg -> match t with
| Var _ -> t
Hashtbl.add env.t_bindings var t;
Hashtbl.add env.hide_bindings var false;
Var (var,Msg))
| _ ->
let (var, map_fresh') =
fresh_name env map_fresh side arg TVar in
Hashtbl.add env.t_bindings var t;
Hashtbl.add env.hide_bindings var true;
Var (var,Msg))
l l_args
| _ -> l in
......@@ -442,17 +445,6 @@ let ireduce env map_fresh side gp_list =
map_fresh
((g, p') :: (g, p'') :: acc_gp_list')
| g, Let (s, t, p') ->
let (var, map_fresh') = fresh_name env map_fresh side s TVar in
Hashtbl.add env.t_bindings var t;
Hashtbl.add env.hide_bindings var false;
aux_ireduce
reduced_gp_list
map_fresh'
((g, process_subst s (Var (var,Msg)) p') :: acc_gp_list')
| g, IfThenElse (b, p', p'') ->
aux_ireduce
reduced_gp_list
......@@ -463,7 +455,25 @@ let ireduce env map_fresh side gp_list =
aux_ireduce
(gp :: reduced_gp_list)
map_fresh
acc_gp_list' in
acc_gp_list'
| g, Let (s, t, p') -> match collect_all env t with
| Var _ ->
aux_ireduce
reduced_gp_list
map_fresh
((g, process_subst s t p') :: acc_gp_list')
| _ ->
let (var, map_fresh') = fresh_name env map_fresh side s TVar in
Hashtbl.add env.t_bindings var t;
Hashtbl.add env.hide_bindings var true;
aux_ireduce
reduced_gp_list
map_fresh'
((g, process_subst s (Var (var,Msg)) p') :: acc_gp_list') in
aux_ireduce [] map_fresh gp_list
......@@ -792,20 +802,25 @@ let rec i_tree_size = function
(* Transform an If-tree into a term by keeping only the last element of
each frame. *)
let rec term_from_itree itree = match itree with
| Node (g, i1, i2) -> term_from_guard g i1 i2
let rec term_from_itree env itree = match itree with
| Node (g, i1, i2) ->
let t1 = term_from_itree env i1
and t2 = term_from_itree env i2 in
term_from_guard env g t1 t2
| Leave t -> t
and term_from_guard g i1 i2 = match g with
| NilGuard -> term_from_itree i1
| Guard b -> If (b, term_from_itree i1, term_from_itree i2)
| NGuard b -> If (b, term_from_itree i2, term_from_itree i1)
and term_from_guard env g t1 t2 = match g with
| NilGuard -> t1
| Guard b -> If (b, t1, t2)
| NGuard b -> If (b, t2, t1)
| Conj (b, g2) ->
If (b, term_from_guard g2 i1 i2, term_from_itree i2)
If (b, term_from_guard env g2 t1 t2, t2)
| NConj (b, g2) ->
If (b, term_from_itree i2, term_from_guard g2 i1 i2)
If (b, t2, term_from_guard env g2 t1 t2)
(* Sort a list of actions using the lexicographical order on (x,c) where
x \in \{AIn,AOut\} and c is the (inputting or outputting) channel name
......@@ -866,7 +881,7 @@ let get_adv_term configuration env map_fresh side s =
let (var,map_fresh') = fresh_name env map_fresh side s TVar in
Hashtbl.add env.t_bindings var adv_term;
Hashtbl.add env.hide_bindings var false;
Hashtbl.add env.hide_bindings var true;
let adv_term_var = Var (var,Msg) in
......@@ -925,7 +940,7 @@ let apply_action action configuration env map_fresh side =
([], Leave (Fun ("silence",[])), map_fresh)
sorted_gp_list in
let outputed_term = term_from_itree itree in
let outputed_term = term_from_itree env itree in
(* We weakly normalize the outputed term. *)
let norm_outputed_term =
......@@ -939,7 +954,7 @@ let apply_action action configuration env map_fresh side =
let term_phi' = Fun ("pair", [configuration.phi; norm_outputed_term]) in
Hashtbl.add env.t_bindings var_phi' term_phi';
Hashtbl.add env.hide_bindings var_phi' false;
Hashtbl.add env.hide_bindings var_phi' true;
let phi' = Var (var_phi',Msg) in
......@@ -1010,7 +1025,6 @@ let fold_protocol env left_process right_process =
else
let rec aux left_configuration right_configuration env map_fresh =
Printf.eprintf "1\n\n%!";
if (configuration_is_empty left_configuration)
&& (configuration_is_empty right_configuration) then
let left_frame_reversed = left_configuration.frame
......
......@@ -25,12 +25,22 @@ type _ term =
let enc u r pk = Fun("enc",[u;Name (r,Msg);Fun ("pk",[Name (pk,Msg)])])
and ite b u v = If (b,u,v)
and dec u sk = Fun("dec",[u;Fun ("sk",[Name (sk,Msg)])])
and pair a b = Fun("pair",[a;b])
and sk s = Fun("sk",[Name (s,Msg)])
and pk s = Fun("pk",[Name (s,Msg)])
and eq a b = EQ(a,b)
and name r = Name (r,Msg)
and var r = Var (r,Msg)
and cst a = Fun(a,[])
......@@ -1368,7 +1378,8 @@ let pseudo_normalize : type a. environement -> a term -> a term = fun env t ->
(* x_conds is a list of if-free, simply normalized, Sym-ordered
conditionals that have already been pulled. *)
let rec ps_aux pos_conds neg_conds t =
let wn_t = weak_normalize env t in
let wn_t = weak_normalize env t
|> collect_all env in
let to_pull_candidates = select_if_free_conds env wn_t in
......@@ -1418,12 +1429,28 @@ let pseudo_normalize : type a. environement -> a term -> a term = fun env t ->
let r_equal : type a. environement -> a term -> a term -> bool =
fun env t t' ->
let test = (* match get_sort t' with *)
(* | Msg -> syntactic_equal env t' *)
(* TODO *)
(* | _ -> false *) false in
let nt = pseudo_normalize env t
and nt' = pseudo_normalize env t' in
let cond_nt = conds env nt
and cond_nt' = conds env nt' in
debug (fun () -> if test then
begin
let open Fmt in
pf stderr "r_equal debug :@?@[<v 0>@;@[%a@]@;\
@[%a@]@;@[%a@]@;@[%a@]@;@]%!"
print_term t
print_term nt
print_term t'
print_term nt'
end;);
if cond_nt <> cond_nt' then
false
else
......
(* First trace *)
hide bind *;
cca2 guard;
cca2 guard;
......@@ -9,8 +7,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(nA_l,A());
cond_fresh Right EQ(nA_r,A());
cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
......@@ -23,8 +21,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi1(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi1(mb_r)),nB_r);
cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
......@@ -37,8 +35,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi1(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi1(mb_r)),nB_r);
cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
......@@ -46,22 +44,40 @@ cond_fresh Right EQ(dec__0,nB_r);
cca2;
(* Second trace *)
hide bind *;
cca2 guard;
cond_fresh Left EQ(nA_l,A());
cond_fresh Right EQ(nA_r,A());
cca2;
cca2 guard;
cca2 guard;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cca2;
cca2 guard;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi1(dec_ma_l)),nB_l);
cond_fresh Right EQ(pi1(pi1(dec_ma_r)),nB_r);
cond_fresh Left EQ(pi1(pi2(dec_mb_l_1)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_mb_r_1)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cca2;
cca2 guard;
cca2 guard;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
......@@ -74,22 +90,29 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi1(dec_mb_l_0)),nB_l);
cond_fresh Right EQ(pi1(pi1(dec_mb_r_0)),nB_r);
cond_fresh Left EQ(pi1(pi2(dec_mb_l_0)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_mb_r_0)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cca2;
(* Third trace *)
hide bind *;
cca2 guard;
cca2 guard;
cond_fresh Left EQ(nA_l,A());
cond_fresh Right EQ(nA_r,A());
cca2;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2 guard;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cca2 guard;
cca2 guard;
......
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