diff --git a/src/display.ml b/src/display.ml
index 8f19c22..3b68a77 100644
--- a/src/display.ml
+++ b/src/display.ml
@@ -866,6 +866,7 @@ let display_rule_num ((hyp,concl,hist,constra) as rule) =
 	    Rn _ -> print_string "(The attacker can create new names.)"
 	  | Init -> print_string "(Initial knowledge of the attacker.)"
 	  | PhaseChange -> print_string "(Knowledge is communicated from one phase to the next.)"
+	  | FuturePhaseChange -> print_string "(Channel messages are retained in the future.)"
 	  | TblPhaseChange -> print_string "(Tables are communicated from one phase to the next.)"
 	  | Apply(Func(f),p) ->
 	      print_string "(The attacker applies function ";
@@ -1477,6 +1478,26 @@ let display_attacker_fact = function
       print_string ") in off-line phase"
   | _ -> Parsing_helper.internal_error "Unexpected attacker fact"
 
+let display_message_fact = function
+    Pred({p_info = [Mess(n,_)]}, [vc;vm]) ->
+      WithLinks.term vm;
+      print_string " from channel ";
+      WithLinks.term vc;
+      if n > 0 then 
+	print_string (" in phase " ^ (string_of_int n))
+  | Pred({p_info = [MessBin(n,_)]}, [vc;vm;vc';vm']) ->
+      WithLinks.term vm;
+      print_string " (resp. ";
+      WithLinks.term vm';
+      print_string ") from channel ";
+      WithLinks.term vc;
+      print_string " (resp. ";
+      WithLinks.term vc';
+      print_string ")";
+      if n > 0 then 
+	print_string (" in phase " ^ (string_of_int n))
+  | _ -> Parsing_helper.internal_error "Unexpected message fact"
+
 let display_tbl_fact = function
     Pred({p_info = [Table(n)]}, [v]) ->
       WithLinks.term v;
@@ -1536,6 +1557,15 @@ let display_attacker_hyp nl hl =
 	print_string ".";
 	newline()) nl hl
 
+let display_message_hyp nl hl =
+  List.iter2 (fun n h ->
+    display_step n;
+    print_string "the attacker may know ";
+    display_message_fact h.thefact;
+    print_string ".";
+    newline()) nl hl
+  
+
 let display_tbl_hyp nl hl =
   List.iter2 (fun n h ->
     display_step n;
@@ -1754,6 +1784,12 @@ let display_clause_explain n lbl hyp_num_list hl constra concl =
       display_attacker_fact concl;
       print_string ".";
       newline()
+  | FuturePhaseChange ->
+      display_message_hyp hyp_num_list hl;
+      print_string "So the attacker may know ";
+      display_attacker_fact concl;
+      print_string ".";
+      newline()
   | TblPhaseChange -> 
       display_tbl_hyp hyp_num_list hl;
       print_string "So a table may contain the entry ";
diff --git a/src/lexertotex.mll b/src/lexertotex.mll
index 2cecf90..057f05a 100644
--- a/src/lexertotex.mll
+++ b/src/lexertotex.mll
@@ -43,7 +43,7 @@ let init_kinds d =
   List.iter (function
       FunDecl((f,_),_,_) -> Hashtbl.add kinds f "\\kwf"
     | DataFunDecl((f,_),_) -> Hashtbl.add kinds f "\\kwf"
-    | Reduc((((PFunApp((f,_),_) ,_),_)::_),_) -> Hashtbl.add kinds f "\\kwf"
+    | Reduc((((PFunApp((f,_),_) ,_),_)::_),_,_) -> Hashtbl.add kinds f "\\kwf"
     | PredDecl((p,_),_,_) -> Hashtbl.add kinds p "\\kwp"
     | Free(l,_) -> List.iter (fun (c,_) -> Hashtbl.add kinds c "\\kwc") l
     | _ -> ()) d
diff --git a/src/param.ml b/src/param.ml
index b436849..2a9f563 100644
--- a/src/param.ml
+++ b/src/param.ml
@@ -326,6 +326,7 @@ let choice_fun_memo = memo (fun t ->
     f_cat = Choice;
     f_initial_cat = Choice;
     f_private = true;
+    f_phases = [];
     f_options = 0 })
 
 let choice_fun t = 
@@ -340,9 +341,11 @@ let fun_decls = ((Hashtbl.create 49) : (string, funsymb) Hashtbl.t)
 let pred_env = Hashtbl.create 7
 let freenames = ref ([] : funsymb list)
 let max_used_phase = ref 0
+let future_phase = ref None
 let session1 = { f_name = "session1"; 
 		 f_type = [], sid_type;
                  f_private = false;
+                 f_phases = [];
 		 f_options = 0;
 		 f_cat = Eq [];
 	         f_initial_cat = Eq [] }
diff --git a/src/param.mli b/src/param.mli
index 68ab3bb..a18095a 100644
--- a/src/param.mli
+++ b/src/param.mli
@@ -194,6 +194,7 @@ val fun_decls : (string,Types.funsymb) Hashtbl.t
 val pred_env : (string,Types.predicate) Hashtbl.t
 val freenames : Types.funsymb list ref
 val max_used_phase : int ref
+val future_phase : (int * Types.term list) option ref
 val session1 : Types.funsymb
 val red_rules : (Types.fact list * Types.fact * Types.constraints list list * Types.label) list ref
 val elim_true : Types.fact list ref
diff --git a/src/piauth.ml b/src/piauth.ml
index d52d723..93a14a3 100644
--- a/src/piauth.ml
+++ b/src/piauth.ml
@@ -96,6 +96,7 @@ let rec put_constants = function
 				      f_cat = SpecVar v;
 				      f_initial_cat = SpecVar v;
 				      f_private = false;
+				      f_phases = [];
 				      f_options = 0 }, []));
 	    current_bound_vars := v :: (!current_bound_vars)
 	| _ -> internal_error "unexpected link in put_constants"
