Commit 4d4889b5 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

added mli files and re-organised src

parent fdb1f1e1
Pipeline #1667 passed with stage
in 2 minutes and 11 seconds
S src
S src/unitary
B _build/src
B _build/src/unitary
PKG ANSITerminal fmt
\ No newline at end of file
<src/unitary>: include
true: use_menhir, explain
true: bin_annot
true: debug
\ No newline at end of file
......@@ -146,7 +146,7 @@ let print_axiom_success : type a. Format.formatter -> a axiom_success -> unit =
| Decryption -> pf ppf "Dec"
let print_res_hint : type a. env -> Format.formatter -> axiom_result -> unit =
let print_res_hint : env -> Format.formatter -> axiom_result -> unit =
fun env ppf res ->
let open Fmt in
let ident ppf s = pf ppf "%s" s in
......
open Term
open Side
open Fmt
type cca
type _ axiom_type =
| CCA : cca axiom_type
type name_string_pair = name_string * name_string
type msg_pair = msg term * msg term
(* Unitary axiom feedback hint. *)
type _ axiom_hint =
| No_cca_hint : cca axiom_hint
(* Guard_problem (enc_pairs,l_superfl,r_superfl) : Error with the
decryption guards:
- enc_pairs : encryption oracle calls (u,v) are not guarded on one side.
- guards for encryptions x_superfl should not be on side 'x'. *)
| Guard_problem : msg_pair list * msg term list
* msg term list -> cca axiom_hint
(* Encryption randomness appearing in two encryptions on 'side'. *)
| Bad_randomness_twice : msg_pair * side -> cca axiom_hint
(* Encryption randomness badly used on 'side'. *)
| Bad_randomness : name_string * side -> cca axiom_hint
(* Cipher key randomness badly used on 'side'. *)
| Bad_key_randomness : name_string * side -> cca axiom_hint
(* Secret key badly used on 'side' (e.g. sk(n) appearing outside a decryption
dec(_,.)). *)
| Bad_secret_key : name_string * side -> cca axiom_hint
(* Bad decryption. *)
| Bad_decryption : msg term * side -> cca axiom_hint
(* No_alpha_renaming (n,n') (s,s') : There is a alpha-renaming constraint
(n,n'), and a conflict with (s,s'). *)
| 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_success -> axiom_result
| Failure_hint : _ axiom_hint -> axiom_result
| Failure : _ axiom_type -> axiom_result
| Unset : axiom_result
(*****************)
(* Miscellaneous *)
(*****************)
val hint_type : 'a axiom_hint -> 'a axiom_type
val hint_same_shape : axiom_result -> axiom_result -> bool
(*******************)
(* Pretty Printing *)
(*******************)
val print_axiom_hint : env -> Format.formatter -> 'a axiom_hint -> unit
val print_axiom_success : Format.formatter -> 'a axiom_success -> unit
val print_res_hint : env -> Format.formatter -> axiom_result -> unit
val debug : (unit -> 'a) -> 'a
val interactive_proof : State.state list -> unit
......@@ -130,8 +130,7 @@ let env =
:: [("nB_0", TName)] )
let init_cca_constraints key_pairs =
{ alpha = { msg_constraints = key_pairs;
bool_constraints = [] };
{ alpha = Alpha.new_alpha key_pairs;
key_pairs = key_pairs;
encryption_rands = [];
encryptions = [];
......
module Mem (M:Hashtbl.HashedType) : sig
val make : (M.t -> 'a) -> M.t -> 'a
val make2 : ('b -> M.t -> 'a) -> 'b -> M.t -> 'a
end
......@@ -11,8 +11,7 @@ type param =
{ shell_mode : bool;
force_color : bool;
small_size_heuristic : int;
mutable input_channel : in_channel;
}
input_channel : in_channel }
let new_emacs_param force_color =
......
(* 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.
- force_color: force color using ANSI codes, in the case automatic detection
of color support of the terminal failed.
- small_size_heuristic: heuristic constant used to decide to apply the
IfThen rule to EQ(t,s) when s is of small size (rewriting occurrences of t
into s in the then branch).
- input_channel: channel used to receive the proof instructions *)
type param =
{ shell_mode : bool;
force_color : bool;
small_size_heuristic : int;
input_channel : in_channel }
val new_emacs_param : bool -> param
val new_proof_param : string -> param
val new_shell_param : bool -> param
all:
@make -C ../.. $@
%:
@make -C ../.. $@
open Term
open Axiom_result
open Side
(* Alpha-renaming constraints:
- msg_constraints: list of Msg Names that are alpha-equal.
- bool_constraints: list of Bool Names that are alpha-equal. *)
type alpha_const =
{ msg_constraints : name_string_pair list;
bool_constraints : name_string_pair list }
(*****************)
(* Miscellaneous *)
(*****************)
(* Prints the alpha-renaming constraints in stderr. *)
let print_alpha_constraints env ppf alpha =
let open Fmt in
let ident = fun ppf s -> pf ppf "%s" s in
pf ppf "@[<v>%a @[<h>%a@]@;%a @[<h>%a@]@]"
(styled `Bold ident) "Msg constraints :"
(list
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
(print_term env) (t_name l Msg)
(print_term env) (t_name r Msg)))
alpha.msg_constraints
(styled `Bold ident) "Bool constraints : "
(list
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
(print_term env) (t_name l Msg)
(print_term env) (t_name r Msg)))
alpha.bool_constraints;;
let new_alpha key_pairs = { msg_constraints = key_pairs;
bool_constraints = [] }
(****************************)
(* Alpha Renaming Functions *)
(****************************)
(* Alpha_conflict (n,n') (s,s') : Raised when there is a alpha-renaming
constraint (n,n'), and a conflict with (s,s'). *)
exception Alpha_conflict of
(name_string * name_string) * (name_string * name_string)
exception Shape_no_match
(* name_alpha_equal alpha_const n n' sort: try to alpha-rename the names n and
n' 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 name_alpha_equal : type a.
alpha_const -> name_string -> name_string -> a sort -> alpha_const =
fun alpha_const n n' sort ->
let constraints = match sort with
| Bool -> alpha_const.bool_constraints
| Msg -> alpha_const.msg_constraints in
if List.mem (n,n') constraints then
(* The constraint already exists. *)
alpha_const
else if List.exists (fun (x,y) -> (x = n) || (y =n')) constraints then
(* An incompatible constraint already exists. *)
let a_const = List.find (fun (x,y) -> (x = n) || (y =n')) constraints in
raise (Alpha_conflict (a_const,(n,n')))
else match sort with
(* We add the constraint (n,n') to the corresponding list. *)
| Bool ->
{ msg_constraints = alpha_const.msg_constraints;
bool_constraints = (n,n') :: alpha_const.bool_constraints }
| Msg ->
{ msg_constraints = (n,n') :: alpha_const.msg_constraints;
bool_constraints = alpha_const.bool_constraints }
(* alpha_rename alpha_const t t': try to alpha-rename the terms t and t' t'
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' ->
match t.content, t'.content with
| True,True -> alpha_const
| False,False -> alpha_const
| Name (s,sort), Name (s',sort') ->
if sort = sort' then
name_alpha_equal alpha_const s s' sort
else
raise Shape_no_match
| 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')
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'
| 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'
end
| _ -> raise Shape_no_match
open Term
open Axiom_result
open Side
(* Alpha-renaming constraints:
- msg_constraints: list of Msg Names that are alpha-equal.
- bool_constraints: list of Bool Names that are alpha-equal. *)
type alpha_const
(* Alpha_conflict (n,n') (s,s') : Raised when there is a alpha-renaming
constraint (n,n'), and a conflict with (s,s'). *)
exception Alpha_conflict of
(name_string * name_string) * (name_string * name_string)
exception Shape_no_match
val print_alpha_constraints : env -> Format.formatter -> alpha_const -> unit
val new_alpha : name_string_pair list -> alpha_const
(* name_alpha_equal alpha_const n n' sort: try to alpha-rename the names n and
n' 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). *)
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
......@@ -2,19 +2,13 @@ open Term
open Formula
open Axiom_result
open Side
open Alpha
(* General comment: the algorithm we use builds all the constraints
simultaneously while doing a pass through the list of term pairs. Therefore,
two passes must be done. The first pass get new constraints, and the second
pass checks that all constraints are satisfied. *)
(* Alpha-renaming constraints:
- msg_constraints: list of Msg Names that are alpha-equal.
- bool_constraints: list of Bool Names that are alpha-equal. *)
type alpha_const =
{ msg_constraints : name_string_pair list;
bool_constraints : name_string_pair list }
(* CCA2 constraints:
- alpha: alpha-renaming constraints.
- left_key_list: list of randomness used in the key pairs on the left.
......@@ -42,35 +36,10 @@ let update_alpha cca_constraints alpha_const =
exception Case_fail of cca axiom_hint
(*****************)
(* Miscellaneous *)
(*****************)
(* Prints the alpha-renaming constraints in stderr. *)
let print_alpha_constraints env ppf alpha =
let open Fmt in
let ident = fun ppf s -> pf ppf "%s" s in
pf ppf "@[<v>%a @[<h>%a@]@;%a @[<h>%a@]@]"
(styled `Bold ident) "Msg constraints :"
(list
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
(print_term env) (t_name l Msg)
(print_term env) (t_name r Msg)))
alpha.msg_constraints
(styled `Bold ident) "Bool constraints : "
(list
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
(print_term env) (t_name l Msg)
(print_term env) (t_name r Msg)))
alpha.bool_constraints;;
(*******************)
(* Pretty Printing *)
(*******************)
let print_cca_constraints_aux env long ppf constraints =
let open Fmt in
......@@ -125,85 +94,6 @@ let print_cca_constraints env ppf constraints =
let print_cca_constraints_long env ppf constraints =
print_cca_constraints_aux env true ppf constraints
(****************************)
(* Alpha Renaming Functions *)
(****************************)
(* Alpha_conflict (n,n') (s,s') : Raised when there is a alpha-renaming
constraint (n,n'), and a conflict with (s,s'). *)
exception Alpha_conflict of
(name_string * name_string) * (name_string * name_string)
exception Shape_no_match
(* name_alpha_equal alpha_const n n' sort: try to alpha-rename the names n and
n' 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 name_alpha_equal : type a.
alpha_const -> name_string -> name_string -> a sort -> alpha_const =
fun alpha_const n n' sort ->
let constraints = match sort with
| Bool -> alpha_const.bool_constraints
| Msg -> alpha_const.msg_constraints in
if List.mem (n,n') constraints then
(* The constraint already exists. *)
alpha_const
else if List.exists (fun (x,y) -> (x = n) || (y =n')) constraints then
(* An incompatible constraint already exists. *)
let a_const = List.find (fun (x,y) -> (x = n) || (y =n')) constraints in
raise (Alpha_conflict (a_const,(n,n')))
else match sort with
(* We add the constraint (n,n') to the corresponding list. *)
| Bool ->
{ msg_constraints = alpha_const.msg_constraints;
bool_constraints = (n,n') :: alpha_const.bool_constraints }
| Msg ->
{ msg_constraints = (n,n') :: alpha_const.msg_constraints;
bool_constraints = alpha_const.bool_constraints }
(* alpha_rename alpha_const t t': try to alpha-rename the terms t and t' t'
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' ->
match t.content, t'.content with
| True,True -> alpha_const
| False,False -> alpha_const
| Name (s,sort), Name (s',sort') ->
if sort = sort' then
name_alpha_equal alpha_const s s' sort
else
raise Shape_no_match
| 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')
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'
| 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'
end
| _ -> raise Shape_no_match
(********************************)
(* CCA2 Axiom : Encryption Case *)
......@@ -1118,8 +1008,7 @@ let rec apply_cca formula option_constraints =
let env = formula.env in
let initial_constraints = match option_constraints with
| None -> { alpha = { msg_constraints = [];
bool_constraints = [] };
| None -> { alpha = new_alpha [];
key_pairs = [];
encryption_rands = [];
encryptions = [];
......
open Term
open Formula
open Axiom_result
open Alpha
(* General comment: the algorithm we use builds all the constraints
simultaneously while doing a pass through the list of term pairs. Therefore,
two passes must be done. The first pass get new constraints, and the second
pass checks that all constraints are satisfied. *)
(* Alpha-renaming constraints:
- msg_constraints: list of Msg Names that are alpha-equal.
- bool_constraints: list of Bool Names that are alpha-equal. *)
type alpha_const =
{ msg_constraints : name_string_pair list;
bool_constraints : name_string_pair list }
(* CCA2 constraints:
- alpha: alpha-renaming constraints.
- left_key_list: list of randomness used in the key pairs on the left.
......@@ -38,20 +32,9 @@ type cca_constraints =
val print_cca_constraints : env -> Format.formatter -> cca_constraints -> unit
(*********************************)
(* Alpha Renaming and CCA2 Cases *)
(*********************************)
(* Alpha_conflict (n,n') (s,s') : Raised when there is a alpha-renaming
constraint (n,n'), and a conflict with (s,s'). *)
exception Alpha_conflict of
(name_string * name_string) * (name_string * name_string)
exception Shape_no_match
(* Raises Shape_no_match if the terms are not alpha-equal. *)
val alpha_rename : env -> alpha_const -> 'a term -> 'a term
-> alpha_const
(**************)
(* CCA2 Cases *)
(**************)
(* subterm_encryptions enc t n: Return the list of encryptions under key sk(n)
appearing in the term t, in the environment env. *)
......
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