(** Contents :

   0: General House Keeping

   1: Syntax definitions 

   2: Equality, membership and extraction functions for the syntax
      2A: Equality functions
      2B: Membership functions
      2C: Extraction of submembers functions


   3: Substitution

   4: Ground terms and rules instances

   5: Tamarin Reduction

   6: Example

   7: Definitions from Chapter 5 of the thesis


   8: Tests and Definitions for Well formedness 
       8A: Functions to test no or One Input / Output in facts
       8B: Definitions on Variables and Terms  for Equivalence proof 
       8C: Well formedness definitions 
       
    9: Some useful lemmas on well formedness

   10: Definitions from Chapter 6 of the thesis
      10A: Types of Facts allowed in the system  

   11: Props and Theorems from Chapter 6 

**)


Load Sec0_UtilityFunctions.
 
(** ============================
       1: Syntax definitions 
    ===========================**)

(*These are the domains of terms, I think this can probabaly be improved **)

Definition freshNameSetup : Type := string.  (* fr from tamarin *) 
Definition freshNameProto : Type := string.  (* fr from tamarin *)

Definition sidTerm : Type := string. (* Session ID*)

Definition publicName : Type := string.  (* pub from tamarin *)

Inductive name : Type := 
  | Fresh_S : freshNameSetup -> name 
  | Fresh_P : freshNameProto -> name
  | Pub     : publicName     -> name.

Definition n : string := "n".
Definition x : string := "x".

Definition names : Type := list name.

Definition variable : Type := string.
Definition variables : Type := list variable.

Inductive baseTerm : Type := 
  | Var   : variable -> baseTerm
  | Name  : name -> baseTerm.

Definition baseTerms : Type := list baseTerm.

Definition func_name : Type := string.

Inductive term : Type :=
  | Func  : func_name -> list baseTerm -> term
  | Bterm : baseTerm -> term.

Definition terms : Type := list term.


Inductive tpair: Type :=
  | pair : term -> term -> tpair
  | emptypair : tpair.

Definition tpairs : Type := list tpair.
(** Action Label with facts (values) *)

Inductive actionLabel : Type :=
  | ActLabel : name -> terms -> actionLabel. (** I'm not sure if this should be name, of some over kind *)

(** Label with facts : List of Action Label with facts (values) *)

(*
Def2,2 in the paper adds optional logs into labels
We model this by replacing labels as lists of action labels: Definition label : Type := list actionLabel.
with two subtypes for labels i.e., labels with logs, and labels without logs. 
*)

Inductive label : Type :=
 | BasicLabel     : list actionLabel -> label
 | LoggedLabel    : actionLabel -> list actionLabel -> label
 | LoggedSIDLabel : baseTerm -> actionLabel -> list actionLabel -> label.

Definition emptyLabel := (BasicLabel []).

Inductive fact : Type :=
  | IN    : terms -> fact   (** An input **)
  | OUT   : terms -> fact   (** An output **)  
  | K     : terms -> fact   (** Attacker knowledge *)
  | STATE : name -> terms -> fact(** General protocol state informtaion. I'm not sure if this should be name, or some over kind kind of identifier*)
  | FR_P  : baseTerm -> fact.   (** A new fresh name in protocol stage**)

Definition facts : Type := list fact.

(** A rule is a triple : pattern followed by Label followed by patterns *)

Definition trace : Type := list label.

Inductive rule : Type :=
  | RuleSetup : facts -> label -> facts -> rule
  | RuleProto : facts -> label -> facts -> rule.

(* A protocol is modelled as a list of these rules:*)
(** A ruleList : List of rule *)
Definition ruleList : Type := list rule.