@@ -452,6 +453,7 @@ let session_id_cst =
   { f_name = "session_id";
     f_type = [], Param.sid_type;
     f_private = false;
+    f_phases = [];
     f_options = 0;
     f_cat = Eq [];
     f_initial_cat = Eq []
@@ -463,6 +465,7 @@ let session_id_cst2 =
   { f_name = "session_id2";
     f_type = [], Param.sid_type;
     f_private = false;
+    f_phases = [];
     f_options = 0;
     f_cat = Eq [];
     f_initial_cat = Eq []
diff --git a/src/pilexer.mll b/src/pilexer.mll
index 99de48a..78652e5 100644
--- a/src/pilexer.mll
+++ b/src/pilexer.mll
@@ -41,6 +41,9 @@ let keyword_table =
 [ "data", DATA;
   "param", PARAM;
   "private", PRIVATE;
+  "with", WITH;
+  "channel", CHANNEL;
+  "future", FUTURE;
 (* Common keywords *)
   "new", NEW;
   "out", OUT;
diff --git a/src/piparser.mly b/src/piparser.mly
index 6f2bb8e..86b8306 100644
--- a/src/piparser.mly
+++ b/src/piparser.mly
@@ -89,6 +89,9 @@ exception Syntax
 %token DATA
 %token PARAM
 %token PRIVATE
+%token FUTURE
+%token WITH
+%token CHANNEL
 
 
 /* Precedence (from low to high) and associativities */
@@ -110,9 +113,13 @@ all:
 |       DATA IDENT SLASH INT DOT all
 	{ (DataFunDecl($2, $4)) :: $6 }
 |	EQUATION term EQUAL term DOT all
-	{ (Equation($2, $4)) :: $6 }
+	{ (Equation(($2, $4), [])) :: $6 }
+|	IN PHASE intseq EQUATION term EQUAL term DOT all
+	{ (Equation(($5, $7), $3)) :: $9 }
 |	privateopt REDUCTION reduc all
-	{ (Reduc($3,$1)) :: $4 }
+	{ (Reduc($3,$1,[])) :: $4 }
+|	IN PHASE intseq privateopt REDUCTION reduc all
+	{ (Reduc($6,$4,$3)) :: $7 }
 |       PREDICATE IDENT SLASH INT neidentseq DOT all
         { (PredDecl($2, $4, $5)) :: $7 }
 |       PREDICATE IDENT SLASH INT DOT all
@@ -143,6 +150,8 @@ all:
         { (Clauses($2)) :: $3 }
 |	PROCESS process EOF
 	{ [Process $2] }
+|	FUTURE PHASE INT WITH CHANNEL negtermseq DOT all
+	{ (Future($3, $6)) :: $8 }
 
 privateopt:
 	PRIVATE
@@ -152,6 +161,12 @@ privateopt:
 
 /* Rewrite rules */
 
+intseq:
+|	INT
+	{ [$1] }
+|	INT COMMA intseq
+	{ $1::$3 }
+
 reduc:
 	term EQUAL term SEMI reduc
 	{ ($1,$3) :: $5 }
diff --git a/src/piptree.mli b/src/piptree.mli
index 9f57dcb..91979ac 100644
--- a/src/piptree.mli
+++ b/src/piptree.mli
@@ -133,8 +133,8 @@ type process =
 type decl = 
     FunDecl of ident * int * bool
   | DataFunDecl of ident * int
-  | Reduc of fundef * bool
-  | Equation of equation
+  | Reduc of fundef * bool (* private? *) * int list (* phases (empty = all) *)
+  | Equation of equation * int list (* phases (empty = all) *)
   | PredDecl of ident * int * ident list
   | Param of ident * Ptree.pval
   | PDef of ident * process
@@ -147,4 +147,5 @@ type decl =
   | Elimtrue of fact_e
   | Free of ident list * bool
   | Clauses of clause list
+  | Future of int (* phase *) * gterm_e list (* channels *)
 
diff --git a/src/pisyntax.ml b/src/pisyntax.ml
index a3111ae..ea55212 100644
--- a/src/pisyntax.ml
+++ b/src/pisyntax.ml
@@ -71,6 +71,7 @@ let create_name s arity is_free =
      f_cat = cat;
      f_initial_cat = cat;
      f_private = not is_free;
+     f_phases = [];
      f_options = 0 }
 
 let create_name_uniq s arity is_free =
@@ -84,6 +85,7 @@ let create_name_uniq s arity is_free =
      f_cat = cat;
      f_initial_cat = cat;
      f_private = not is_free;
+     f_phases = [];
      f_options = 0 }
 
 
@@ -97,6 +99,7 @@ let check_fun_decl is_tuple (name,ext) arity is_private =
       f_cat = cat;
       f_initial_cat = cat;
       f_private = is_private;
+      f_phases = [];
       f_options = 0 }
 
 let get_var env s =
@@ -154,13 +157,13 @@ let rec check_eq_term f_allowed varenv (term,ext) =
       FunApp (Terms.get_tuple_fun (List.map (fun _ -> Param.any_type) tlist), 
               List.map (check_eq_term f_allowed varenv) tlist)
 
-let check_equation (t1, t2) =
+let check_equation (t1, t2) phases =
    let var_env = Hashtbl.create 7 in
    let t1' = check_eq_term f_eq_tuple var_env t1 in
    let t2' = check_eq_term f_eq_tuple var_env t2 in
-   TermsEq.register_equation (t1',t2')
+   TermsEq.register_equation (t1',t2') phases
 
-let check_red tlist is_private =
+let check_red tlist is_private phases =
   match tlist with 
     ((PFunApp((f,ext),l),_),_)::_ ->
       begin 
@@ -196,6 +199,7 @@ let check_red tlist is_private =
         let fsymb = { f_name = f;
                       f_type = (List.map (fun _ -> Param.any_type) l), Param.any_type;
                       f_private = is_private;
+                      f_phases = phases;
 		      f_options = 0;
                       f_cat = cat;
 		      f_initial_cat = cat
@@ -498,6 +502,7 @@ let get_event_fun s arity ext =
 	      f_cat = Eq[]; 
 	      f_initial_cat = Eq[]; 
 	      f_private = true;
+	      f_phases = [];
               f_options = 0 } in
     Hashtbl.add event_fun_table s p;
     p
@@ -596,6 +601,7 @@ let get_non_interf (id, lopt) =
    | Some l -> Some (List.map (check_ni_term (Hashtbl.create 7)) l))
 
 let query_list = ref ([] : Piptree.query list list)
+let future_phase = ref (None : (int * Piptree.gterm_e list) option)
 let need_vars_in_names = Reduction_helper.need_vars_in_names
 let noninterf_list = ref ([] : (funsymb * term list option) list list)
 let not_list = ref ([] : ((Piptree.gfact_e * int) * (Piptree.ident * Piptree.gterm_e) list) list)
@@ -705,11 +711,19 @@ let rec check_all = function
   | (DataFunDecl (f,i))::l -> 
       check_fun_decl true f i false;
       check_all l
-  | (Equation eq)::l ->
-      check_equation eq;
+  | (Equation (eq, phases))::l ->
+      check_equation eq phases;
+      List.iter (fun phase ->
+        if phase > !Param.max_used_phase then
+          Param.max_used_phase := phase
+      ) phases;
       check_all l
-  | (Reduc (r,is_private))::l -> 
-      check_red r is_private; 
+  | (Reduc (r,is_private,phases))::l -> 
+      check_red r is_private phases; 
+      List.iter (fun phase ->
+        if phase > !Param.max_used_phase then
+          Param.max_used_phase := phase
+      ) phases;
       check_all l
   | (PredDecl (p, arity, info)) :: l ->
       check_pred p arity info;
@@ -782,6 +796,11 @@ let rec check_all = function
 	nvn_e f;
 	List.iter (fun (_,t) -> nvn_t t) b) (!not_list);
       r
+  | (Future(phase, channels)) :: l ->
+      (if phase > !Param.max_used_phase then Param.max_used_phase := phase);
+      (* TODO: Check for duplicate "future" declaration. *)
+      future_phase := Some (phase, channels);
+      check_all l
   | _ -> internal_error "The first process part is not the last element of the file"
 
 (* Get the maximum phase number *)
@@ -803,21 +822,6 @@ let rec set_max_used_phase = function
 	Param.max_used_phase := n;
       set_max_used_phase p
 
-let parse_file s = 
-  let p = check_all (parse s) in
-  if !Param.key_compromise = 2 then
-    Param.max_used_phase := 1
-  else
-    set_max_used_phase p;
-  p
-
-let display () =
-   print_string "Functions ";
-   Hashtbl.iter (fun _ fsymb -> 
-     print_string (fsymb.f_name ^ "/" ^ (string_of_int (List.length (fst fsymb.f_type))) ^ ". ")
-       ) fun_decls;
-   print_string "\n"
-
 (* queries *)
 
 let non_compromised_session = FunApp(Param.session1, [])
@@ -938,6 +942,27 @@ and binding_find s = function
       else
 	binding_find s l
 
+let parse_file s = 
+  let p = check_all (parse s) in
+  begin match !future_phase with
+    | None -> ()
+    | Some (phase, channels) ->
+        let channels = List.map check_query_term channels in
+        Param.future_phase := Some (phase, channels)
+  end;
+  if !Param.key_compromise = 2 then
+    Param.max_used_phase := 1
+  else
+    set_max_used_phase p;
+  p
+
+let display () =
+   print_string "Functions ";
+   Hashtbl.iter (fun _ fsymb -> 
+     print_string (fsymb.f_name ^ "/" ^ (string_of_int (List.length (fst fsymb.f_type))) ^ ". ")
+       ) fun_decls;
+   print_string "\n"
+
 let add_binding ((i,e),t) =
   if Hashtbl.mem glob_table i then
     input_error ("Variable " ^ i ^ " defined after used.") e
diff --git a/src/pitransl.ml b/src/pitransl.ml
index f238b9a..f9396ff 100644
--- a/src/pitransl.ml
+++ b/src/pitransl.ml
@@ -45,6 +45,7 @@ List.fold_left (fun accu v -> accu') accu0 vlist
 let session0 = { f_name = "session0"; 
 		 f_type = [], Param.sid_type;
                  f_private = false;
+                 f_phases = [];
 		 f_options = 0;
 		 f_cat = Eq [];
 		 f_initial_cat = Eq []
@@ -527,11 +528,12 @@ let rec transl_term next_f cur_state = function
       | Eq red_rules ->
           transl_term_list (fun cur_state1 patlist -> 
 	    next_f cur_state1 (FunApp(f, patlist));
-	    List.iter (fun red_rule ->
-              let (left_list, right) = Terms.copy_red red_rule in
-	      next_f { cur_state1 with last_step_unif = List.fold_left2(fun accu_unif pat left ->
-                (pat,left)::accu_unif) cur_state1.last_step_unif patlist left_list } right
-	      ) red_rules
+	    List.iter (fun (red_rule, phases) ->
+	      if (phases = []) || (List.exists ((=) cur_state.cur_phase) phases) then
+                  let (left_list, right) = Terms.copy_red red_rule in
+	          next_f { cur_state1 with last_step_unif = List.fold_left2(fun accu_unif pat left ->
+                    (pat,left)::accu_unif) cur_state1.last_step_unif patlist left_list } right
+	          ) red_rules
 	      ) cur_state l
       | Red red_rules ->
           transl_term_list (fun cur_state1 patlist -> 
@@ -621,6 +623,7 @@ let occ_cst = FunApp({ f_name = "@occ_cst";
 		       f_cat = Tuple;
 		       f_initial_cat = Tuple;
 		       f_private = false;
+		       f_phases = [];
 		       f_options = 0 }, [])
 
 let occ_var_map = Hashtbl.create 7
@@ -1038,27 +1041,30 @@ let rec transl_process cur_state = function
                       output_pred = Param.get_pred (OutputP(n)) } p
 
 let rules_for_red f phase red_rule =
-  let res_pred = Param.get_pred (Attacker(phase, snd f.f_type)) in
-  let (hyp, concl) = Terms.copy_red red_rule in
-  add_rule (List.map (att_fact phase) hyp)
-    (att_fact phase concl) [] (Apply(Func(f), res_pred));
-  if !Param.non_interference then
-    begin
-      if !Terms.current_bound_vars != [] then
-	Parsing_helper.internal_error "bound vars should be cleaned up (pitransl4)";
-      let hyp' = List.map (Terms.generalize_vars_not_in []) hyp in
-      Terms.cleanup();
-  
-      let thyp = List.map Terms.get_term_type hyp in
-      let tuple_fun = Terms.get_tuple_fun thyp in
-      let vlist = List.map Terms.new_var_def thyp in
-      add_rule 
-        ((Pred(testunif_pred, [FunApp(tuple_fun, vlist); FunApp(tuple_fun, hyp')]))
-	 :: List.map (att_fact phase) vlist)
-	(Pred(bad_pred, []))
-	[]
-	(TestApply(Func(f), res_pred))
-    end
+  if (f.f_phases = []) || (List.exists ((=) phase) f.f_phases) then
+  begin
+    let res_pred = Param.get_pred (Attacker(phase, snd f.f_type)) in
+    let (hyp, concl) = Terms.copy_red red_rule in
+    add_rule (List.map (att_fact phase) hyp)
+      (att_fact phase concl) [] (Apply(Func(f), res_pred));
+    if !Param.non_interference then
+      begin
+        if !Terms.current_bound_vars != [] then
+	  Parsing_helper.internal_error "bound vars should be cleaned up (pitransl4)";
+        let hyp' = List.map (Terms.generalize_vars_not_in []) hyp in
+        Terms.cleanup();
+    
+        let thyp = List.map Terms.get_term_type hyp in
+        let tuple_fun = Terms.get_tuple_fun thyp in
+        let vlist = List.map Terms.new_var_def thyp in
+        add_rule 
+          ((Pred(testunif_pred, [FunApp(tuple_fun, vlist); FunApp(tuple_fun, hyp')]))
+	   :: List.map (att_fact phase) vlist)
+	  (Pred(bad_pred, []))
+	  []
+	  (TestApply(Func(f), res_pred))
+      end
+  end
 
 let rules_for_function phase _ f =
    if (not f.f_private) &&
@@ -1071,7 +1077,10 @@ let rules_for_function phase _ f =
 	 let vars = Terms.var_gen (fst f.f_type) in
 	 add_rule (List.map (att_fact phase) vars)
            (att_fact phase (FunApp(f,vars))) [] (Apply(Func(f), res_pred));
-	 List.iter (rules_for_red f phase) red_rules
+	 List.iter (fun (red_rule, phases) ->
+	    if (phases = []) || (List.exists ((=) phase) phases) then
+	        rules_for_red f phase red_rule
+	 ) red_rules
      | Red red_rules ->
 	 List.iter (rules_for_red f phase) red_rules
      | Tuple ->
@@ -1145,6 +1154,7 @@ let weak_memo = Param.memo (fun t ->
   { f_name = "@weaksecretcst"; 
     f_type = [], t;
     f_private = true;
+    f_phases = [];
     f_options = 0;
     f_cat = Eq [];
     f_initial_cat = Eq []
@@ -1173,7 +1183,8 @@ let rules_for_function_guess _ f =
     match f.f_cat with
       Eq red_rules -> 
 	let vars1 = Terms.var_gen (fst f.f_type) in
-        rules_for_red_guess f ((vars1, FunApp(f, vars1)) :: red_rules)
+        (* Note: Phases in red_rules are ignored here. *)
+        rules_for_red_guess f ((vars1, FunApp(f, vars1)) :: (List.map fst red_rules))
     | Red red_rules ->
 	rules_for_red_guess f red_rules;
 	List.iter (fun red ->
diff --git a/src/pitranslweak.ml b/src/pitranslweak.ml
index 0eef683..394deb7 100644
--- a/src/pitranslweak.ml
+++ b/src/pitranslweak.ml
@@ -29,6 +29,14 @@ open Parsing_helper
 open Types
 open Pitypes
 
+let available_red_rules phase red_rules =
+    List.fold_left (fun result (red, phases) ->
+        if (phases = []) || (List.exists ((=) phase) phases) then
+            red :: result
+        else
+            result
+    ) [] red_rules
+
 (* Find the minimum phase in which choice is used *)
 
 let rec has_choice = function
@@ -357,7 +365,7 @@ let rec transl_term next_f cur_state = function
 	    next_f cur_state1 (FunApp(f, patlist1)) (FunApp(f, patlist2))) cur_state l
       | Eq red_rules ->
 	  let vars1 = Terms.var_gen (fst f.f_type) in
-	  transl_red ((vars1, FunApp(f, vars1)) :: red_rules)
+	  transl_red ((vars1, FunApp(f, vars1)) :: (available_red_rules cur_state.cur_phase red_rules))
       | Red red_rules ->
 	  transl_red red_rules
       |	Choice ->
@@ -689,43 +697,46 @@ let rules_for_function phase _ f =
    match f.f_cat with
      Eq red_rules -> 
 	let vars1 = Terms.var_gen (fst f.f_type) in
-        rules_for_red f phase ((vars1, FunApp(f, vars1)) :: red_rules)
+        rules_for_red f phase ((vars1, FunApp(f, vars1)) :: (available_red_rules phase red_rules))
    | Red red_rules ->
-       rules_for_red f phase red_rules;
-       List.iter (fun red ->
-	  let (hyp, _) = Terms.copy_red red in
-	  let vlist = List.map Terms.new_var_def (List.map Terms.get_term_type hyp) in
-	  let make_constra red =
-	    let (hyp, _) = Terms.copy_red red in
-	    if !Terms.current_bound_vars != [] then
-	      Parsing_helper.internal_error "bound vars should be cleaned up (pitranslweak3)";
-	    let hyp' = List.map (Terms.generalize_vars_not_in []) hyp in
-	    Terms.cleanup();
-	    List.map2 (fun v t -> Neq(v,t)) vlist hyp'
-	  in  
-	  add_rule 
-            (List.map2 (att_fact phase) hyp vlist)
-	    (Pred(Param.bad_pred, []))
-	    (List.map make_constra red_rules)
-	    (TestApply(Func(f), res_pred));
-
-	  let (hyp, _) = Terms.copy_red red in
-	  let vlist = List.map Terms.new_var_def (List.map Terms.get_term_type hyp) in
-	  let make_constra red =
-	    let (hyp, _) = Terms.copy_red red in
-	    if !Terms.current_bound_vars != [] then
-	      Parsing_helper.internal_error "bound vars should be cleaned up (pitranslweak3)";
-	    let hyp' = List.map (Terms.generalize_vars_not_in []) hyp in
-	    Terms.cleanup();
-	    List.map2 (fun v t -> Neq(v,t)) vlist hyp'
-	  in  
-	  add_rule 
-            (List.map2 (att_fact phase) vlist hyp)
-	    (Pred(Param.bad_pred, []))
-	    (List.map make_constra red_rules)
-	    (TestApply(Func(f), res_pred))
-
-		  ) red_rules
+       if (f.f_phases = []) || (List.exists ((=) phase) f.f_phases) then
+       begin
+         rules_for_red f phase red_rules;
+         List.iter (fun red ->
+            let (hyp, _) = Terms.copy_red red in
+            let vlist = List.map Terms.new_var_def (List.map Terms.get_term_type hyp) in
+            let make_constra red =
+              let (hyp, _) = Terms.copy_red red in
+              if !Terms.current_bound_vars != [] then
+                Parsing_helper.internal_error "bound vars should be cleaned up (pitranslweak3)";
+              let hyp' = List.map (Terms.generalize_vars_not_in []) hyp in
+              Terms.cleanup();
+              List.map2 (fun v t -> Neq(v,t)) vlist hyp'
+            in  
+            add_rule 
+              (List.map2 (att_fact phase) hyp vlist)
+              (Pred(Param.bad_pred, []))
+              (List.map make_constra red_rules)
+              (TestApply(Func(f), res_pred));
+
+            let (hyp, _) = Terms.copy_red red in
+            let vlist = List.map Terms.new_var_def (List.map Terms.get_term_type hyp) in
+            let make_constra red =
+              let (hyp, _) = Terms.copy_red red in
+              if !Terms.current_bound_vars != [] then
+                Parsing_helper.internal_error "bound vars should be cleaned up (pitranslweak3)";
+              let hyp' = List.map (Terms.generalize_vars_not_in []) hyp in
+              Terms.cleanup();
+              List.map2 (fun v t -> Neq(v,t)) vlist hyp'
+            in  
+            add_rule 
+              (List.map2 (att_fact phase) vlist hyp)
+              (Pred(Param.bad_pred, []))
+              (List.map make_constra red_rules)
+              (TestApply(Func(f), res_pred))
+
+                    ) red_rules
+       end
    | Tuple -> 
 	(* For tuple constructor *)
 	let vars1 = Terms.var_gen (fst f.f_type) in
@@ -871,12 +882,25 @@ let transl p =
 	  let v2 = Terms.new_var Param.def_var_name t in
 	  Selfun.add_no_unif (att_i, [FVar v1; FVar v2]) Selfun.never_select_weight
 	end;
-      if i > 0 then
-	let w1 = Terms.new_var_def t in
-	let w2 = Terms.new_var_def t in
-	let att_im1 = Param.get_pred (AttackerBin(i-1,t)) in
-	add_rule [Pred(att_im1, [w1; w2])] (Pred(att_i, [w1; w2])) [] PhaseChange
-	  ) (if !Param.ignore_types then [Param.any_type] else !Param.all_types);
+      if i > 0 then begin
+	match !Param.future_phase with
+	  | Some (phase, channels) when phase = i ->
+	    for j = 0 to (i - 1) do
+	      let mess_j = Param.get_pred (MessBin(j,t)) in
+	      List.iter (fun channel ->
+	        let vm1 = Terms.new_var_def t in
+	        let vm2 = Terms.new_var_def t in
+	        add_rule [Pred(mess_j, [channel; vm1; channel; vm2])]
+	                 (Pred(att_i, [vm1; vm2])) [] FuturePhaseChange
+	      ) channels
+	    done
+	  | _ ->
+	    let att_im1 = Param.get_pred (AttackerBin(i-1,t)) in
+	    let w1 = Terms.new_var_def t in
+	    let w2 = Terms.new_var_def t in
+	    add_rule [Pred(att_im1, [w1; w2])] (Pred(att_i, [w1; w2])) [] PhaseChange
+      end
+    ) (if !Param.ignore_types then [Param.any_type] else !Param.all_types);
     if i > 0 then
       let w1 = Terms.new_var_def Param.table_type in
       let w2 = Terms.new_var_def Param.table_type in
@@ -886,13 +910,22 @@ let transl p =
   done;
 
 
-   (* Knowing the free names and creating new names is necessary only in phase 0.
-      The subsequent phases will get them by attacker'_i(x,y) -> attacker'_{i+1}(x,y) *)
+  (* Knowing the free names and creating new names is necessary only in phase 0.
+     The subsequent phases will get them by attacker'_i(x,y) -> attacker'_{i+1}(x,y)
+     However, in a "future phase", this is not the case. *)
 
-   (* The attacker has the public free names *)
-   List.iter (fun ch ->
+  let do_free_names phase =
+    (* The attacker has the public free names *)
+    List.iter (fun ch ->
       if not ch.f_private then
-        add_rule [] (att_fact 0 (FunApp(ch, [])) (FunApp(ch, []))) [] Init) (!Param.freenames);
+        add_rule [] (att_fact phase (FunApp(ch, [])) (FunApp(ch, []))) [] Init
+    ) (!Param.freenames)
+  in
+  do_free_names 0;
+  begin match !Param.future_phase with
+    | None -> ()
+    | Some(phase,_) -> do_free_names phase
+  end;
 
   List.iter (fun t ->
     (* The attacker can create new names *)
diff --git a/src/pitsyntax.ml b/src/pitsyntax.ml
index 3d3a2ce..9b1cd3d 100644
--- a/src/pitsyntax.ml
+++ b/src/pitsyntax.ml
@@ -212,6 +212,7 @@ let check_fun_decl (name, ext) argtypes restype options =
 	    f_cat = cat;
 	    f_initial_cat = cat;
 	    f_private = !is_private;
+	    f_phases = [];
 	    f_options = !opt }
   in
   Hashtbl.add fun_decls name r;
@@ -296,7 +297,7 @@ let check_equation env t1 t2 =
        let ext = merge_ext (snd t1) (snd t2) in
        input_error "the two members of an equation should have the same type" ext
      end;
-   TermsEq.register_equation (t1',t2')
+   TermsEq.register_equation (t1',t2') []
 
 (* Definitions of destructors by rewrite rules *)
 
@@ -341,6 +342,7 @@ let check_red tlist options =
             let fsymb = { f_name = f;
                           f_type = tylhs, tyrhs;
                           f_private = !is_private;
+                          f_phases = [];
 			  f_options = 0;
                           f_cat = cat;
 			  f_initial_cat = cat
@@ -535,6 +537,7 @@ let create_name s ty is_free =
      f_cat = cat;
      f_initial_cat = cat;
      f_private = not is_free;
+     f_phases = [];
      f_options = 0 }
 
 let create_name_uniq s ty is_free =
@@ -544,6 +547,7 @@ let create_name_uniq s ty is_free =
      f_cat = cat;
      f_initial_cat = cat;
      f_private = not is_free;
+     f_phases = [];
      f_options = 0 }
 
 let add_free_name (s,ext) t options =
@@ -1101,6 +1105,7 @@ let check_event (name, ext) argtypes =
 	    f_cat = Eq[];
 	    f_initial_cat = Eq[];
 	    f_private = true;
+	    f_phases = [];
 	    f_options = 0 }
   in
   Hashtbl.add event_fun_table name r;
@@ -1133,6 +1138,7 @@ let check_table (name, ext) argtypes =
 	    f_cat = Eq[];
 	    f_initial_cat = Eq[];
 	    f_private = true;
+	    f_phases = [];
 	    f_options = 0 }
   in
   global_env := StringMap.add name (ETable r) (!global_env)
diff --git a/src/reduction.ml b/src/reduction.ml
index 17b8bca..562e69a 100644
--- a/src/reduction.ml
+++ b/src/reduction.ml
@@ -1710,6 +1710,7 @@ let new_sid() =
     f_cat = cat;
     f_initial_cat = cat;
     f_private = false;
+    f_phases = [];
     f_options = 0
   }
 
diff --git a/src/reduction_helper.ml b/src/reduction_helper.ml
index 0390562..d873d5e 100644
--- a/src/reduction_helper.ml
+++ b/src/reduction_helper.ml
@@ -181,6 +181,7 @@ let funsymb_from_funspec = function
 	  f_cat = cat;
 	  f_initial_cat = cat;
           f_private = f.f_private;
+          f_phases = [];
 	  f_options = f.f_options }
       else
 	let vars = var_gen (fst f.f_type) in
@@ -192,6 +193,7 @@ let funsymb_from_funspec = function
 	  f_cat = cat;
 	  f_initial_cat = cat;
           f_private = f.f_private;
+          f_phases = [];
 	  f_options = f.f_options }
 	  
 (* Test equality. t1 and t2 must be closed, but they
@@ -240,6 +242,7 @@ let new_name p s t =
     f_cat = cat;
     f_initial_cat = cat;
     f_private = p;
+    f_phases = [];
     f_options = 0
   }
 
diff --git a/src/rules.ml b/src/rules.ml
index 511676f..fb17b91 100644
--- a/src/rules.ml
+++ b/src/rules.ml
@@ -426,6 +426,7 @@ let elim_var_if_possible has_gen_var rule v =
 				f_cat = Eq []; (* Should not be a name to avoid bad interaction with any_name_fsymb *)
 				f_initial_cat = Eq []; (* Should not be a name to avoid bad interaction with any_name_fsymb *)
 				f_private = true;
+				f_phases = [];
 			        f_options = 0 }, []));
              Terms.current_bound_vars := v :: (!Terms.current_bound_vars)
          | TLink _ -> ()
diff --git a/src/syntax.ml b/src/syntax.ml
index e61fa5c..9404b2f 100644
--- a/src/syntax.ml
+++ b/src/syntax.ml
@@ -93,6 +93,7 @@ let check_fun_decl is_tuple (name,ext) arity =
       Hashtbl.add fun_decls name { f_name = name;
 				   f_type = (Terms.copy_n arity Param.any_type), Param.any_type;
 				   f_private = false;
+				   f_phases = [];
 				   f_options = 0;
 				   f_cat = cat;
 				   f_initial_cat = cat }
@@ -198,6 +199,7 @@ let get_name s arity ext =
               f_cat = cat;
 	      f_initial_cat = cat;
               f_private = true;
+              f_phases = [];
 	      f_options = 0 } 
     in
     Hashtbl.add name_env s r;
@@ -332,7 +334,7 @@ let query_facts = ref ([] : fact list)
 let rec check_all = function
     (FunDecl (f,i))::l -> check_fun_decl false f i; check_all l
   | (DataFunDecl(f,i))::l -> check_fun_decl true f i; check_all l
-  | (Equation(t1,t2))::l -> check_equation (t1,t2); check_all l
+  | (Equation(t1,t2))::l -> check_equation (t1,t2) []; check_all l
   | (Query fact) :: l -> 
       let env = Hashtbl.create 7 in
       query_facts := (check_simple_fact env fact) :: (!query_facts);
diff --git a/src/terms.ml b/src/terms.ml
index f8bed79..d8e1931 100644
--- a/src/terms.ml
+++ b/src/terms.ml
@@ -45,6 +45,7 @@ let get_tuple_fun tl =
               f_cat = Tuple;
               f_initial_cat = Tuple;
               f_private = false;
+              f_phases = [];
 	      f_options = 0 }
     in
     Hashtbl.add tuple_table tl r;
@@ -563,6 +564,7 @@ let new_gen_var t =
     f_cat = General_var;
     f_initial_cat = General_var;
     f_private = true;
+    f_phases = [];
     f_options = 0 }
 
 let rec generalize_vars_not_in vlist = function
@@ -727,6 +729,7 @@ let true_cst =
     f_cat = Tuple;
     f_initial_cat = Tuple;
     f_private = false;
+    f_phases = [];
     f_options = 0 }
 
 let false_cst =
@@ -735,6 +738,7 @@ let false_cst =
     f_cat = Tuple;
     f_initial_cat = Tuple;
     f_private = false;
+    f_phases = [];
     f_options = 0 }
 
 (* Functions *)
@@ -750,6 +754,7 @@ let equal_memo = Param.memo (fun t ->
     f_cat = equal_cat;
     f_initial_cat = equal_cat;
     f_private = false;
+    f_phases = [];
     f_options = 0 })
 
 let equal_fun t =
@@ -762,6 +767,7 @@ let and_fun =
     f_cat = and_cat;
     f_initial_cat = and_cat;
     f_private = false;
+    f_phases = [];
     f_options = 0 }
 
 let not_cat = 
@@ -774,6 +780,7 @@ let not_fun =
     f_cat = not_cat;
     f_initial_cat = not_cat;
     f_private = false;
+    f_phases = [];
     f_options = 0 }
 
 let new_name_memo = Param.memo (fun t ->
@@ -783,6 +790,7 @@ let new_name_memo = Param.memo (fun t ->
     f_cat = cat;
     f_initial_cat = cat;
     f_private = false;
+    f_phases = [];
     f_options = 0 })
 
 let new_name_fun t =
diff --git a/src/termsEq.ml b/src/termsEq.ml
index c0a4b06..c6693ca 100644
--- a/src/termsEq.ml
+++ b/src/termsEq.ml
@@ -32,9 +32,9 @@ open Parsing_helper
 let equationsToRecord = ref false
 
 let equations_list = ref []
-let register_equation eq =
+let register_equation eq phases =
   equationsToRecord := true;
-  equations_list := eq :: (!equations_list)
+  equations_list := (eq, phases) :: (!equations_list)
 
 let hasEquations() =
   !equations_list != []
@@ -57,7 +57,7 @@ let rec close_term_eq restwork = function
 	restwork (FunApp(f,l'));
 	match f.f_cat with
 	  Eq eqlist ->
-	    List.iter (fun red ->
+	    List.iter (fun (red, _) ->
 	      let curr_bound_vars = !current_bound_vars in
 	      current_bound_vars := [];
 	      let (leq', req') = copy_red red in
@@ -154,7 +154,7 @@ let rec close_term_destr_eq restwork = function
 	match f.f_cat with
 	  Eq eqlist ->
 	    restwork (FunApp(f,l'));
-	    List.iter (fun red ->
+	    List.iter (fun (red, _) ->
 	      let curr_bound_vars = !current_bound_vars in
 	      current_bound_vars := [];
 	      let (leq', req') = copy_red red in
@@ -677,137 +677,144 @@ let record_eqs () =
 
    if !Param.eqtreatment = Param.ConvLin then
    begin
-    (*print_string "Building order...";
-    Display.Text.newline();*)
-    List.iter add_order (!equations_list);
-    (*print_string "Building blocks...";
-    Display.Text.newline();*)
-    let blocks = buildblocks (!equations_list) in
-    (*print_string "Separating convergent/linear...";
-    Display.Text.newline();*)
-    let convergent_part = ref [] in
-    let linear_part = ref [] in
-    List.iter (fun block ->
-      try 
-	check_convergent block;
-        convergent_part := block @ (!convergent_part)
-      with
-	(Nontermination _ | Nonconfluent _) as e ->
-	  if is_linear block then
-            linear_part := block @ (!linear_part)
-	  else
-            begin
-              print_string "Error: Cannot handle the following equations:";
-              Display.Text.display_item_list Display.Text.display_eq block;
-	      print_string "This block of equations is not linear and could not be proved convergent.\n";
-	      begin
-		match e with
-		  Nontermination eq -> 
-		    print_string "(I could not prove that\n";
-		    Display.Text.display_eq eq;
-		    print_string "\nis decreasing in a lexicographic path ordering.)\n"
-		| Nonconfluent(eq1,eq2) ->
-		    print_string "(The system is not confluent because of a critical pair between\n";
-		    Display.Text.display_eq eq1;
-		    print_string "\nand\n";
-		    Display.Text.display_eq eq2;
-		    print_string ".)\n"
-		| _ -> Parsing_helper.internal_error "TermsEq: added to avoid warning for non-exhaustive pattern-matching"
-	      end;
-              Parsing_helper.user_error "These equations cannot be handled.\n"
-        end
-       ) blocks;
-
-    if !Param.html_output then
-      begin
-        Display.Html.print_string "<H2>Linear part</H2>\n";
-        Display.Html.print_string "Initial equations:";
-        Display.Html.display_item_list Display.Html.display_eq (!linear_part)
-      end
-    else if !Param.verbose_eq then
-      begin
-        Display.Text.print_string "Linear part:";
-        Display.Text.display_item_list Display.Text.display_eq (!linear_part)
-      end;
-    List.iter (fun eq -> 
-       add_eq eq; 
-       add_eq (swap_eq eq)) (!linear_part);
-    print_string "Completing equations...";
-    Display.Text.newline();
-    let resulting_equations_linear = complete_eq true in
-    eq_base := [];
-    if !Param.html_output then
-      begin
-        Display.Html.print_string "Completed equations:";
-        Display.Html.display_item_list Display.Html.display_eq resulting_equations_linear
-      end
-    else if !Param.verbose_eq then
-      begin
-        Display.Text.print_string "Completed equations:";
-        Display.Text.display_item_list Display.Text.display_eq resulting_equations_linear
-      end;
-
-    if !Param.html_output then
-      begin
-        Display.Html.print_string "<H2>Convergent part</H2>\n";
-        Display.Html.print_string "Initial equations:";
-	Display.Html.display_item_list Display.Html.display_eq (!convergent_part)
-      end
-    else if !Param.verbose_eq then
-      begin
-        Display.Text.print_string "Convergent part:";
-	Display.Text.display_item_list Display.Text.display_eq (!convergent_part)
-      end;
-    rewrite_system := !convergent_part;
-    List.iter add_eq (!convergent_part);
-    print_string "Completing equations...";
-    Display.Text.newline();
-    let resulting_equations_convergent = complete_eq false in
-    if !Param.html_output then
-      begin
-        Display.Html.print_string "Completed equations:";
-        Display.Html.display_item_list Display.Html.display_eq resulting_equations_convergent
-      end
-    else if !Param.verbose_eq then
-      begin
-        Display.Text.print_string "Completed equations:";
-            Display.Text.display_item_list Display.Text.display_eq resulting_equations_convergent
-      end;
-    
-    let resulting_equations = resulting_equations_linear @ resulting_equations_convergent in
-    (* record the equations in each constructor *)
-    List.iter (function
-      (FunApp(f, l), req) as eq -> 
-        begin
-	  let var_list_rhs = ref [] in
-	  Terms.get_vars var_list_rhs req;
-	  if not (List.for_all (fun v -> List.exists (Terms.occurs_var v) l) (!var_list_rhs)) then
-	    begin
-	      print_string "Equation: ";
-	      Display.Text.display_eq eq;
-	      print_newline();
-	      Parsing_helper.user_error "Error: All variables of the right-hand side of an equation\nshould also occur in the left-hand side.\n"
-	    end;
-
-          match f.f_cat with
-            Eq leq -> f.f_cat <- Eq ((l, req) :: leq)
-          | _ -> user_error "Does not support equations on non-constructors\n"
-        end
-    | _ -> ()) resulting_equations
-
+    for phase = 0 to !Param.max_used_phase do
+        (* Transform equations for each phase separately. *)
+        (*print_string "Building order...";
+        Display.Text.newline();*)
+        order := [];
+        (* Only transform the equations that are available in this phase. *)
+        let equations = List.filter (fun (eq, phases) ->
+            (phases = []) || (List.exists ((=) phase) phases)
+        ) !equations_list in
+        List.iter add_order (List.map fst equations);
+        (*print_string "Building blocks...";
+        Display.Text.newline();*)
+        let blocks = buildblocks (List.map fst equations) in
+        (*print_string "Separating convergent/linear...";
+        Display.Text.newline();*)
+        let convergent_part = ref [] in
+        let linear_part = ref [] in
+        List.iter (fun block ->
+          try 
+            check_convergent block;
+            convergent_part := block @ (!convergent_part)
+          with
+            (Nontermination _ | Nonconfluent _) as e ->
+              if is_linear block then
+                linear_part := block @ (!linear_part)
+              else
+                begin
+                  print_string "Error: Cannot handle the following equations:";
+                  Display.Text.display_item_list Display.Text.display_eq block;
+                  print_string "This block of equations is not linear and could not be proved convergent.\n";
+                  begin
+                    match e with
+                      Nontermination eq -> 
+                        print_string "(I could not prove that\n";
+                        Display.Text.display_eq eq;
+                        print_string "\nis decreasing in a lexicographic path ordering.)\n"
+                    | Nonconfluent(eq1,eq2) ->
+                        print_string "(The system is not confluent because of a critical pair between\n";
+                        Display.Text.display_eq eq1;
+                        print_string "\nand\n";
+                        Display.Text.display_eq eq2;
+                        print_string ".)\n"
+                    | _ -> Parsing_helper.internal_error "TermsEq: added to avoid warning for non-exhaustive pattern-matching"
+                  end;
+                  Parsing_helper.user_error "These equations cannot be handled.\n"
+            end
+           ) blocks;
+
+         if !Param.html_output then
+           begin
+             Display.Html.print_string "<H2>Linear part</H2>\n";
+             Display.Html.print_string "Initial equations:";
+             Display.Html.display_item_list Display.Html.display_eq (!linear_part)
+           end
+         else if !Param.verbose_eq then
+           begin
+             Display.Text.print_string "Linear part:";
+             Display.Text.display_item_list Display.Text.display_eq (!linear_part)
+           end;
+         List.iter (fun eq -> 
+            add_eq eq; 
+            add_eq (swap_eq eq)) (!linear_part);
+         print_string "Completing equations...";
+         Display.Text.newline();
+         let resulting_equations_linear = complete_eq true in
+         eq_base := [];
+         if !Param.html_output then
+           begin
+             Display.Html.print_string "Completed equations:";
+             Display.Html.display_item_list Display.Html.display_eq resulting_equations_linear
+           end
+         else if !Param.verbose_eq then
+           begin
+             Display.Text.print_string "Completed equations:";
+             Display.Text.display_item_list Display.Text.display_eq resulting_equations_linear
+           end;
+
+         if !Param.html_output then
+           begin
+             Display.Html.print_string "<H2>Convergent part</H2>\n";
+             Display.Html.print_string "Initial equations:";
+             Display.Html.display_item_list Display.Html.display_eq (!convergent_part)
+           end
+         else if !Param.verbose_eq then
+           begin
+             Display.Text.print_string "Convergent part:";
+             Display.Text.display_item_list Display.Text.display_eq (!convergent_part)
+           end;
+         rewrite_system := !convergent_part;
+         List.iter add_eq (!convergent_part);
+         print_string "Completing equations...";
+         Display.Text.newline();
+         let resulting_equations_convergent = complete_eq false in
+         if !Param.html_output then
+           begin
+             Display.Html.print_string "Completed equations:";
+             Display.Html.display_item_list Display.Html.display_eq resulting_equations_convergent
+           end
+         else if !Param.verbose_eq then
+           begin
+             Display.Text.print_string "Completed equations:";
+                 Display.Text.display_item_list Display.Text.display_eq resulting_equations_convergent
+           end;
+         
+         let resulting_equations = resulting_equations_linear @ resulting_equations_convergent in
+         (* record the equations in each constructor *)
+         List.iter (function
+           (FunApp(f, l), req) as eq -> 
+             begin
+               let var_list_rhs = ref [] in
+               Terms.get_vars var_list_rhs req;
+               if not (List.for_all (fun v -> List.exists (Terms.occurs_var v) l) (!var_list_rhs)) then
+                 begin
+                   print_string "Equation: ";
+                   Display.Text.display_eq eq;
+                   print_newline();
+                   Parsing_helper.user_error "Error: All variables of the right-hand side of an equation\nshould also occur in the left-hand side.\n"
+                 end;
+
+               match f.f_cat with
+                 Eq leq -> f.f_cat <- Eq (((l, req), [phase]) :: leq)
+               | _ -> user_error "Does not support equations on non-constructors\n"
+             end
+         | _ -> ()) resulting_equations
+    done
    end
    else
    begin
     (* Old, non-proved treatment of equations.
        Kept just in case it is useful... *)
-    List.iter find_rewrite_system (!equations_list);
+    List.iter find_rewrite_system (List.map fst !equations_list);
     if !Param.verbose_eq then
       begin
         print_string "Rewriting system:";
         Display.Text.display_item_list Display.Text.display_eq (!rewrite_system)
       end;
 
-    List.iter (fun eq -> add_eq eq;
+    List.iter (fun (eq,_) -> add_eq eq;
                          add_eq (swap_eq eq)) (!equations_list);
     print_string "Completing equations...";
     Display.Text.newline();
@@ -832,7 +839,7 @@ let record_eqs () =
 	    end;
 
           match f.f_cat with
-            Eq leq -> f.f_cat <- Eq ((l, req) :: leq)
+            Eq leq -> f.f_cat <- Eq (((l, req), []) :: leq)
           | _ -> user_error "Does not support equations on non-constructors\n"
         end
     | _ -> ()) resulting_equations
@@ -888,7 +895,7 @@ let rec close_term_eq_exc restwork = function
           match f.f_cat with
             Eq eqlist ->
 	      let rec reweqlist = function
-		  (leq, req) :: lrew ->
+		  ((leq, req), _) :: lrew ->
 		    let curr_bound_vars = !current_bound_vars in
 		    current_bound_vars := [];
 		    let leq' = List.map copy_term leq in
@@ -957,6 +964,7 @@ let get_syntactic f =
                f_cat = Syntactic f;
                f_initial_cat = Syntactic f;
                f_private = f.f_private;
+               f_phases = [];
 	       f_options = f.f_options } in
     Hashtbl.add syntactic_table f f';
     f'
@@ -1048,7 +1056,7 @@ let rec close_term_eq_synt restwork = function
           match f.f_cat with
             Eq eqlist ->
 	      let rec reweqlist = function
-		  (leq, req) :: lrew ->
+		  ((leq, req), _) :: lrew ->
 		    let curr_bound_vars = !current_bound_vars in
 		    current_bound_vars := [];
 		    let leq' = List.map put_syntactic leq in
diff --git a/src/termsEq.mli b/src/termsEq.mli
index 6483665..4f16c50 100644
--- a/src/termsEq.mli
+++ b/src/termsEq.mli
@@ -29,7 +29,7 @@
    an equational theory *)
 
 (* Register an equation *)
-val register_equation : Types.term * Types.term -> unit
+val register_equation : Types.term * Types.term -> int list (* phases *) -> unit
 
 (* returns true when at least one equation has been registered since last
    call to record_eqs *)
diff --git a/src/tsyntax.ml b/src/tsyntax.ml
index 8081f0e..5c3391b 100644
--- a/src/tsyntax.ml
+++ b/src/tsyntax.ml
@@ -107,6 +107,7 @@ let check_name_decl (s,ext) ty =
               f_cat = cat;
 	      f_initial_cat = cat;
               f_private = true;
+              f_phases = [];
 	      f_options = 0 } 
     in
     Hashtbl.add name_env s r
@@ -152,6 +153,7 @@ let check_fun_decl (name, ext) argtypes restype options =
     Hashtbl.add fun_decls name { f_name = name;
 				 f_type = tyarg, tyres;
 				 f_private = false;
+				 f_phases = [];
 				 f_options = !opt;
 				 f_cat = cat;
 				 f_initial_cat = cat }
@@ -225,7 +227,7 @@ let check_equation env t1 t2 =
        (* TO DO locate this error message *)
        user_error "The two members of an equation should have the same type.\n" 
      end;
-   TermsEq.register_equation (t1',t2')
+   TermsEq.register_equation (t1',t2') []
 
 
 let rule_counter = ref 0
diff --git a/src/types.mli b/src/types.mli
index 25c13ff..11c271e 100644
--- a/src/types.mli
+++ b/src/types.mli
@@ -119,7 +119,8 @@ and name_info = { mutable prev_inputs : term option;
 
 and funcats = 
     Red of (term list * term) list
-  | Eq of (term list * term) list
+  | Eq of ((term list * term) * int list (* phases *)) list
+        (* XXX: phase list never contains more than 1 element. *)
   | Tuple 
   | Name of name_info
   | SpecVar of binder
@@ -134,6 +135,7 @@ and funsymb = { f_name : string;
                                             equational theory. The initial f_cat is used in reduction.ml,
 					    and also in check_several_types *)
 	    	f_private : bool; (* true when the function cannot be applied by the adversary *)
+	    	f_phases  : int list; (* phases containing this function (empty list means all phases) *)
 		f_options : int
               }
 
@@ -212,6 +214,7 @@ type label =
   | Rn of predicate
   | Init
   | PhaseChange
+  | FuturePhaseChange
   | TblPhaseChange
   | LblComp
   | LblNone
