diff --git a/build b/build
index 305849f..93ec1d7 100755
--- a/build
+++ b/build
@@ -8,11 +8,11 @@ ocamlyacc piparser.mly
 ocamllex pilexer.mll
 ocamlyacc pitparser.mly
 ocamllex pitlexer.mll
-ocamlopt -o ../proverif parsing_helper.mli parsing_helper.ml stringmap.mli stringmap.ml ptree.mli piptree.mli pitptree.mli types.mli pitypes.mli param.mli param.ml parser.mli parser.ml lexer.ml queue.mli queue.ml terms.mli terms.ml termslinks.mli termslinks.ml display.mli display.ml history.mli history.ml termsEq.mli termsEq.ml pievent.mli pievent.ml weaksecr.mli weaksecr.ml noninterf.mli noninterf.ml selfun.mli selfun.ml rules.mli rules.ml syntax.mli syntax.ml tsyntax.mli tsyntax.ml piparser.mli piparser.ml pilexer.ml pitparser.mli pitparser.ml pitlexer.ml spassout.mli spassout.ml reduction_helper.mli reduction_helper.ml pisyntax.mli pisyntax.ml pitsyntax.mli pitsyntax.ml pitransl.mli pitransl.ml pitranslweak.mli pitranslweak.ml reduction.mli reduction.ml reduction_bipro.mli reduction_bipro.ml piauth.mli piauth.ml main.ml
+ocamlopt -o ../proverif lists.mli lists.ml parsing_helper.mli parsing_helper.ml stringmap.mli stringmap.ml ptree.mli piptree.mli pitptree.mli types.mli pitypes.mli param.mli param.ml parser.mli parser.ml lexer.ml queue.mli queue.ml terms.mli terms.ml termslinks.mli termslinks.ml display.mli display.ml optimisation.mli optimisation.ml history.mli history.ml termsEq.mli termsEq.ml pievent.mli pievent.ml weaksecr.mli weaksecr.ml noninterf.mli noninterf.ml selfun.mli selfun.ml rules.mli rules.ml syntax.mli syntax.ml tsyntax.mli tsyntax.ml piparser.mli piparser.ml pilexer.ml pitparser.mli pitparser.ml pitlexer.ml spassout.mli spassout.ml reduction_helper.mli reduction_helper.ml pisyntax.mli pisyntax.ml pitsyntax.mli pitsyntax.ml pitransl.mli pitransl.ml pitranslweak.mli pitranslweak.ml reduction.mli reduction.ml reduction_bipro.mli reduction_bipro.ml piauth.mli piauth.ml main.ml
 
 ocamllex lexertotex.mll
 ocamllex pitlexertotex.mll
-ocamlopt -o ../proveriftotex parsing_helper.cmx param.cmx piparser.cmx pilexer.cmx pitparser.cmx pitlexer.cmx fileprint.ml lexertotex.ml pitlexertotex.ml proveriftotex.ml
+ocamlopt -o ../proveriftotex lists.mli lists.ml parsing_helper.cmx param.cmx piparser.cmx pilexer.cmx pitparser.cmx pitlexer.cmx fileprint.ml lexertotex.ml pitlexertotex.ml proveriftotex.ml
 
 if [ -f xtime.c ]
 then
diff --git a/build.bat b/build.bat
index 7ae0ace..518be05 100755
--- a/build.bat
+++ b/build.bat
@@ -6,10 +6,10 @@ ocamlyacc piparser.mly
 ocamllex pilexer.mll
 ocamlyacc pitparser.mly
 ocamllex pitlexer.mll
-ocamlc -o ..\proverif.exe parsing_helper.mli parsing_helper.ml stringmap.mli stringmap.ml ptree.mli piptree.mli pitptree.mli types.mli pitypes.mli param.mli param.ml parser.mli parser.ml lexer.ml queue.mli queue.ml terms.mli terms.ml display.mli display.ml termslinks.mli termslinks.ml history.mli history.ml termsEq.mli termsEq.ml pievent.mli pievent.ml weaksecr.mli weaksecr.ml noninterf.mli noninterf.ml selfun.mli selfun.ml rules.mli rules.ml syntax.mli syntax.ml tsyntax.mli tsyntax.ml piparser.mli piparser.ml pilexer.ml pitparser.mli pitparser.ml pitlexer.ml spassout.mli spassout.ml reduction_helper.mli reduction_helper.ml pisyntax.mli pisyntax.ml pitsyntax.mli pitsyntax.ml pitransl.mli pitransl.ml pitranslweak.mli pitranslweak.ml reduction.mli reduction.ml reduction_bipro.mli reduction_bipro.ml piauth.mli piauth.ml main.ml
+ocamlc -o ..\proverif.exe lists.mli lists.ml parsing_helper.mli parsing_helper.ml stringmap.mli stringmap.ml ptree.mli piptree.mli pitptree.mli types.mli pitypes.mli param.mli param.ml parser.mli parser.ml lexer.ml queue.mli queue.ml terms.mli terms.ml display.mli display.ml termslinks.mli termslinks.ml optimisation.mli optimisation.ml history.mli history.ml termsEq.mli termsEq.ml pievent.mli pievent.ml weaksecr.mli weaksecr.ml noninterf.mli noninterf.ml selfun.mli selfun.ml rules.mli rules.ml syntax.mli syntax.ml tsyntax.mli tsyntax.ml piparser.mli piparser.ml pilexer.ml pitparser.mli pitparser.ml pitlexer.ml spassout.mli spassout.ml reduction_helper.mli reduction_helper.ml pisyntax.mli pisyntax.ml pitsyntax.mli pitsyntax.ml pitransl.mli pitransl.ml pitranslweak.mli pitranslweak.ml reduction.mli reduction.ml reduction_bipro.mli reduction_bipro.ml piauth.mli piauth.ml main.ml
 
 ocamllex lexertotex.mll
 ocamllex pitlexertotex.mll
-ocamlc -o ..\proveriftotex.exe parsing_helper.mli parsing_helper.ml ptree.mli piptree.mli pitptree.mli types.mli param.mli param.ml piparser.mli piparser.ml pilexer.ml pitparser.mli pitparser.ml pitlexer.ml fileprint.ml lexertotex.ml pitlexertotex.ml proveriftotex.ml
+ocamlc -o ..\proveriftotex.exe lists.mli lists.ml parsing_helper.mli parsing_helper.ml ptree.mli piptree.mli pitptree.mli types.mli param.mli param.ml piparser.mli piparser.ml pilexer.ml pitparser.mli pitparser.ml pitlexer.ml fileprint.ml lexertotex.ml pitlexertotex.ml proveriftotex.ml
 
 cd ..
diff --git a/examples/pi/state/Garay-Mackenzie.pi b/examples/pi/state/Garay-Mackenzie.pi
new file mode 100644
index 0000000..b231016
--- /dev/null
+++ b/examples/pi/state/Garay-Mackenzie.pi
@@ -0,0 +1,255 @@
+(* Two-party instance of the Garay and Mackenzie contract signing protocol. *)
+
+param verboseClauses = short.
+param propagateState = true.
+
+(* Public channel. *)
+free Internet.
+
+(* Value used for initial states. *)
+free Init.
+
+(* Commands. *)
+free Abort.
+free Resolve_1.
+free Resolve_2.
+
+(* Trusted party states. *)
+free Aborted.
+free Resolved_2.
+free Resolved_1.
+
+(* Contract for which the security properties are verified. *)
+free Witnessing_Contract.
+
+(* Trusted party's secret key. *)
+private free Trusted_Party_Secret_Key.
+
+(* Secret keys. *)
+free Secret_Key_1.
+free Secret_Key_2.
+
+(* Cryptography. *)
+fun Public_Key /1.
+fun Sign       /2.
+fun PCS        /4.
+
+reduc Check_Get_Message (Public_Key (Secret_Key),
+                         Sign (Secret_Key, Message))
+        = Message.
+
+fun OK     /0.
+
+(* Check private contract signature. *)
+reduc Check_PCS (Contract,
+                 Public_Key (Secret_Key_X),
+                 Public_Key_Y,
+                 Public_Key_Z,
+                 PCS (Secret_Key_X,
+                      Public_Key_Y,
+                      Public_Key_Z,
+                      Contract))
+        = OK.
+
+(* Convert a private contract signature to a signature. *)
+reduc Convert_PCS (Public_Key_Z,
+                   PCS (Secret_Key_X,
+                        Public_Key_Y,
+                        Public_Key (Secret_Key_Z),
+                        Contract))
+        = Sign (Secret_Key_X, Contract).
+
+(* State of the trusted party. (mode, signatures) pair. *)
+
+cell Trusted_Party_State := (Init, Init).
+
+
+query attacker:Some_State,
+               ( Sign (Trusted_Party_Secret_Key,
+                       ( ( Contract,
+                           ( Public_Key (Secret_Key_1),
+                             Public_Key (Secret_Key_2) )),
+                         Sign (Secret_Key_1,
+                               ( Contract,
+                                 ( Public_Key (Secret_Key_1),
+                                   Public_Key (Secret_Key_2) ))))),
+                 Sign (Trusted_Party_Secret_Key,
+                       ( Sign (Secret_Key_1, Contract),
+                         Sign (Secret_Key_2, Contract)))) .
+
+let T' =
+  out (Internet, Public_Key (Trusted_Party_Secret_Key));
+  Trusted_Party | ! Stateless_Trusted_Party .
+
+(* Precise model of the trusted party for the witnessing contract. *)
+
+let Trusted_Party =
+  (* Contract for which the security properties will
+     be verified. *)
+  new Witnessing_Contract;
+
+  out (Internet, Witnessing_Contract);
+  let Public_Key_1 = Public_Key (Secret_Key_1) in
+  let Public_Key_2 = Public_Key (Secret_Key_2) in
+  ( ! Abort_1_Process 
+  | ! Resolve_2_Process
+  | ! Resolve_1_Process ) .
+
+let Abort_1_Process =
+  in (Internet, ( Command,
+                  ( ( Contract, Parties ),
+                    Signature )));
+  if Command = Abort then
+    if Parties = ( Public_Key_1, Public_Key_2 ) then
+      if Contract = Witnessing_Contract then
+        if Check_Get_Message (Public_Key_1, Signature)
+          = ( Contract, Parties )
+        then
+          lock (Trusted_Party_State);
+          read Trusted_Party_State as
+            ( Current_State, Current_Signatures );
+          if Current_State = Aborted then
+            unlock (Trusted_Party_State);
+            out (Internet, Current_Signatures)
+          else if Current_State = Init then
+            let TP_Signature = Sign (Trusted_Party_Secret_Key,
+                                  ( ( Contract, Parties ),
+                                    Signature )) in
+            Trusted_Party_State := ( Aborted, TP_Signature );
+            unlock (Trusted_Party_State);
+            out (Internet, TP_Signature) .
+
+let Resolve_2_Process =
+  in (Internet, ( Command,
+                  ( PCS_1, Signature_2 )));
+  let Contract = Check_Get_Message (Public_Key_2, Signature_2) in
+  if Contract = Witnessing_Contract then
+    if Check_PCS (Contract,
+                  Public_Key_1,
+                  Public_Key_2,
+                  Public_Key (Trusted_Party_Secret_Key),
+                  PCS_1) = OK
+    then
+      lock (Trusted_Party_State);
+      read Trusted_Party_State as ( Current_Status, Current_Signatures );
+      if Current_Status = Resolved_2 then
+        unlock (Trusted_Party_State);
+        out (Internet, Current_Signatures)
+      else if Current_Status = Init then
+        let Signature_1 = Convert_PCS (Trusted_Party_Secret_Key, PCS_1) in
+        let TP_Signature = Sign (Trusted_Party_Secret_Key,
+                              ( Signature_1, Signature_2 )) in
+        Trusted_Party_State := ( Resolved_2, TP_Signature );
+        unlock (Trusted_Party_State);
+        out (Internet, TP_Signature) .
+
+let Resolve_1_Process =
+  in (Internet, ( Command,
+                  ( Signature_1, PCS_2 )));
+  let Contract = Check_Get_Message (Public_Key_1, Signature_1) in
+  if Contract = Witnessing_Contract then
+    if Check_PCS (Contract,
+                  Public_Key_2,
+                  Public_Key_1,
+                  Public_Key (Trusted_Party_Secret_Key),
+                  PCS_2) = OK
+    then
+      lock (Trusted_Party_State);
+      read Trusted_Party_State as ( Current_Status, Current_Signatures );
+      if Current_Status = Resolved_1 then
+        unlock (Trusted_Party_State);
+        out (Internet, Current_Signatures)
+      else if Current_Status = Init then
+        let Signature_2 = Convert_PCS (Trusted_Party_Secret_Key, PCS_2) in
+        let TP_Signature = Sign (Trusted_Party_Secret_Key,
+                              ( Signature_1, Signature_2 )) in
+        Trusted_Party_State := ( Resolved_1, TP_Signature );
+        unlock (Trusted_Party_State);
+        out (Internet, TP_Signature) .
+
+(* Approximate, stateless model of the trusted party for contracts other than
+   the witnessing contract. *)
+
+let Stateless_Trusted_Party =
+  new Bogus_Contract;
+  out (Internet, Bogus_Contract);
+  in (Internet, Public_Key_1);
+  in (Internet, Public_Key_2);
+  ( ! Stateless_Abort_1_Process
+  | ! Stateless_Resolve_2_Process
+  | ! Stateless_Resolve_1_Process ) .
+
+
+let Stateless_Abort_1_Process =
+  in (Internet, ( Command,
+                  ( ( Contract, Parties ),
+                    Signature )));
+  if Command = Abort then
+    if Parties = ( Public_Key_1, Public_Key_2 ) then
+      if Contract = Bogus_Contract then
+        if Check_Get_Message (Public_Key_1, Signature)
+          = ( Contract, Parties )
+        then
+          lock (Trusted_Party_State);
+          read Trusted_Party_State as
+            ( Current_State, Current_Signatures );
+          if Current_State = Aborted then
+            unlock (Trusted_Party_State);
+            out (Internet, Current_Signatures)
+          else if Current_State = Init then
+            let TP_Signature = Sign (Trusted_Party_Secret_Key,
+                                  ( ( Contract, Parties ),
+                                    Signature )) in
+            Trusted_Party_State := ( Aborted, TP_Signature );
+            unlock (Trusted_Party_State);
+            out (Internet, TP_Signature) .
+
+let Stateless_Resolve_2_Process =
+  in (Internet, ( Command,
+                  ( PCS_1, Signature_2 )));
+  let Contract = Check_Get_Message (Public_Key_2, Signature_2) in
+  if Contract = Bogus_Contract then
+    if Check_PCS (Contract,
+                  Public_Key_1,
+                  Public_Key_2,
+                  Public_Key (Trusted_Party_Secret_Key),
+                  PCS_1) = OK
+    then
+      lock (Trusted_Party_State);
+      read Trusted_Party_State as ( Current_Status, Current_Signatures );
+      if Current_Status = Resolved_2 then
+        unlock (Trusted_Party_State);
+        out (Internet, Current_Signatures)
+      else if Current_Status = Init then
+        let Signature_1 = Convert_PCS (Trusted_Party_Secret_Key, PCS_1) in
+        let TP_Signature = Sign (Trusted_Party_Secret_Key,
+                              ( Signature_1, Signature_2 )) in
+        Trusted_Party_State := ( Resolved_2, TP_Signature );
+        unlock (Trusted_Party_State);
+        out (Internet, TP_Signature) .
+
+let Stateless_Resolve_1_Process =
+  in (Internet, ( Command,
+                  ( Signature_1, PCS_2 )));
+  let Contract = Check_Get_Message (Public_Key_1, Signature_1) in
+  if Contract = Bogus_Contract then
+    if Check_PCS (Contract,
+                  Public_Key_2,
+                  Public_Key_1,
+                  Public_Key (Trusted_Party_Secret_Key),
+                  PCS_2) = OK
+    then
+      lock (Trusted_Party_State);
+      read Trusted_Party_State as ( Current_Status, Current_Signatures );
+      if Current_Status = Resolved_1 then
+        unlock (Trusted_Party_State);
+        out (Internet, Current_Signatures)
+      else if Current_Status = Init then
+        let Signature_2 = Convert_PCS (Trusted_Party_Secret_Key, PCS_2) in
+        let TP_Signature = Sign (Trusted_Party_Secret_Key,
+                              ( Signature_1, Signature_2 )) in
+        Trusted_Party_State := ( Resolved_1, TP_Signature );
+        unlock (Trusted_Party_State);
+        out (Internet, TP_Signature) .
+
+process Trusted_Party
diff --git a/examples/pi/state/security-device.pi b/examples/pi/state/security-device.pi
new file mode 100644
index 0000000..97aaeb4
--- /dev/null
+++ b/examples/pi/state/security-device.pi
@@ -0,0 +1,67 @@
+(* This is a model of a security device that can be set to work in two modes:
+   "left" mode and "right" mode". The device can be configured only once.
+   The device can then be sent pairs of secrets (a,b) encrypted with its public key.
+   In "left" mode, the device will output a, while in "right" mode it will output b. *)
+
+param verboseClauses = short.
+param propagateState = true.
+param grounding = true.
+
+(* Channel on which left or right is sent to configure the device. *)
+free config.
+
+(* Channel on which the encrypted secrets are sent to the device,
+   and the decrypted secrets are returned. *)
+free decryption.
+
+(* Channel to publish values. *)
+free broadcast.
+
+free unconfigured.
+free left.
+free right.
+
+(* Asymmetric encryption. *)
+fun pk/1.
+fun aenc/3.
+reduc adec(k, aenc(pk(k), random, plaintext)) = plaintext.
+
+(* The device is initially configured to neither "left" nor "right" mode. *)
+cell device_mode := unconfigured.
+
+(* There should not exist a state in which the attacker can know both
+   left_secret and right_secret (from the source_of_secrets process). *)
+query attacker:vs, (left_secret, right_secret).
+
+let device =
+    (* The device broadcasts its public key. *)
+    ! out(broadcast, pk(k)) |
+
+    ! (
+        in(config, new_mode);
+        lock(device_mode);
+        read device_mode as ymode;
+        if ymode = unconfigured then
+            if new_mode = left then device_mode := new_mode; unlock(device_mode)
+            else if new_mode = right then device_mode := new_mode; unlock(device_mode)
+    ) |
+
+    ! (
+        in(decryption, secrets);
+        let (lsecret, rsecret) = adec(k, secrets) in
+        read device_mode as ymode;
+        if ymode = left then out(decryption, lsecret)
+        else if ymode = right then out(decryption, rsecret)
+    )
+.
+
+let source_of_secrets =
+    new random;
+    new left_secret;
+    new right_secret;
+    out(broadcast, aenc(pk(k), random, (left_secret, right_secret)))
+.
+
+process
+    new k;
+    device | ! source_of_secrets
diff --git a/src/display.ml b/src/display.ml
index 8f19c22..cf74b1a 100644
--- a/src/display.ml
+++ b/src/display.ml
@@ -30,6 +30,18 @@ open Pitypes
 
 type cl = CFun | CName | CVar | CPred | CType | CExplain | CKeyword | CConn
 
+(* Convert the integer n into a string corresponding to (n+1)-th *)
+
+let order_of_int n = 
+  (string_of_int (n+1)) ^ 
+  (
+  if (n>=10) && (n<14) then "th" else
+  match (n+1) mod 10 with
+  | 1 -> "st"
+  | 2 -> "nd"
+  | 3 -> "rd"
+  | _ -> "th")
+
 module type LangSig =
 sig
 val indentstring : string
@@ -516,11 +528,13 @@ let concl upper concl tag =
       print_string (if upper then "The message " else "the message ");
       begin
 	match concl with
-	  Pred({p_info = [Attacker(n,_)]} as p, [v]) ->
+	  Pred({p_info = [Attacker(n,_)]} as p, args) ->
+	    let phi, [v] = Lists.head_tail args 1 in
 	    term v;
 	    print_string " may be sent to the attacker";
 	    display_phase p
-	| Pred({p_info = [Mess(n,_)]} as p, [vc;v]) ->
+	| Pred({p_info = [Mess(n,_)]} as p, args) ->
+	    let phi, [vc; v] = Lists.head_tail args 2 in
 	    term v;
 	    print_string " may be sent on channel ";
 	    term vc;
@@ -535,16 +549,37 @@ let concl upper concl tag =
 	    term v;
 	    print_string " may be sent on channel ";
 	    term vc;
-            print_string " (resp. message ";
+	        print_string " (resp. message ";
 	    term v';
 	    print_string " on channel ";
 	    term vc';
- 	    print_string ")";
+	    print_string ")";
 	    display_phase p
 	| _ -> Parsing_helper.internal_error "Unexpected conclusion for OutputTag"
       end;
       print_string " at output ";
       Lang.display_occ occ
+  | AssignmentTag(cell_indices) :: _ ->
+      begin
+        match concl with
+          Pred(p, args) ->
+            let phi = fst (Lists.head_tail args (
+              match p with
+                  { p_info = [Attacker(_,_)]} -> 1
+                | { p_info = [Mess(_,_)]} -> 2
+                | _ -> Parsing_helper.internal_error "Unexpected conclusion for AssignmentTag"
+            )) in
+            let first = (ref true) in
+            (List.iter
+              (fun cell_index ->
+                (print_string ((if (! first) && upper then "The" else if (! first) then "the" else " and the") ^ " cell "
+                  ^ (fst (List.nth (! Param.cells) cell_index))
+                  ^ " may be assigned the value "));
+                (term (List.nth phi cell_index));
+                first := false)
+              cell_indices)
+        | _ -> Parsing_helper.internal_error "Unexpected conclusion for AssignmentTag"
+      end;
   | TestUnifTag occ :: _ | TestUnifTag2 occ :: _ ->
       begin
 	print_string (if upper then "The attacker can make a distinguishing test at " else "the attacker can make a distinguishing test at ");
@@ -732,6 +767,27 @@ let rec display_hyp hyp tag =
   | (h, OutputTag _ :: t) | (h, InsertTag _ :: t) | (h, LetFilterTag _ :: t)
   | (h, BeginEvent _ :: t) ->
       display_hyp h t
+  | (m::h, AssignmentTag(_) :: t) -> display_hyp h t
+  | (m::h, ReadTag(cell_indices) :: t) ->
+    begin
+      display_hyp h t;
+      begin
+        match m with
+          Pred({p_info = [Mess(n,_)]}, args) ->
+            begin
+              let phi, [vc; vm] = (Lists.head_tail args 2) in
+              (List.iter
+                (fun cell_index ->
+                  (print_string ("the cell " ^ (fst (List.nth (! Param.cells) cell_index))
+                    ^ " is in the "));
+                  (display_term (List.nth phi cell_index));
+                  (print_string " state, "))
+                cell_indices)
+            end
+        | _ -> Parsing_helper.internal_error "Unexpected hypothesis for ReadTag"
+      end;
+      newline ()
+    end
   | (h, ReplTag _ :: t) ->
       if !Param.non_interference then
 	if !Param.key_compromise == 1 then
@@ -748,14 +804,16 @@ let rec display_hyp hyp tag =
       display_hyp h t;
       begin
 	match m with
-	  Pred({p_info = [Attacker(n,_)]} as p, [v]) ->
+	  Pred({p_info = [Attacker(n,_)]} as p, args) ->
+	    let phi, [v] = Lists.head_tail args 1 in
 	    print_string "the message ";
 	    display_term v;
 	    print_string " is received from the attacker";
 	    display_phase p;
 	    print_string " at input ";
 	    Lang.display_occ occ
-	| Pred({p_info = [Mess(n,_)]} as p, [vc;v]) ->
+	| Pred({p_info = [Mess(n,_)]} as p, args) ->
+	    let phi, [vc; v] = Lists.head_tail args 2 in
 	    print_string "the message ";
 	    display_term v;
 	    print_string " is received on channel ";
@@ -837,6 +895,7 @@ let rec empty_hyp hyp tags =
   | (h, LetTag _ :: t) | (h, InputPTag _ :: t) | (h, OutputPTag _ :: t) 
   | (h, OutputTag _ :: t) | (h, LetFilterTag _ :: t) | (h, InsertTag _ :: t) 
   | (h, BeginEvent _ :: t) -> empty_hyp h t
+  | (_::h, AssignmentTag _ :: t) -> empty_hyp h t
   | (h, ReplTag _ :: t) ->
       if !Param.non_interference then
 	if !Param.key_compromise == 1 then
@@ -873,7 +932,7 @@ let display_rule_num ((hyp,concl,hist,constra) as rule) =
 	      display_phase p;
 	      print_string ".)"
 	  | Apply(Proj(f,n),p) ->
-	      print_string ("(The attacker applies the " ^ (string_of_int n) ^ "th inverse of function ");
+	      print_string ("(The attacker applies the " ^ (order_of_int n) ^ " inverse of function ");
 	      display_function_name f;
 	      display_phase p;
 	      print_string ".)"
@@ -927,7 +986,7 @@ let display_rule_num ((hyp,concl,hist,constra) as rule) =
 	  | TestUnif ->
 	      print_string "(The attacker can test whether these terms unify.)"
 	  | ProcessRule(tags, _) | ProcessRule2(tags, _, _) -> 
-	      if empty_hyp hyp tags && constra == [] then
+	      if (empty_hyp hyp tags) && (constra == []) then
 		begin
 		  print_string "(";
 		  Std.concl true concl tags;
@@ -1089,7 +1148,7 @@ let rec may_have_else = function
   | Repl(p,_) -> may_have_else p
   | Test _ | Let _ | LetFilter _ -> true
   | Restr(_,p,_) | Event(_,p,_) | Output(_,_,p,_) | Input(_,_,p,_) | Insert(_,p,_) | Get(_,_,p,_) 
-  | Phase(_,p,_) -> may_have_else p
+  | Phase(_,p,_) | Assign(_,p) | ReadAs(_,p) | Lock(_,p) | Unlock(_,p) -> may_have_else p
 
 let display_proc show_occ align proc =
   let display_occ occ =
@@ -1283,6 +1342,31 @@ let display_proc show_occ align proc =
 	  end
 	else
 	  display_process align p
+    | Assign(pairs, p) ->
+        (print_string align);
+        (display_list print_string "," (fst (List.split pairs)));
+        (print_string " := ");
+        (display_list display_term "," (snd (List.split pairs)));
+        display_opt_process align p
+    | ReadAs(pairs, p) ->
+        (print_string align);
+        (print_string "read ");
+        (display_list print_string "," (fst (List.split pairs)));
+        (print_string " as ");
+        (display_list display_pattern "," (snd (List.split pairs)));
+        display_opt_process align p
+    | Lock(cells, p) ->
+        (print_string align);
+        (print_string "lock(");
+        (display_list print_string "," cells);
+        (print_string ")");
+        (display_opt_process align p)
+    | Unlock(cells, p) ->
+        (print_string align);
+        (print_string "unlock(");
+        (display_list print_string "," cells);
+        (print_string ")");
+        (display_opt_process align p)
   and display_opt_process align p =
     match p with
       Nil -> newline()
@@ -1459,10 +1543,11 @@ let display_step_low n =
     end
 
 let display_attacker_fact = function
-    Pred({p_info = [Attacker(n,_)]}, [v]) ->
+    Pred({p_info = [Attacker(n,_)]}, args) ->
+      let phi, [v] = Lists.head_tail args 1 in
       WithLinks.term v;
       if n > 0 then 
-	print_string (" in phase " ^ (string_of_int n))
+    print_string (" in phase " ^ (string_of_int n))
   | Pred({p_info = [AttackerBin(n,_)]}, [v;v']) ->
       WithLinks.term v;
       print_string " (resp. ";
@@ -1567,6 +1652,8 @@ let display_hyp_spec = function
   | OutputPTag o -> print_string "op"; print_string (string_of_int o)
   | InsertTag o ->  print_string "it"; print_string (string_of_int o)
   | GetTag o ->  print_string "gt"; print_string (string_of_int o)
+  | AssignmentTag _ -> print_string "assign"
+  | ReadTag _ -> print_string "read"
 
 let rec display_hyp hyp hl tag =
   match (hyp, hl, tag) with
@@ -1583,6 +1670,27 @@ let rec display_hyp hyp hl tag =
   | (h, hl, OutputPTag _ :: t) | (h, hl, BeginEvent _ :: t)
   | (h, hl, OutputTag _ :: t) | (h, hl, InsertTag _ :: t) ->
       display_hyp h hl t
+  | (m::h, _::hl, AssignmentTag(_) :: t) -> display_hyp h hl t
+  | (m::h, _::hl, ReadTag(cell_indices) :: t) ->
+    begin
+      display_hyp h hl t;
+      begin
+        match m with
+          Pred({p_info = [Mess(n,_)]}, args) ->
+            begin
+              let phi, [vc; vm] = (Lists.head_tail args 2) in
+              (List.iter
+                (fun cell_index ->
+                  (print_string ("the cell " ^ (fst (List.nth (! Param.cells) cell_index))
+                    ^ " is in the "));
+                  (display_term (List.nth phi cell_index));
+                  (print_string " state, "))
+                cell_indices)
+            end
+        | _ -> Parsing_helper.internal_error "Unexpected hypothesis for ReadTag"
+      end;
+      newline ()
+    end
   | (h, hl, ReplTag _ :: t) ->
       if !Param.non_interference then
 	if !Param.key_compromise == 1 then
@@ -1619,7 +1727,8 @@ let rec display_hyp hyp hl tag =
       display_hyp h hl t;
       begin
 	match m with
-	  Pred({p_info = [Attacker(n,_)]} as p, [v]) ->
+	  Pred({p_info = [Attacker(n,_)]} as p, args) ->
+	    let phi, [v] = Lists.head_tail args 1 in
 	    print_string "The message ";
 	    WithLinks.term v;
 	    print_string " that the attacker may have";
@@ -1627,7 +1736,8 @@ let rec display_hyp hyp hl tag =
 	    display_step_low s;
 	    print_string " may be received at input ";
 	    Lang.display_occ occ
-	| Pred({p_info = [Mess(n,_)]} as p, [vc;v]) ->
+	| Pred({p_info = [Mess(n,_)]} as p, args) ->
+	    let phi, [vc; v] = Lists.head_tail args 2 in
 	    print_string "The message ";
 	    WithLinks.term v;
 	    print_string " that may be sent on channel ";
@@ -1655,7 +1765,7 @@ let rec display_hyp hyp hl tag =
 	    WithLinks.term v';
 	    print_string " on channel ";
 	    WithLinks.term vc';
- 	    print_string ")";
+	    print_string ")";
 	    display_phase p;
 	    display_step_low s;
 	    print_string " may be received at input ";
@@ -2050,18 +2160,6 @@ let display_abbrev_table l =
   print_string "Abbreviations:";
   display_item_list display_eq (List.rev l)
 
-(* Convert the integer n into a string corresponding to (n+1)-th *)
-
-let order_of_int n = 
-  (string_of_int (n+1)) ^ 
-  (
-  if (n>=10) && (n<14) then "th" else
-  match (n+1) mod 10 with
-  | 1 -> "st"
-  | 2 -> "nd"
-  | 3 -> "rd"
-  | _ -> "th")
-
 (* Display reduction step *)
 
 let display_step = function
diff --git a/src/display.mli b/src/display.mli
index 18d83a6..b7b9c90 100644
--- a/src/display.mli
+++ b/src/display.mli
@@ -134,6 +134,8 @@ val display_eq_query : Pitypes.eq_query -> unit
 val display_function_name : funsymb -> unit
 val display_phase : predicate -> unit
 
+val display_format : format -> unit
+
 
 module WithLinks :
   sig
diff --git a/src/lists.ml b/src/lists.ml
new file mode 100644
index 0000000..c03e93e
--- /dev/null
+++ b/src/lists.ml
@@ -0,0 +1,21 @@
+let head_tail lst n =
+    let head = ref [] in
+    let tail = ref [] in
+    for i = (List.length lst) downto 1 do
+        if (List.length lst) - i < n then
+            tail := (List.nth lst (i-1)) :: !tail
+        else
+            head := (List.nth lst (i-1)) :: !head
+    done;
+    !head, !tail
+
+let update_list lst n new_value =
+    let i = ref (-1) in
+    List.map (fun x ->
+        i := !i + 1;
+        if !i == n then
+            new_value
+        else
+            x)
+        lst
+
diff --git a/src/lists.mli b/src/lists.mli
new file mode 100644
index 0000000..86bb952
--- /dev/null
+++ b/src/lists.mli
@@ -0,0 +1,12 @@
+(* [a;b;c;d;e] 2 -> [a;b;c], [d;e]
+   Split a list into two.
+   The second list contains the n last elements of lst.
+   The first list contains all the other elements.
+   I.e. head_tail lst n will break the n last elements off lst into
+   a separate list. *)
+
+val head_tail : 'a list -> int -> 'a list * 'a list
+
+(* Return a copy of lst with item n (range 0..length-1)
+   replaced with new_value. *)
+val update_list : 'a list -> int -> 'a -> 'a list
diff --git a/src/main.ml b/src/main.ml
index 8d2f9ab..885b2c7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -366,6 +366,8 @@ let anal_file s =
 	    then Parsing_helper.user_error "Queries are incompatible with choice\n";
 	    if (!Param.key_compromise != 0) then
 	      Parsing_helper.user_error "Key compromise is incompatible with choice\n";
+	    if (!Param.has_state = true) then
+	      Parsing_helper.user_error "Cells are incompatible with choice\n";
 
 	    print_string "-- Observational equivalence"; print_newline();
 	    if !Param.html_output then
diff --git a/src/optimisation.ml b/src/optimisation.ml
new file mode 100644
index 0000000..5d9bcf0
--- /dev/null
+++ b/src/optimisation.ml
@@ -0,0 +1,435 @@
+open Types
+
+type hyp_selection = Keep | Discard
+
+let rec discard_hypotheses hypotheses tags = begin
+  match (hypotheses, tags) with
+    | (sel,h1)::h, TestUnifTag _   :: t
+    | (sel,h1)::h, AssignmentTag _ :: t
+    | (sel,h1)::h, ReadTag _       :: t
+    | (sel,h1)::h, InputTag _      :: t 
+    | (sel,h1)::h, GetTag _        :: t ->
+      begin
+        let (hypotheses', tags') = (discard_hypotheses h t) in
+        match sel with
+          | Keep -> (h1 :: hypotheses', (List.hd tags) :: tags')
+          | Discard -> (hypotheses', tags')
+      end
+    | h, TestUnifTag2 _ :: t
+    | h, TestTag      _ :: t
+    | h, LetTag       _ :: t
+    | h, InputPTag    _ :: t
+    | h, OutputPTag   _ :: t
+    | h, BeginEvent   _ :: t
+    | h, OutputTag    _ :: t
+    | h, InsertTag    _ :: t
+    | h, ReplTag      _ :: t
+    | h, LetFilterTag _ :: t ->
+      begin
+        let (hypotheses', tags') = (discard_hypotheses h t) in
+        (hypotheses', (List.hd tags) :: tags')
+      end
+    | (sel,h1)::h, LetFilterFact :: LetFilterTag x :: t ->
+      begin
+        let (hypotheses', tags') = (discard_hypotheses h t) in
+        match sel with
+          | Keep -> (h1 :: hypotheses', LetFilterFact :: LetFilterTag x :: tags')
+          | Discard -> (hypotheses', tags')
+      end
+    | (sel,Out(a,b))::h, BeginFact :: BeginEvent x :: t ->
+      begin
+        let (hypotheses', tags') = (discard_hypotheses h t) in
+        match sel with
+          | Keep -> (Out(a,b) :: hypotheses', BeginFact :: BeginEvent x :: tags')
+          | Discard -> (hypotheses', tags')
+      end
+    | [], [] -> [], []
+    | _ ->
+      begin
+        (Display.Text.display_list
+          (fun (sel,h) ->
+            (Display.Text.WithLinks.fact h))
+          " & " hypotheses);
+        Display.Text.newline();
+        Parsing_helper.internal_error "Unexpected hypothesis"
+      end
+end
+
+let is_stateful = function
+  | Pred({p_info = [Attacker(_,_) | Mess(_,_)]},args) -> true
+  | _ -> false
+
+let split_states = function
+  | Pred({p_info = [Attacker(_,_)]},args) -> Lists.head_tail args 1
+  | Pred({p_info = [Mess(_,_)]},args) -> Lists.head_tail args 2
+
+let states hyp = fst (split_states hyp)
+
+let non_states hyp = snd (split_states hyp)
+
+let replace_states hyp new_states =
+  match hyp with
+    | Pred({p_info = [Attacker(_,_)]} as p,args) -> Pred(p, new_states @ snd (Lists.head_tail args 1))
+    | Pred({p_info = [Mess(_,_)]} as p,args) -> Pred(p, new_states @ snd (Lists.head_tail args 2))
+
+let state cell_index hyp =
+  (List.nth (states hyp) (cell_index - 1))
+
+let rec appears_in_term x = function
+  | Var y -> x = y
+  | FunApp(f,args) -> List.exists (appears_in_term x) args
+
+let appears_in_hyp x = begin function
+  | Pred(_, args) -> (List.exists (appears_in_term x) args)
+  | Out(a, b) -> begin
+      ((appears_in_term x a)
+       || (List.exists
+            (fun (b,t) -> ((appears_in_term x t) || (b = x)))
+            b))
+  end
+end
+
+(* True if x is in hyp, unless as cell i. *)
+let appears_in_non_state i x = begin function
+  | Pred(p, args) as hyp -> begin
+      (if (is_stateful hyp) then
+      begin
+        let cell_index = (ref (-1)) in
+        (* Check all args. The non-state args have indices greater
+           than the highest cell index, so the comparison is fine. *)
+        (List.exists
+          (fun y ->
+            (incr cell_index);
+            (if (((! cell_index) = i) && (y = (Var x))) then false
+            else (appears_in_term x y)))
+          args)
+      end else begin
+        (appears_in_hyp x hyp)
+      end)
+  end
+  | Out(a,b) -> begin
+      ((appears_in_term x a)
+       || (List.exists
+            (fun (b,t) ->
+              ((appears_in_term x t)
+               || (b = x)))
+            b))
+  end
+end
+
+(* True if x appears as cell_index in one of hyps. *)
+let appears_as_cell cell_index term hyps =
+  (List.exists
+    (fun hyp ->
+      (is_stateful hyp) && ((state cell_index hyp) = term))
+    hyps)
+
+let rec propagate_state hypotheses conclusion constraints = begin
+  match hypotheses with
+    | [] -> hypotheses, conclusion, constraints (* do nothing *)
+    | rightmost :: candidates -> begin
+      if (not (is_stateful rightmost)) then
+      begin
+        (* Don't use this non-stateful hypothesis as a source of state.
+           Use the next one instead. *)
+        let (hypotheses', conclusion', constraints')
+          = (propagate_state candidates conclusion constraints) in
+        (rightmost :: hypotheses', conclusion', constraints')
+      end else begin
+        (rightmost :: List.map (
+          fun h ->
+            if (is_stateful h) then
+            begin
+              let cell_index = ref (-1) in
+              if (List.for_all
+                (fun vs ->
+                  (incr cell_index);
+                  (match vs with
+                    | Var x -> begin                    (* h's states are all variables *)
+                      (not (appears_in_hyp x conclusion)) (* that don't appear in the conclusion *)
+                      && (not (List.exists (appears_in_non_state !cell_index x) hypotheses))
+                                                        (* and don't appear in the
+                                                           non-state part, or in a
+                                                           different cell, of another
+                                                           hypothesis *)
+                    end
+                    | _ -> false
+                  ))
+                (states h))
+              then begin
+                (replace_states h (states rightmost))
+              end else begin
+                h
+              end
+            end else begin
+              h
+            end
+          ) candidates), conclusion, constraints
+        end
+    end
+end
+
+let enumerate =
+  let rec inner i = function
+    | [] -> []
+    | hd :: tl -> (i, hd) :: inner (i+1) tl
+  in inner 1
+
+and equal_term_lists a b =
+  (a == b) || (List.for_all2 Termslinks.equal_terms_with_links a b)
+
+let dejunk hypotheses tags conclusion =
+
+  let rec inner result = begin function
+    | [] -> result
+    | this_hypothesis :: remaining_hypotheses ->
+        (if (is_stateful this_hypothesis) then begin
+
+          let kept = (List.map snd
+                        (List.filter
+                          (function
+                            | (Keep, _) -> true
+                            | (Discard, _) -> false)
+                          result))
+          in
+
+          let this_states = states this_hypothesis in
+          (* this_states must appear in another hypothesis. *)
+          let states_are_here hyp = ((is_stateful hyp) && (equal_term_lists (states hyp) this_states)) in
+          (if (List.exists states_are_here kept
+              || List.exists states_are_here remaining_hypotheses)
+          (* The non-state terms must all be variables
+             that appear nowhere else in the clause. *)
+          && (List.for_all (
+              function
+                | Var x ->
+                    let x_not_in term = (not (appears_in_hyp x term)) in
+                    (List.for_all x_not_in kept)
+                    && (List.for_all x_not_in remaining_hypotheses)
+                    && x_not_in conclusion
+                | _ -> false
+              ) (non_states this_hypothesis)
+            ) then
+          begin
+            (* This hypothesis can be removed. *)
+            (inner ((Discard, this_hypothesis) :: result) remaining_hypotheses)
+          end else begin
+            (inner ((Keep, this_hypothesis) :: result) remaining_hypotheses)
+          end)
+        end else begin
+          (inner ((Keep, this_hypothesis) :: result) remaining_hypotheses)
+        end)
+  end in
+  let (hypotheses', tags')
+    = (discard_hypotheses
+        (List.rev (inner [] hypotheses)) tags) in
+  (hypotheses', tags', conclusion)
+
+let rec is_ground = function
+  | FunApp({ f_cat = (Name _) }, _) -> true
+  | FunApp(f, args) -> (List.for_all is_ground args)
+  | _ -> false
+
+exception Not_variable of string
+
+let key_binder binder = (binder.sname, binder.vname)
+
+let dump_item (a, b) =
+  (print_string (a ^ "_" ^ (string_of_int b) ^ " "))
+
+let dump_list l =
+  (print_string "Listing: ");
+  (List.iter dump_item l);
+  (print_endline "")
+
+let include_item listref newitem =
+  (if (not (List.exists (fun x -> (x = newitem)) (! listref))) then
+  begin
+    (listref := (newitem :: (! listref)));
+  end)
+
+(* (keys => [a; b; c], values => [1; 2]) ->
+     { a->1, b->1, c->1 }; { a->1, b->1, c->2 };
+     { a->1, b->2, c->1 }; { a->1, b->2, c->2 } etc.
+   and call produce for each mapping. *)
+let cartesian_power keys values produce =
+  let current = (Hashtbl.create (List.length keys)) in
+  let rec iterate = begin function
+    | 0 -> produce current
+    | keyi ->
+      let key = (List.nth keys (keyi-1)) in
+      (List.iter
+        (fun value ->
+          (Hashtbl.replace current key value);
+          (iterate (keyi-1)))
+        values)
+  end in
+  (iterate (List.length keys))
+
+(* Find variables that are to be made ground. *)
+let to_be_ground cell_index hyps = begin
+  let collected = (ref []) in
+  let rec collect = begin function
+    | Var x -> (include_item collected (key_binder x))
+    | _ -> ()
+  end in
+  (List.iter
+    (fun hyp -> begin
+      if (is_stateful hyp) then
+      begin
+        (collect (state cell_index hyp))
+      end
+    end)
+    hyps);
+  (! collected)
+end
+
+let look_up table x = begin
+  if (Hashtbl.mem table (key_binder x)) then
+  begin
+    (Hashtbl.find table (key_binder x))
+  end else begin
+    (Var x)
+  end
+end
+
+let rec substitute_in_term table = begin function
+  | Var x -> (look_up table x)
+  | FunApp(f, args) -> FunApp(f, (List.map (substitute_in_term table) args))
+end
+
+let substitute_in_hyp table = begin function
+  | Pred(p, args) -> (Pred(p, (List.map (substitute_in_term table) args)))
+  | Out(a, b) -> begin
+      Out((substitute_in_term table a),
+          (List.map
+            (fun (b, t) -> begin
+              (b, (substitute_in_term table t))
+            end)
+            b))
+  end
+end
+
+let substitute_in_hyps table hyps =
+  (List.map (substitute_in_hyp table) hyps)
+
+let substitute_in_constra table = function
+  | Neq(lhs, rhs) ->
+      (Neq((substitute_in_term table lhs), (substitute_in_term table rhs)))
+
+let substitute_in_constra1 table constra1 =
+  (List.map (substitute_in_constra table) constra1)
+
+let substitute_in_constra2 table constra2 =
+  (List.map (substitute_in_constra1 table) constra2)
+
+let grounding_for_cell cell_index clauses = begin
+  (* Find if grounding is valid.
+     Grounding is valid if, for all clauses C:
+       a) the conclusion of C has a ground term for cell s; or
+       b) the conclusion of C has a term t for cell s, and that term
+          appears as a term for the same cell in one of the hypotheses of C. *)
+  let cell_values = (ref []) in (* finite set of values the cell can take *)
+  (if
+    (List.for_all
+      (fun (hypotheses, conclusion, history, constraints) ->
+        if (is_stateful conclusion) then
+        begin
+          let conclusion_state = (state cell_index conclusion) in
+          (if (is_ground conclusion_state) then
+          begin
+            (include_item cell_values conclusion_state);
+            true
+          end else if (appears_as_cell cell_index conclusion_state hypotheses) then
+          begin
+            true
+          end else begin
+            false
+          end)
+        end else begin
+          (* Conclusion cannot introduce new states - it has no state. *)
+          true
+        end)
+      clauses) then
+  begin
+    (* Grounding this cell is possible. The finite set of possible values
+       for this cell is now in cell_values. *)
+    begin
+      (print_endline
+        ("Grounding is possible for cell " ^ (fst (List.nth (!Param.cells) (cell_index-1)))));
+      let new_clauses = (ref []) in
+      (List.iter
+        (fun (hypotheses, conclusion, history, constraints) ->
+          let variables = (to_be_ground cell_index hypotheses) in
+          (* Note that the conclusion contains no variables to make ground. *)
+          (cartesian_power variables (! cell_values)
+            (fun tab ->
+              (new_clauses :=
+                (((substitute_in_hyps tab hypotheses),
+                  (substitute_in_hyp tab conclusion),
+                  history, (* TODO? *)
+                  substitute_in_constra2 tab constraints)
+                 :: (! new_clauses))))))
+        clauses);
+      (print_endline "Grounding is done.");
+      true, (! new_clauses)
+    end
+  end else begin
+    false, clauses
+  end)
+end
+
+let find_loops clauses =
+  (print_endline "Searching for state cycles...");
+  let rec search_for stack phi = (* Good candidate for memoising *)
+    (* Check stack for loops. *)
+    if (match stack with [] -> false | x::tl -> (equal_term_lists phi x)) then
+      (* We followed an x -> x transition (i.e. no state change).
+         Skip this. *)
+      false
+    else if (List.exists (equal_term_lists phi) stack) then
+    begin
+      (print_string "State loop found: ");
+      (Display.Text.display_list
+        (fun phi' ->
+          print_string "(";
+          Display.Text.display_term_list phi';
+          print_string ")")
+        " -> " (List.rev (phi :: stack)));
+      print_endline "";
+      true
+    end else begin
+      (* Find clauses with phi in a hypothesis. *)
+      let rec loop = function
+        | [] -> false
+        | (hypotheses, conclusion, history, constraints) :: tail -> begin
+            if (is_stateful conclusion) then
+            begin
+              if (List.exists
+                    (fun hyp -> (is_stateful hyp) && (equal_term_lists phi (states hyp)))
+                      (* XXX: This must be unification, rather than equality,
+                         if we don't have the guarantee that all states are ground. *)
+                    hypotheses)
+              then
+                search_for (phi :: stack) (states conclusion) || loop tail
+              else
+                loop tail
+            end else loop tail
+          end
+      in loop clauses
+    end
+  in
+  let phi0 = (List.map (fun (_, init_state) -> init_state) !Param.cells) in
+  if not (search_for [] phi0) then print_endline "States are free of cycles."
+
+let grounding clauses = begin
+  let current_clauses = (ref clauses) in
+  let all_are_ground = ref true in
+  (for i = 1 to (List.length (! Param.cells)) do
+    let did, new_clauses = (grounding_for_cell i (! current_clauses)) in
+    all_are_ground := !all_are_ground && did;
+    current_clauses := new_clauses
+  done);
+  if !all_are_ground then (find_loops (! current_clauses));
+  (! current_clauses)
+end
diff --git a/src/optimisation.mli b/src/optimisation.mli
new file mode 100644
index 0000000..1fe29f0
--- /dev/null
+++ b/src/optimisation.mli
@@ -0,0 +1,22 @@
+type hyp_selection = Keep | Discard
+
+val discard_hypotheses :
+     (hyp_selection * Types.fact) list
+  -> Types.hypspec list
+  -> Types.fact list * Types.hypspec list
+
+val propagate_state : Types.fact list
+                   -> Types.fact
+                   -> Types.constraints list list
+                   -> ( Types.fact list
+                      * Types.fact
+                      * Types.constraints list list )
+
+val dejunk : Types.fact list
+          -> Types.hypspec list
+          -> Types.fact
+          -> ( Types.fact list
+             * Types.hypspec list
+             * Types.fact )
+
+val grounding : Types.reduction list -> Types.reduction list
diff --git a/src/param.ml b/src/param.ml
index b436849..33845fb 100644
--- a/src/param.ml
+++ b/src/param.ml
@@ -105,6 +105,12 @@ let redundancy_test = ref SimpleRed
 
 let move_new = ref false
 
+type output_modes = PhiOutput | HypothesisOutput | OldHeuristicOutput | HeuristicOutput
+let output_mode = ref PhiOutput
+let dejunk_hypotheses = ref false
+let propagate_state = ref false
+let grounding = ref false
+
 let redundant_hyp_elim = ref true
 let redundant_hyp_elim_begin_only = ref true
 
@@ -163,6 +169,16 @@ let common_parameters p ext v =
   | "simplifyDerivation", _ -> boolean_param simplify_derivation p ext v
   | "displayDerivation", _ -> boolean_param display_derivation p ext v
   | "abbreviateDerivation", _ -> boolean_param abbreviate_derivation p ext v
+  | "outputMode", S("Phi",_) -> output_mode := PhiOutput
+  | "outputMode", S("Hypothesis",_) -> output_mode := HypothesisOutput
+  | "outputMode", S("OldHeuristic",_) -> output_mode := OldHeuristicOutput
+  | "outputMode", S("Heuristic",_) -> output_mode := HeuristicOutput
+  | "dejunk", S(("false"|"no"),_) -> dejunk_hypotheses := false
+  | "dejunk", S(("true"|"yes"),_) -> dejunk_hypotheses := true
+  | "propagateState", S(("false"|"no"),_) -> propagate_state := false
+  | "propagateState", S(("true"|"yes"),_) -> propagate_state := true
+  | "grounding", S(("false"|"no"),_) -> grounding := false
+  | "grounding", S(("true"|"yes"),_) -> grounding := true
   | _, _ -> Parsing_helper.input_error ("Bad parameter " ^ p ^ "=" ^ 
 			 (match v with S (s,_) -> s | I n -> string_of_int n)) ext
 
@@ -196,7 +212,7 @@ let build_pred = function
     Attacker(i,t) -> 
       { p_name = "attacker" ^ (get_type_suffix t) ^ (get_suffix i); 
 	p_type = [t];
-	p_prop = pred_ANY + pred_TUPLE + pred_ATTACKER;
+	p_prop = pred_ANY + pred_ATTACKER;
 	p_info = [Attacker(i,t)] }
   | Mess(i,t) ->
       { p_name = "mess" ^ (get_type_suffix t) ^ (get_suffix i); 
@@ -339,6 +355,8 @@ let all_types = ref [channel_type; bitstring_type; bool_type]
 let fun_decls = ((Hashtbl.create 49) : (string, funsymb) Hashtbl.t)
 let pred_env = Hashtbl.create 7
 let freenames = ref ([] : funsymb list)
+let cells = ref []
+let has_state = ref false
 let max_used_phase = ref 0
 let session1 = { f_name = "session1"; 
 		 f_type = [], sid_type;
@@ -348,3 +366,13 @@ let session1 = { f_name = "session1";
 	         f_initial_cat = Eq [] }
 let red_rules = ref []
 let elim_true = ref []
+
+let find_cell_index name =
+  let result = ref (-1) in
+  for i = 0 to (List.length !cells) - 1 do
+    if fst (List.nth !cells i) = name then
+      result := i
+  done;
+  if !result = -1 then
+    Parsing_helper.internal_error ("Cell does not exist: " ^ name);
+  !result
diff --git a/src/param.mli b/src/param.mli
index 68ab3bb..5bd2ed2 100644
--- a/src/param.mli
+++ b/src/param.mli
@@ -122,6 +122,12 @@ val redundancy_test : red_type ref
 
 val move_new : bool ref
 
+type output_modes = PhiOutput | HypothesisOutput | OldHeuristicOutput | HeuristicOutput
+val output_mode : output_modes ref
+val dejunk_hypotheses : bool ref
+val propagate_state : bool ref
+val grounding : bool ref
+
 val redundant_hyp_elim : bool ref
 val redundant_hyp_elim_begin_only : bool ref
 val check_pred_calls : bool ref
@@ -193,8 +199,11 @@ val all_types : Types.typet list ref
 val fun_decls : (string,Types.funsymb) Hashtbl.t
 val pred_env : (string,Types.predicate) Hashtbl.t
 val freenames : Types.funsymb list ref
+val cells : (string * Types.term) list ref
+val has_state  : bool ref
 val max_used_phase : int 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
 
+val find_cell_index : string -> int
diff --git a/src/parsing_helper.ml b/src/parsing_helper.ml
index 41235cf..b9b2e99 100644
--- a/src/parsing_helper.ml
+++ b/src/parsing_helper.ml
@@ -28,7 +28,7 @@
 open Lexing
 
 let internal_error mess =
-  print_string ("Internal error: " ^ mess ^ "\nPlease report bug to Bruno.Blanchet@ens.fr, including input file and output\n");
+  print_string ("Internal error: " ^ mess ^ "\nPlease report bug to j.phillips@cs.bham.ac.uk, including input file and output\n");
   exit 3
 
 (* extent, for error messages *)
diff --git a/src/pilexer.mll b/src/pilexer.mll
index 99de48a..91dc0ea 100644
--- a/src/pilexer.mll
+++ b/src/pilexer.mll
@@ -67,7 +67,12 @@ let keyword_table =
   "phase", PHASE;
   "among", AMONG;
   "weaksecret", WEAKSECRET;
-  "choice", CHOICE ]
+  "choice", CHOICE;
+  "read", READ;
+  "as", AS;
+  "cell", CELL;
+  "lock", LOCK;
+  "unlock", UNLOCK]
 
 }
 
@@ -110,6 +115,7 @@ rule token = parse
 | ':' { COLON }
 | '&' { WEDGE }
 | "->" { RED } 
+| ":=" { ASSIGN }
 | "<->" { EQUIV } 
 | "<=>" { EQUIVEQ } 
 | "<>" { DIFF }
diff --git a/src/piparser.mly b/src/piparser.mly
index 6f2bb8e..5d65a3f 100644
--- a/src/piparser.mly
+++ b/src/piparser.mly
@@ -84,6 +84,12 @@ exception Syntax
 %token PHASE
 %token AMONG
 %token WEAKSECRET
+%token ASSIGN
+%token READ
+%token AS
+%token CELL
+%token LOCK
+%token UNLOCK
 
 /* Untyped front-end only */
 %token DATA
@@ -139,6 +145,8 @@ all:
         { (Elimtrue ($2)) :: $4 } 
 |       privateopt FREE neidentseq DOT all
         { (Free($3,$1)) :: $5 }
+|       CELL IDENT ASSIGN term DOT all
+        { Param.has_state := true; (Cell($2,$4)) :: $6 }
 |       CLAUSES clauses all
         { (Clauses($2)) :: $3 }
 |	PROCESS process EOF
@@ -446,6 +454,18 @@ process:
         { PEvent($2, $4, $6) }
 |       PHASE INT optprocess
         { PPhase($2, $3) }
+|       LOCK LPAREN neidentseq RPAREN optprocess
+        { Param.has_state := true; PLock($3, $5) }
+|       LOCK optprocess
+        { Param.has_state := true; PLockAll($2, parse_extent ()) }
+|       UNLOCK LPAREN neidentseq RPAREN optprocess
+        { Param.has_state := true; PUnlock($3, $5) }
+|       UNLOCK optprocess
+        { Param.has_state := true; PUnlockAll($2, parse_extent ()) }
+|       READ neidentseq AS patternseq optprocess
+        { Param.has_state := true; PReadAs((List.combine $2 $4), $5) }
+|       neidentseq ASSIGN netermseq optprocess
+        { Param.has_state := true; PAssign((List.combine $1 $3), $4) }
 
 optprocess:
         SEMI process
diff --git a/src/piptree.mli b/src/piptree.mli
index 9f57dcb..bfadc51 100644
--- a/src/piptree.mli
+++ b/src/piptree.mli
@@ -126,7 +126,12 @@ type process =
   | PLetFilter of ident list * fact_e * process * process
   | PEvent of ident * term_e list * process
   | PPhase of int * process
-
+  | PLock of ident list * process
+  | PUnlock of ident list * process
+  | PLockAll of process * Parsing_helper.extent
+  | PUnlockAll of process * Parsing_helper.extent
+  | PReadAs of (ident * pattern) list * process
+  | PAssign of (ident * term_e) list * process
 
 (* Declarations *)
 
@@ -146,5 +151,6 @@ type decl =
   | Not of (gfact_e * int) * (ident * gterm_e) list
   | Elimtrue of fact_e
   | Free of ident list * bool
+  | Cell of ident * term_e
   | Clauses of clause list
 
diff --git a/src/pisyntax.ml b/src/pisyntax.ml
index a3111ae..ade81e5 100644
--- a/src/pisyntax.ml
+++ b/src/pisyntax.ml
@@ -99,13 +99,23 @@ let check_fun_decl is_tuple (name,ext) arity is_private =
       f_private = is_private;
       f_options = 0 }
 
+(* Environment of a process.
+   May contain function symbols, names and variables.
+   Is a map from strings to the description of the ident *)
+
+type envElement = EFun of funsymb
+                | EVar of binder
+                | EName of funsymb
+
 let get_var env s =
   try 
-    Hashtbl.find env s
+    match (Hashtbl.find env s) with
+        EVar x -> Var x
+      | EName f -> FunApp(f, [])
   with Not_found -> 
     let r = Terms.new_var s Param.any_type in
-    Hashtbl.add env s r;
-    r
+    Hashtbl.add env s (EVar r);
+    Var r
 
 let get_fun (s,ext) arity =
   try
@@ -144,7 +154,7 @@ let rec check_eq_term f_allowed varenv (term,ext) =
 	  f_allowed f ext;
 	  FunApp(f, [])
 	with
-	  Not_found -> Var (get_var varenv s)
+	  Not_found -> get_var varenv s
       end
   | (PFunApp (fi, tlist)) ->
       let f = get_fun fi (List.length tlist) in
@@ -291,16 +301,6 @@ let check_clause = function
       Rules.add_equiv (hyp, concl, -1); (* TO DO should give a real rule number, but that's not easy... *)
       if not select then Terms.add_unsel concl
 
-      
-
-(* Environment of a process.
-   May contain function symbols, names and variables.
-   Is a map from strings to the description of the ident *)
-
-type envElement = EFun of funsymb
-                | EVar of binder
-                | EName of funsymb
-
 let glob_table = Hashtbl.create 7
 
 let init_env () =
@@ -310,6 +310,9 @@ let init_env () =
      Hashtbl.add glob_table s (EFun f)) fun_decls;
    !m 
 
+let all_unlocked () =
+  (List.map (fun _ -> None) (! Param.cells))
+
 let clear_var_env () =
   let list_var = ref [] in
   Hashtbl.iter (fun s v ->
@@ -335,6 +338,9 @@ let add_free_name is_pub s =
   freenames := r :: !freenames;
   r
 
+let add_cell name init_value =
+  Param.cells := (! Param.cells) @ [(name, init_value)]
+
 let get_non_interf_name (s,ext) =
    try
      match Hashtbl.find glob_table s  with
@@ -388,7 +394,7 @@ let rec check_ni_term varenv (term,ext) =
 		  FunApp (r, Terms.var_gen (fst r.f_type))
 	    | EFun _ | EVar _ -> internal_error "should not find var/fun here"
 	  with Not_found ->
-	    Var (get_var varenv s)
+	    get_var varenv s
       end
 | (PFunApp ((s,ext) as fi, tlist)) ->
     let f = get_fun fi (List.length tlist) in
@@ -502,38 +508,77 @@ let get_event_fun s arity ext =
     Hashtbl.add event_fun_table s p;
     p
 
-let rec check_process env = function 
-    PNil -> Nil
+let is_unique lst = begin
+  let rec check = begin function
+    | [] -> true
+    | a :: b :: rest when a = b -> false
+    | a :: rest -> check rest
+  end in
+  (check (List.sort compare lst))
+end
+
+let check_cell_list lst = begin
+  if (not (is_unique (List.map fst lst))) then
+    (input_error "cannot name a cell more than once here"
+      (snd (List.hd lst)))
+end
+
+(* locks : extent option list
+   One entry for each cell.
+   None -> cell is not locked by this process
+   Some ext -> cell was locked at ext *)
+let rec check_process env locks = function
+    PNil ->
+      (for i = 1 to (List.length (! Param.cells)) do
+        (match (List.nth locks (i-1)) with
+          | None -> ()
+          | Some ext ->
+              (input_error ("cell " ^ (fst (List.nth (! Param.cells) (i-1)))
+                ^ " is left locked") ext))
+      done);
+      Nil
   | PPar (p1,p2) -> 
-      let p1' = check_process env p1 in
-      let p2' = check_process env p2 in
+      (for i = 1 to (List.length (! Param.cells)) do
+        (match (List.nth locks (i-1)) with
+          | None -> ()
+          | Some ext ->
+              (input_error "cannot have parallel processes inside a lock" ext))
+      done);
+      let p1' = check_process env locks p1 in
+      let p2' = check_process env locks p2 in
       Par(p1', p2')
   | PRepl p -> 
-      Repl(check_process env p, new_occurrence())
+      (for i = 1 to (List.length (! Param.cells)) do
+        (match (List.nth locks (i-1)) with
+          | None -> ()
+          | Some ext ->
+              (input_error "cannot have a replication inside a lock" ext))
+      done);
+      Repl(check_process env locks p, new_occurrence())
   | PTest((f,_),p1,p2) -> 
       let occ' = new_occurrence() in
       begin
 	match f with
 	  PSimpleFact(pred,l) ->
-	    let p1' = check_process env p1 in
-	    let p2' = check_process env p2 in
+	    let p1' = check_process env locks p1 in
+	    let p2' = check_process_implicit_unlock env locks p2 in
 	    let (pred',l') = check_fl_term env (pred,l) in
 	    LetFilter([], Pred(pred',l'), p1', p2', occ')
 	| PSEqual(t1,t2) ->
-	    let p1' = check_process env p1 in
-	    let p2' = check_process env p2 in
+	    let p1' = check_process env locks p1 in
+	    let p2' = check_process_implicit_unlock env locks p2 in
 	    Test(check_term env t1, check_term env t2,
 		 p1', p2', occ')
 	| PSNeq(t1,t2) ->
-	    let p2' = check_process env p2 in
-	    let p1' = check_process env p1 in
+	    let p2' = check_process_implicit_unlock env locks p2 in
+	    let p1' = check_process env locks p1 in
 	    Test(check_term env t1, check_term env t2,
 		 p2', p1', occ')
       end
   | PLetDef (s,ext) ->
       begin
 	try
-          check_process env (Hashtbl.find pdeftbl s)
+          check_process env locks (Hashtbl.find pdeftbl s)
         with Not_found ->
           input_error ("process " ^ s ^ " not defined") ext
       end
@@ -542,21 +587,21 @@ let rec check_process env = function
       Hashtbl.add glob_table s (EName r);
       if (StringMap.mem s env) && (!Param.tulafale != 1) then
 	input_warning ("identifier " ^ s ^ " rebound") ext;
-      Restr(r, check_process (StringMap.add s (EName r) env) p, 
+      Restr(r, check_process (StringMap.add s (EName r) env) locks p, 
 	    new_occurrence())
   | PInput(tc,pat,p) ->
       let (pat',env') = check_pat env pat in
       Input(check_term env tc, pat',
-	    check_process env' p, new_occurrence())
+	    check_process env' locks p, new_occurrence())
   | POutput(tc,t,p) ->
       Output(check_term env tc,
 	     check_term env t,
-	     check_process env p, new_occurrence())
+	     check_process env locks p, new_occurrence())
   | PLet(pat,t,p,p') ->
       let (pat', env') = check_pat env pat in
       let occ' = new_occurrence() in
-      let p1 = check_process env' p in
-      let p1' = check_process env p' in
+      let p1 = check_process env' locks p in
+      let p1' = check_process_implicit_unlock env locks p' in
       Let(pat',check_term env t, p1, p1', occ')
   | PLetFilter(identlist,(f,ext),p,q) ->
       let (env', vlist) = List.fold_left (fun (env, vlist) (s,e) ->
@@ -575,19 +620,103 @@ let rec check_process env = function
 	  Pred(pred',l')
       in
       let occ' = new_occurrence() in
-      let p' = check_process env' p in
-      let q' = check_process env q in
+      let p' = check_process env' locks p in
+      let q' = check_process env locks q in
       LetFilter(vlist, f', p', q', occ')
   | PEvent((i,ext),l,p) ->
       if !Param.key_compromise == 0 then
 	let f = get_event_fun i (List.length l) ext in
-	Event(FunApp(f, List.map (check_term env) l), check_process env p, new_occurrence())
+	Event(FunApp(f, List.map (check_term env) l), check_process env locks p, new_occurrence())
       else
 	let f = get_event_fun i (1+List.length l) ext in
-	Event(FunApp(f, (Terms.new_var_def Param.any_type) :: (List.map (check_term env) l)), check_process env p, new_occurrence())
+	Event(FunApp(f, (Terms.new_var_def Param.any_type) :: (List.map (check_term env) l)), check_process env locks p, new_occurrence())
   | PPhase(n, p) ->
       let occ' = new_occurrence() in
-      Phase(n, check_process env p, occ')
+      Phase(n, check_process env locks p, occ')
+  | PLock(cells, p) ->
+      (check_cell_list cells);
+      Lock(
+        (List.map fst cells),
+        (check_process env
+          (List.map2
+            (fun old_locked (cell_name, _) ->
+              (List.fold_left
+                (fun new_locked (to_lock, ext) ->
+                  if (cell_name = to_lock) then
+                  begin
+                    (match old_locked with
+                      | None -> ()
+                      | Some _ -> (input_error ("cell " ^ cell_name ^ " is already locked") ext));
+                    Some ext
+                  end else
+                    new_locked)
+                old_locked cells))
+            locks (! Param.cells))
+          p))
+  | PUnlock(cells, p) ->
+      (check_cell_list cells);
+      Unlock(
+        (List.map fst cells),
+        (check_process env
+          (List.map2
+            (fun old_locked (cell_name, _) ->
+              (List.fold_left
+                (fun new_locked (to_lock, ext) ->
+                  if (cell_name = to_lock) then
+                  begin
+                    (match old_locked with
+                      | Some _ -> ()
+                      | None -> (input_error ("cell " ^ cell_name ^ " is not locked") ext));
+                    None
+                  end else
+                    new_locked)
+                old_locked cells))
+            locks (! Param.cells))
+          p))
+  | PLockAll(p,ext) ->
+      (for i = 1 to (List.length (! Param.cells)) do
+        (match (List.nth locks (i-1)) with
+          | None -> ()
+          | Some _ ->
+              (input_error ("cell " ^ (fst (List.nth (! Param.cells) (i-1)))
+                ^ " is already locked") ext))
+      done);
+      Lock((List.map fst (! Param.cells)),
+        check_process env (List.map (fun _ -> (Some ext)) locks) p)
+  | PUnlockAll(p,ext) ->
+      (for i = 1 to (List.length (! Param.cells)) do
+        (match (List.nth locks (i-1)) with
+          | None ->
+              (input_error ("cell " ^ (fst (List.nth (! Param.cells) (i-1)))
+                ^ " is not locked") ext)
+          | Some _ -> ())
+      done);
+      Unlock((List.map fst (! Param.cells)),
+        check_process env (List.map (fun _ -> None) locks) p)
+  | PAssign(pairs, p) ->
+      (check_cell_list (List.map fst pairs));
+      Assign(
+        (List.map
+          (fun (cell, term) ->
+            ((fst cell), (check_term env term)))
+          pairs),
+        (check_process env locks p))
+  | PReadAs(pairs, p) ->
+      (check_cell_list (List.map fst pairs));
+      let env' = (ref env) in
+      let pairs' = 
+        (List.map
+          (fun (cell, pattern) ->
+            let (pattern', env'') = (check_pat (! env') pattern) in
+            env' := env'';
+            ((fst cell), pattern'))
+          pairs) in
+      ReadAs(pairs', (check_process (! env') locks p))
+
+(* Handle implicit unlocks in else clauses that are not provided. *)
+and check_process_implicit_unlock env locks = function
+  | PNil -> Nil
+  | p -> (check_process env locks p)
 
 let get_non_interf (id, lopt) =
   (get_non_interf_name id, 
@@ -742,6 +871,11 @@ let rec check_all = function
 	  input_error ("free name " ^ i ^ " already declared") ext;
 	ignore(add_free_name (not b) i)) il;
       check_all l
+  | (Cell (name, init_value)) :: l ->
+      if (List.exists (fun r -> (fst r) = (fst name)) !Param.cells) then
+        input_error ("cell " ^ (fst name) ^ " already declared") (snd name);
+      add_cell (fst name) (check_eq_term (fun _ _ -> ()) glob_table init_value);
+      check_all l
   | (Clauses c) :: l ->
       List.iter check_clause c;
       check_all l
@@ -773,7 +907,7 @@ let rec check_all = function
       end;
       check_all l
   | [Process p] -> 
-      let r = check_process (init_env()) p in
+      let r = check_process (init_env()) (all_unlocked()) p in
       List.iter (List.iter nvn_q) (!query_list);
       List.iter (fun (fact,_,bl) ->
 	nvn_ff fact;
@@ -802,6 +936,8 @@ let rec set_max_used_phase = function
       if n > !Param.max_used_phase then
 	Param.max_used_phase := n;
       set_max_used_phase p
+  | Lock(_,p) | Unlock(_,p)
+  | Assign(_,p) | ReadAs(_,p) -> set_max_used_phase p
 
 let parse_file s = 
   let p = check_all (parse s) in
@@ -961,6 +1097,12 @@ let find_event_arity s e'' arity =
   with Not_found ->
     input_error ("unknown event " ^s) e''
 
+let check_arity predicate expected_arity actual_arity e =
+  let expected_arity' = expected_arity + (List.length !Param.cells) in
+  if actual_arity <> expected_arity' then
+    input_error ("arity of predicate " ^ predicate ^ " should be " ^
+      (string_of_int expected_arity')) e
+
 let check_event ((f,e),n) =
   match f with
     PGNeq(t1,t2) ->
@@ -1000,8 +1142,7 @@ let check_event ((f,e),n) =
 	| _ -> input_error "predicate evinj should have one argument, which is a function application" e'
       end
   | PGSimpleFact(("attacker",_), tl) ->
-      if List.length tl != 1 then
-	input_error "arity of predicate attacker should be 1" e;
+      check_arity "attacker" 1 (List.length tl) e;
       if n > !Param.max_used_phase then
 	begin
 	  input_warning "phase greater than the maximum phase used in the process.\nIs that really what you want?" e;
@@ -1010,8 +1151,7 @@ let check_event ((f,e),n) =
       let att_n = Param.get_pred (Attacker((if n = -1 then (!Param.max_used_phase) else n), Param.any_type)) in
       QFact(att_n, List.map check_query_term tl)
   | PGSimpleFact(("mess",_), tl) ->
-      if List.length tl != 2 then
-	input_error "arity of predicate mess should be 2" e;
+      check_arity "mess" 2 (List.length tl) e;
       if n > !Param.max_used_phase then
 	begin
 	  input_warning "phase greater than the maximum phase used in the process.\nIs that really what you want?" e;
@@ -1353,15 +1493,13 @@ let check_gfact_format ((s, ext), tl, n) =
     "ev" | "evinj" -> 
       input_error "predicates ev and evinj not allowed in nounif" ext
   | "attacker" ->
-      if List.length tl != 1 then
-	input_error "arity of predicate attacker should be 1" ext;
+      (check_arity "attacker" 1 (List.length tl) ext);
       if n > !Param.max_used_phase then
 	input_warning "nounif declaration for a phase greater than used" ext;
       let att_n = Param.get_pred (Attacker((if n = -1 then (!Param.max_used_phase) else n), Param.any_type)) in
       (att_n, List.map check_gformat tl)
   | "mess" ->
-      if List.length tl != 2 then
-	input_error "arity of predicate mess should be 2" ext;
+      (check_arity "mess" 2 (List.length tl) ext);
       if n > !Param.max_used_phase then
 	input_warning "nounif declaration for a phase greater than used" ext;
       let mess_n = Param.get_pred (Mess((if n = -1 then (!Param.max_used_phase) else n), Param.any_type)) in
diff --git a/src/pitransl.ml b/src/pitransl.ml
index f238b9a..158de8c 100644
--- a/src/pitransl.ml
+++ b/src/pitransl.ml
@@ -29,6 +29,8 @@ open Parsing_helper
 open Types
 open Pitypes
 
+let initial_cell_states () = List.map snd !Param.cells
+
 (* TO DO: improve this translation algorithm by
    making the unifications as soon as they are known.
    Pb: we have to be able to undo unifications... *)
@@ -94,6 +96,8 @@ let rec check_uniq_ev f = function
  | Get(_,_,p,_) -> check_uniq_ev f p
  | Phase(n,p,_) ->
      check_uniq_ev f p
+ | Lock(_,p) | Unlock(_,p)
+ | ReadAs(_,p) | Assign(_,p) -> check_uniq_ev f p
 
 (* Compute in accu the list of events that are injective, so that
    they must be executed at most once for each value of the session
@@ -120,6 +124,9 @@ let rec get_uniq_ev_proc accu = function
  | Get(_,_,p,_) -> get_uniq_ev_proc accu p
  | Phase(n,p,_) ->
      get_uniq_ev_proc accu p
+ | Lock(_,p) | Unlock(_,p)
+ | ReadAs(_,p) | Assign(_,p) ->
+     get_uniq_ev_proc accu p
 
 (* Check that all injective events can be executed at most once
    for each value of the session identifiers *)
@@ -306,6 +313,7 @@ type name_param_info =
    term: to put as parameter of name function symbol
 *)
 
+type stronger_state = PhiIsStronger | HypIsStronger
 
 type transl_state = 
     { hypothesis : fact list; (* Current hypotheses of the rule *)
@@ -328,14 +336,19 @@ type transl_state =
       cur_phase : int;
       input_pred : predicate;
       output_pred : predicate;
-      hyp_tags : hypspec list
+      hyp_tags : hypspec list;
+      stronger_state : stronger_state;
+      last_states : term list; (* last known cell states *)
+      cell_locks : bool list   (* lock status for each cell *)
     }
 
-let att_fact phase t =
-  Pred(Param.get_pred (Attacker(phase, Terms.get_term_type t)), [t])
+let att_fact phase last_states t =
+  assert ((List.length last_states) = (List.length !Param.cells));
+  Pred(Param.get_pred (Attacker(phase, Terms.get_term_type t)), last_states @ [t])
   
-let mess_fact phase tc tm =
-  Pred(Param.get_pred (Mess(phase, Terms.get_term_type tm)), [tc;tm])
+let mess_fact phase last_states tc tm =
+  assert ((List.length last_states) = (List.length !Param.cells));
+  Pred(Param.get_pred (Mess(phase, Terms.get_term_type tm)), last_states @ [tc;tm])
   
 let table_fact phase t =
   Pred(Param.get_pred (Table(phase)), [t])
@@ -399,6 +412,18 @@ let output_rule { hypothesis = prev_input; constra = constra; unif = unif;
       let constra2 = List.map Terms.copy_constra2 constra in
       let name_params2 = List.map Terms.copy_term2 name_params in
       Terms.cleanup();
+      let hyp, concl, constra2 = (
+        if !Param.propagate_state then
+          Optimisation.propagate_state hyp concl constra2
+        else
+          hyp, concl, constra2 (* do nothing *)
+        ) in
+      let hyp, hyp_tags, concl = (
+        if !Param.dejunk_hypotheses then
+          Optimisation.dejunk hyp hyp_tags concl
+        else
+          hyp, hyp_tags, concl (* do nothing *)
+        ) in
       begin
 	try
 	  add_rule hyp concl (Rules.simplify_constra_list (concl::hyp) constra2) 
@@ -706,6 +731,26 @@ let transl_fact next_fun f cur_state =
       transl_term_list_incl_destructor (fun patl cur_state1 ->
 	next_fun (Pred(p,patl)) cur_state1) tl cur_state 
 
+let rec dup_term = function
+    FunApp(f, args) -> FunApp(f, List.map dup_term args)
+  | Var x -> Var (Terms.copy_var x)
+
+let rec dup_pat = function
+    PatVar x -> PatVar (Terms.copy_var x)
+  | PatTuple(f,l) -> PatTuple(f, List.map dup_pat l)
+  | PatEqual(t) -> PatEqual(dup_term t)
+
+(* Produce fresh variables for all unlocked cells. *)
+
+let freshen_cells cur_state =
+    List.map2 (fun (old_value, locked) cell ->
+        if locked then
+            old_value
+        else
+            Var (Terms.new_var ("v" ^ (fst cell)) Param.any_type))
+        (List.combine cur_state.last_states cur_state.cell_locks)
+        !Param.cells
+
 (* Translate process *)
 
 let rec transl_process cur_state = function
@@ -733,14 +778,14 @@ let rec transl_process cur_state = function
 	 begin
 	   if (!Param.key_compromise == 0) then
 	     transl_process { cur_state with 
-			      hypothesis = (att_fact cur_state.cur_phase (Var v)) :: cur_state.hypothesis;
+			      hypothesis = (att_fact cur_state.cur_phase (freshen_cells cur_state) (Var v)) :: cur_state.hypothesis;
 			      current_session_id = Some v;
 			      name_params = Always(("!" ^ (string_of_int cur_state.repl_count)), v', Var v) :: cur_state.name_params;
 			      hyp_tags = (ReplTag(occ, count_params)) :: cur_state.hyp_tags
 			    } p
 	   else if (!Param.key_compromise == 1) then
 	     transl_process { cur_state with 
-			      hypothesis = (att_fact cur_state.cur_phase (Var v)) :: (att_fact cur_state.cur_phase (Var comp_session_var)) :: cur_state.hypothesis;
+			      hypothesis = (att_fact cur_state.cur_phase (freshen_cells cur_state) (Var v)) :: (att_fact cur_state.cur_phase (freshen_cells cur_state) (Var comp_session_var)) :: cur_state.hypothesis;
 			      current_session_id = Some v;
 			      name_params = Always("!comp", comp_session_var, Var comp_session_var) :: 
                                  Always(("!" ^ (string_of_int cur_state.repl_count)), v', Var v) :: cur_state.name_params;
@@ -748,7 +793,7 @@ let rec transl_process cur_state = function
 			    } p
 	   else 
 	     transl_process { cur_state with 
-			      hypothesis = (att_fact cur_state.cur_phase (Var v)) :: cur_state.hypothesis;
+			      hypothesis = (att_fact cur_state.cur_phase (freshen_cells cur_state) (Var v)) :: cur_state.hypothesis;
 			      current_session_id = Some v;
 			      name_params = Always("!comp", v', compromised_session) :: 
                                  Always(("!" ^ (string_of_int cur_state.repl_count)), v', Var v) :: cur_state.name_params;
@@ -831,10 +876,10 @@ let rec transl_process cur_state = function
       let v = Reduction_helper.new_var_pat pat in
       begin
         match tc with
-          FunApp({ f_cat = Name _; f_private = false },_) when !Param.active_attacker ->
+          (*FunApp({ f_cat = Name _; f_private = false },_) when !Param.active_attacker ->
 	    transl_pat PutAlways (end_destructor_group (fun cur_state1 -> transl_process cur_state1 p) occ)
 	      pat v { cur_state with 
-		      hypothesis = (att_fact cur_state.cur_phase v) :: cur_state.hypothesis;
+		      hypothesis = (att_fact cur_state.cur_phase (freshen_cells cur_state) v) :: cur_state.hypothesis;
 		      hyp_tags = (InputTag(occ)) :: cur_state.hyp_tags 
 		    };
             if !Param.non_interference then
@@ -845,13 +890,15 @@ let rec transl_process cur_state = function
 		    (Pred(cur_state.input_pred, [pat1]))
                 ) occ cur_state1
               ) tc cur_state
-        | _ -> 
+        | *)_ -> 
 	    transl_term_incl_destructor (fun pat1 cur_state1 ->
               end_destructor_group (fun cur_state2 ->
+	        let phi' = freshen_cells cur_state2 in
 	        transl_pat PutAlways (end_destructor_group (fun cur_state3 -> 
                   transl_process cur_state3 p) occ) pat v 
 		    { cur_state2 with 
-		      hypothesis = (mess_fact cur_state.cur_phase pat1 v) :: cur_state2.hypothesis;
+		      hypothesis = (mess_fact cur_state.cur_phase phi' pat1 v) :: cur_state2.hypothesis;
+		      last_states = phi';
 		      hyp_tags = (InputTag(occ)) :: cur_state2.hyp_tags
 		    };
 	        if !Param.non_interference then
@@ -863,8 +910,8 @@ let rec transl_process cur_state = function
       end
  | Output(tc,t,p,occ) ->
       begin
-        match tc with 
-          FunApp({ f_cat = Name _; f_private = false },_) when !Param.active_attacker -> 
+        match tc with
+          (*FunApp({ f_cat = Name _; f_private = false },_) when !Param.active_attacker -> 
 	    if !Param.non_interference then
 	    begin
 	      transl_term (fun cur_state1 patc ->
@@ -880,23 +927,62 @@ let rec transl_process cur_state = function
                 output_rule { cur_state2 with 
                               hypothesis = replace_begin_out cur_state2.name_params cur_state2.hyp_tags cur_state2.hypothesis;
                               hyp_tags = (OutputTag occ) :: cur_state2.hyp_tags
-			    } (att_fact cur_state.cur_phase pat1)
+			    } (att_fact cur_state.cur_phase cur_state.last_states pat1)
               ) occ cur_state1
             ) cur_state t
-        | _ -> transl_term (fun cur_state1 patc ->
+        | *)_ -> transl_term (fun cur_state1 patc ->
                  transl_term (fun cur_state2 pat1 ->
                    end_destructor_group (fun cur_state3 ->
-         	     if !Param.non_interference then
+                     if !Param.non_interference then
                        output_rule { cur_state3 with
                                      hyp_tags = (OutputPTag occ) :: cur_state3.hyp_tags }
-			  (Pred(cur_state.output_pred, [patc]));
+                          (Pred(cur_state.output_pred, [patc]));
+
+                     let state_to_use = (
+                       if (List.for_all ((=) true) cur_state.cell_locks) then
+                         cur_state.last_states
+                       else begin
+                           if !Param.output_mode <> Param.PhiOutput then
+                             try
+                               let last_hyp_state = (
+                                 match (
+                                   List.find (
+                                     function
+                                         Pred({p_info = [Attacker(_,_)]},_)
+                                       | Pred({p_info = [Mess(_,_)]},_) -> true
+                                       | _ -> false
+                                     ) cur_state.hypothesis
+                                 ) with
+                                     Pred({p_info = [Attacker(_,_)]},args) -> fst (Lists.head_tail args 1)
+                                   | Pred({p_info = [Mess(_,_)]},args) -> fst (Lists.head_tail args 2)
+                                   | _ -> raise Not_found )
+                               in
+                               if (!Param.output_mode = Param.HypothesisOutput) then
+                                 last_hyp_state
+                               else if (!Param.output_mode = Param.OldHeuristicOutput) then
+                                 if (List.for_all (function Var x -> true | _ -> false) last_hyp_state) then
+                                   last_hyp_state
+                                 else
+                                   cur_state.last_states
+                               else if (!Param.output_mode = Param.HeuristicOutput) then
+                                 match cur_state.stronger_state with
+                                   | PhiIsStronger -> cur_state.last_states
+                                   | HypIsStronger -> last_hyp_state
+                               else
+                                 raise Not_found (* Should not reach here *)
+                             with Not_found ->
+                               cur_state.last_states
+                           else
+                             cur_state.last_states
+                       end)
+                     in
                      output_rule { cur_state3 with 
-				   hypothesis = replace_begin_out cur_state3.name_params cur_state3.hyp_tags cur_state3.hypothesis;
+                                   hypothesis = replace_begin_out cur_state3.name_params cur_state3.hyp_tags cur_state3.hypothesis;
                                    hyp_tags = (OutputTag occ) :: cur_state2.hyp_tags
-			         } (mess_fact cur_state.cur_phase patc pat1)
+                                 } (mess_fact cur_state.cur_phase state_to_use patc pat1)
                    ) occ cur_state2
                  ) cur_state1 t
-	       ) cur_state tc
+               ) cur_state tc
       end;
       transl_process { cur_state with
                        hyp_tags = (OutputTag occ) :: cur_state.hyp_tags } p
@@ -1036,12 +1122,115 @@ let rec transl_process cur_state = function
                       cur_phase = n;
                       input_pred = Param.get_pred (InputP(n));
                       output_pred = Param.get_pred (OutputP(n)) } p
+ | Lock(cells, p) ->
+     let phi' = (freshen_cells cur_state) in
+     let new_locks =
+        (List.fold_left
+          (fun locks cell_name ->
+            (Lists.update_list locks (Param.find_cell_index cell_name) true))
+          cur_state.cell_locks cells) in
+     transl_process { cur_state with
+                      cell_locks = new_locks;
+                      last_states = phi' } p
+ | Unlock(cells, p) ->
+     let phi' = freshen_cells cur_state in
+     let new_locks =
+        (List.fold_left
+          (fun locks cell_name ->
+            (Lists.update_list locks (Param.find_cell_index cell_name) false))
+          cur_state.cell_locks cells) in
+     transl_process { cur_state with
+                      last_states = phi';
+                      cell_locks = new_locks } p
+ | Assign(pairs, p) ->
+     (* pats = list of patterns from transl_term, one for each item in pairs *)
+     let translate_assignment pats cur_state = begin
+        let phi' = (freshen_cells cur_state) in
+        let phi'' =
+          (List.fold_left2
+            (fun phi'' (cell, _) pat ->
+              (Lists.update_list phi'' (Param.find_cell_index cell) pat))
+            phi' pairs pats)
+        in
+        let vc = Var (Terms.new_var "vc" Param.channel_type) in
+        let vm = Var (Terms.new_var "vm" Param.any_type) in
+        let cell_indices = (List.map (fun (cell, _) -> (Param.find_cell_index cell)) pairs) in
+        output_rule { cur_state with
+                      hypothesis = replace_begin_out cur_state.name_params cur_state.hyp_tags
+                                                     ((mess_fact cur_state.cur_phase phi' vc vm) :: cur_state.hypothesis);
+                      hyp_tags = (AssignmentTag(cell_indices)) :: cur_state.hyp_tags
+                    } (mess_fact cur_state.cur_phase phi'' vc vm);
+        output_rule { cur_state with
+                      hypothesis = replace_begin_out cur_state.name_params cur_state.hyp_tags
+                                                     ((att_fact cur_state.cur_phase phi' vm) :: cur_state.hypothesis);
+                      hyp_tags = (AssignmentTag(cell_indices)) :: cur_state.hyp_tags
+                    } (att_fact cur_state.cur_phase phi'' vm);
+        transl_process { cur_state with
+                         stronger_state = PhiIsStronger;
+                         last_states = phi'' } p
+     end in
+     let rec transl_terms pats pairs' cur_state = begin
+        match pairs' with
+        | [] -> (end_destructor_group (translate_assignment (List.rev pats)) 0 cur_state)
+        | (cell, term) :: rest ->
+            (transl_term
+              (fun cur_state pat -> (transl_terms (pat :: pats) rest cur_state))
+              cur_state term)
+     end in
+     (transl_terms [] pairs cur_state)
+  | ReadAs(pairs, p) ->
+     let phi' = (freshen_cells cur_state) in
+     let vc = Var (Terms.new_var "vc" Param.channel_type) in
+     let vm = Var (Terms.new_var "vm" Param.any_type) in
+     let cell_indices = (List.map (fun (cell, _) -> (Param.find_cell_index cell)) pairs) in
+     let rec transl_patterns pairs' cur_state = begin
+        match pairs' with
+        | [] ->
+          begin
+            transl_process { cur_state with
+                             hypothesis     = (mess_fact cur_state.cur_phase phi' vc vm) :: cur_state.hypothesis;
+                             hyp_tags       = (ReadTag(cell_indices)) :: cur_state.hyp_tags;
+                             stronger_state = PhiIsStronger;
+                             last_states    = phi' } p
+          end
+        | (cell, pattern) :: rest ->
+            (transl_pat PutAlways (end_destructor_group (transl_patterns rest) 0)
+              pattern (List.nth phi' (Param.find_cell_index cell)) cur_state)
+     end in
+     (end_destructor_group (transl_patterns pairs) 0 cur_state)
+
+(* Produce a list of terms representing any state,
+   for example [Var vs1; Var vs2] in
+   attacker((vs1,vs2),vc) & attacker((vs1,vs2),vm) -> message((vs1,vs2),vc,vm) *)
+let free_cells_inner = ref None
+let free_cells () =
+    begin
+        match !free_cells_inner with
+            None ->
+                free_cells_inner := Some (
+                    List.map (fun (name, initial_value) ->
+                        Var ({
+                            sname = "freecell_" ^ name;
+                            vname = 0;
+                            btype = Param.any_type;
+                            link = NoLink
+                        }))
+                        !Param.cells)
+          | Some _ -> ()
+    end;
+    match !free_cells_inner with Some x -> x
+
+(* Similarly but produce formats. *)
+let free_cell_vars t =
+    List.map (fun (name, initial_value) ->
+        FVar(Terms.new_var ("freecell_" ^ name) t))
+        !Param.cells
 
 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));
+  add_rule (List.map (att_fact phase (free_cells ())) hyp)
+    (att_fact phase (free_cells ()) concl) [] (Apply(Func(f), res_pred));
   if !Param.non_interference then
     begin
       if !Terms.current_bound_vars != [] then
@@ -1054,7 +1243,7 @@ let rules_for_red f phase red_rule =
       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)
+	 :: List.map (att_fact phase (free_cells ())) vlist)
 	(Pred(bad_pred, []))
 	[]
 	(TestApply(Func(f), res_pred))
@@ -1069,24 +1258,26 @@ let rules_for_function phase _ f =
      match f.f_cat with
        Eq red_rules -> 
 	 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));
+	 let phi = (if (vars = []) then (initial_cell_states ()) else (free_cells())) in
+	 add_rule (List.map (att_fact phase phi) vars)
+           (att_fact phase phi (FunApp(f,vars))) [] (Apply(Func(f), res_pred));
 	 List.iter (rules_for_red f phase) red_rules
      | Red red_rules ->
 	 List.iter (rules_for_red f phase) red_rules
      | Tuple ->
 	(* For tuple constructor *)
 	 let vars = Terms.var_gen (fst f.f_type) in
-	 add_rule (List.map (att_fact phase) vars)
-	   (att_fact phase (FunApp(f, vars))) []
+	 let phi = (if (vars = []) then (initial_cell_states ()) else (free_cells ())) in
+	 add_rule (List.map (att_fact phase phi) vars)
+	   (att_fact phase phi (FunApp(f, vars))) []
 	   (Apply(Func(f), res_pred));
 
 	(* For corresponding projections *)
 	 for n = 0 to (List.length (fst f.f_type))-1 do
 	   let vars = Terms.var_gen (fst f.f_type) in
 	   let v = List.nth vars n in
-	   add_rule [att_fact phase (FunApp(f, vars))]
-	     (att_fact phase v) []
+	   add_rule [att_fact phase (free_cells ()) (FunApp(f, vars))]
+	     (att_fact phase (free_cells ()) v) []
 	     (Apply(Proj(f,n),res_pred))
 	 done
      | _ -> ()
@@ -1103,16 +1294,16 @@ let transl_attacker phase =
     (* The attacker has any message sent on a channel he has *)
     let v = Terms.new_var_def t in
     let vc = Terms.new_var_def Param.channel_type in
-    add_rule [Pred(mess_pred, [vc; v]); att_fact phase vc]
-          (Pred(att_pred, [v])) [] (Rl(att_pred,mess_pred));
+    add_rule [Pred(mess_pred, (free_cells ()) @ [vc; v]); att_fact phase (free_cells ()) vc]
+          (Pred(att_pred, (free_cells ()) @ [v])) [] (Rl(att_pred,mess_pred));
 
     if (!Param.active_attacker) then
       begin
       (* The attacker can send any message he has on any channel he has *)
 	let v = Terms.new_var_def t in
 	let vc = Terms.new_var_def Param.channel_type in
-	add_rule [att_fact phase vc; Pred(att_pred, [v])]
-          (Pred(mess_pred, [vc; v])) [] (Rs(att_pred, mess_pred))
+	add_rule [att_fact phase (free_cells ()) vc; Pred(att_pred, (free_cells ()) @ [v])]
+          (Pred(mess_pred, (free_cells ()) @ [vc; v])) [] (Rs(att_pred, mess_pred))
       end) (if !Param.ignore_types then [Param.any_type] else !Param.all_types);
 
   
@@ -1259,7 +1450,7 @@ let rec comp_transl_process = function
 	     (comp_fact (FunApp(n, name_params)));
 	   if List.exists (fun x -> x == compromised_session) name_params then
 	     comp_output_rule prev_input 
-	       (att_fact 0 (FunApp(n, name_params)))
+	       (att_fact 0 [](FunApp(n, name_params)))
        | _ -> internal_error "name expected in comp_transl_process"
      end;
      comp_transl_process p
@@ -1401,7 +1592,7 @@ let transl p =
     List.iter (fun t -> 
       let att_i = Param.get_pred (Attacker(i,t)) in
       let v = Terms.new_var Param.def_var_name t in
-      Selfun.add_no_unif (att_i, [FVar v]) Selfun.never_select_weight;
+      Selfun.add_no_unif (att_i, (free_cell_vars Param.any_type) @ [FVar v]) Selfun.never_select_weight;
       if i > 0 then
 	let w = Terms.new_var_def t in
 	let att_im1 = Param.get_pred (Attacker(i-1,t)) in
@@ -1421,7 +1612,7 @@ let transl p =
       The non-interference queries have their private flag set. *)
    List.iter (fun ch ->
       if not ch.f_private then
-        add_rule [] (att_fact 0 (FunApp(ch, []))) [] Init) (!Param.freenames);
+        add_rule [] (att_fact 0 (initial_cell_states ()) (FunApp(ch, []))) [] Init) (!Param.freenames);
 
   List.iter (fun t ->
     (* Clauses for equality *)
@@ -1434,10 +1625,10 @@ let transl p =
     let v = Terms.new_var_def Param.sid_type in
     let new_name_fun = Terms.new_name_fun t in
     if !Param.non_interference then
-      add_rule [att_fact 0 v] (att_fact 0 (FunApp(new_name_fun, [v])))
+      add_rule [att_fact 0 (initial_cell_states ()) v] (att_fact 0 (initial_cell_states ()) (FunApp(new_name_fun, [v])))
 	[] (Rn (Param.get_pred (Attacker(0, t))))
     else
-      add_rule [] (att_fact 0 (FunApp(new_name_fun, [v])))
+      add_rule [] (att_fact 0 (initial_cell_states ()) (FunApp(new_name_fun, [v])))
 	[] (Rn (Param.get_pred (Attacker(0, t))));
 
     if (!Param.non_interference) then
@@ -1471,7 +1662,7 @@ let transl p =
 	   List.map (fun t -> 
 	     let v = Terms.new_var_def t in
 	     let att_guess = Param.get_pred (AttackerGuess(t)) in
-	     let hyp = [att_fact (!Param.max_used_phase) v] in
+	     let hyp = [att_fact (!Param.max_used_phase) [] v] in
 	     let concl = Pred(att_guess, [v; v]) in
 	     let r = (t, Rule(!nrule, PhaseChange, hyp, concl, [])) in
 	     add_rule hyp concl [] PhaseChange;
@@ -1501,11 +1692,12 @@ let transl p =
 	     r) (if !Param.ignore_types then [Param.any_type] else !Param.all_types)
 
   end;
-  
+
    List.iter (fun ch -> match ch.f_cat with
                           Name r -> r.prev_inputs <- Some (FunApp(ch, []))
                         | _ -> internal_error "should be a name 1")
-	(!Param.freenames);
+     (!Param.freenames);
+
    transl_process 
      { hypothesis = []; constra = []; unif = []; last_step_unif = [];
        success_conditions = None; name_params = []; 
@@ -1514,7 +1706,11 @@ let transl p =
        input_pred = Param.get_pred (InputP(0));
        output_pred = Param.get_pred (OutputP(0));
        hyp_tags = []; 
+       stronger_state = PhiIsStronger;
+       last_states = initial_cell_states ();
+       cell_locks = List.map (fun _ -> false) !Param.cells;
      } p;
+
    List.iter (fun ch -> match ch.f_cat with
                           Name r -> r.prev_inputs <- None
                         | _ -> internal_error "should be a name 2")
@@ -1555,7 +1751,11 @@ let transl p =
   List.iter (function (f,n) ->
     Selfun.add_no_unif f n) (if !Param.typed_frontend then Pitsyntax.get_nounif() else Pisyntax.get_nounif());
 
-  List.rev (!red_rules)
+  let preground_result = (List.rev (!red_rules)) in
+  (if (!Param.grounding) then
+      (Optimisation.grounding preground_result)
+    else
+      (preground_result))
 
 (* Move restrictions under inputs to make the analysis more precise *)
 
@@ -1628,5 +1828,7 @@ let rec move_new accu = function
       put_new l1 (Get(pat, t1, move_new l2 p, occ))
   | Phase(n,p,occ) ->
       Phase(n, move_new accu p,occ)
-      
+  | Lock(cell, p) -> Lock(cell, move_new accu p)
+  | Unlock(cell, p) -> Unlock(cell, move_new accu p)
+
 let move_new p = move_new [] p
diff --git a/src/reduction.ml b/src/reduction.ml
index 17b8bca..39750df 100644
--- a/src/reduction.ml
+++ b/src/reduction.ml
@@ -1141,11 +1141,11 @@ let rec init_rule state tree =
 		  begin
 		    let (p,c) = 
 		      match tree.thefact with
-			Pred(p,[t]) -> (p,rev_name_subst t)
+			Pred(p,args) -> let phi, [t] = Lists.head_tail args 1 in (p,rev_name_subst t)
 		      | _ -> Parsing_helper.internal_error "unexpected Apply clause"
 		    in
 		    let h = List.map (function 
-			{ thefact = Pred(_,[t]) } -> rev_name_subst t
+			{ thefact = Pred(_,args) } -> let phi, [t] = Lists.head_tail args 1 in rev_name_subst t
 		      |	_ -> Parsing_helper.internal_error "unexpected Apply clause") sons
 		    in
 	            {state1 with prepared_attacker_rule = (p, decompose_list h, decompose_term c)::state1.prepared_attacker_rule}
@@ -1153,7 +1153,8 @@ let rec init_rule state tree =
               | Rn _ ->
                   begin
 	            match tree.thefact with
-                      Pred(p, [t]) ->
+                      Pred(p, args) ->
+                        let (_, [t]) = (Lists.head_tail args 1) in
                         { state1 with prepared_attacker_rule = (p, [], [rev_name_subst t])::state1.prepared_attacker_rule }
                     | _ -> 
 			Parsing_helper.internal_error "Rule Rn should conclude p(name)"
@@ -2342,6 +2343,8 @@ let rec simplify_tree first recheck next_f tree =
 		FactHashtbl.add fact_hashtbl fact_id concl
 	    else
 	      check_coherent factId' (concl, l1, name_params, sons)
+	| AssignmentTag _ | ReadTag _ ->
+	    check_coherent factId' (concl, l1, name_params, sons)
 	| LetTag occ | TestTag occ | LetFilterTag occ | TestUnifTag2 occ ->
 	    check_coherent factId' (concl, l1, name_params, sons)
 	| InputTag _ | GetTag _ | BeginFact | LetFilterFact -> 
diff --git a/src/reduction_helper.ml b/src/reduction_helper.ml
index 0390562..b23a5d6 100644
--- a/src/reduction_helper.ml
+++ b/src/reduction_helper.ml
@@ -95,6 +95,13 @@ let rec occurs_var_proc v = function
       (occurs_var_pat v pat) || (Terms.occurs_var v t) || 
       (occurs_var_proc v p)
   | Phase(_,p,_) -> occurs_var_proc v p
+  | Lock(_,p) | Unlock(_,p) -> occurs_var_proc v p
+  | Assign(pairs, p) ->
+      (List.exists (Terms.occurs_var v) (snd (List.split pairs)))
+      || (occurs_var_proc v p)
+  | ReadAs(pairs, p) ->
+      (List.exists (occurs_var_pat v) (snd (List.split pairs)))
+      || (occurs_var_proc v p)
 
 (* Determine which variables should be included as arguments of names,
    so that queries can be answered *)
@@ -387,6 +394,10 @@ let rec process_subst p n1 n2 =
   | Get(pat, t, p, occ) -> Get(pat_subst pat n1 n2, term_subst t n1 n2, process_subst p n1 n2, occ)
   | Phase(n,p,occ) -> Phase(n,process_subst p n1 n2,occ)
   | LetFilter(bl, f, p, q, occ) -> LetFilter(bl, fact_subst f n1 n2, process_subst p n1 n2, process_subst q n1 n2, occ) 
+  | Lock(cell, p) -> Lock(cell, process_subst p n1 n2)
+  | Unlock(cell, p) -> Unlock(cell, process_subst p n1 n2)
+  | Assign(pairs, p) -> Assign((List.map (fun (cell, term) -> (cell, (term_subst term n1 n2))) pairs), process_subst p n1 n2)
+  | ReadAs(pairs, p) -> ReadAs((List.map (fun (cell, pattern) -> (cell, (pat_subst pattern n1 n2))) pairs), process_subst p n1 n2)
 
 (* let process_subst = Profile.f4 "process_subst" process_subst *)
 
@@ -419,6 +430,10 @@ let rec copy_process = function
   | Get(pat, t, p, occ) -> let pat' = copy_pat pat in Get(pat', copy_term2 t, copy_process p, occ)
   | Phase(n,p,occ) -> Phase(n, copy_process p,occ)
   | LetFilter(bl, f, p, q, occ) -> let bl' = List.map copy_binder bl in LetFilter(bl', copy_fact2 f, copy_process p, copy_process q, occ)
+  | Lock(cell, p) -> Lock(cell, copy_process p)
+  | Unlock(cell, p) -> Unlock(cell, copy_process p)
+  | Assign(pairs, p) -> Assign((List.map (fun (cell, term) -> (cell, (copy_term2 term))) pairs), (copy_process p))
+  | ReadAs(pairs, p) -> ReadAs((List.map (fun (cell, pattern) -> (cell, pattern)) pairs), (copy_process p))
 
 
 (* Close all terms after term_evaluation. Indeed, new variables may
diff --git a/src/rules.ml b/src/rules.ml
index 511676f..cd390ff 100644
--- a/src/rules.ml
+++ b/src/rules.ml
@@ -262,7 +262,7 @@ let occur_count_constra v l =
    inequalities.
  *)
 
-let elim_any_x ((hypl', concl, histl', constra) as r) =
+let elim_any_x ((hypl', concl, histl', constra)) =
    let (hypl'', _, histl'') = List.fold_right (fun hyp1 (hypl, nl, histl) ->
      match hyp1 with
        Pred(chann, l) ->
@@ -697,7 +697,7 @@ let reorder hyp =
 
 (* 5. The final function for subsumption test *)
 
-let implies ((hyp1, concl1, _, constr1) as r1) ((hyp2, concl2, _, constr2) as r2) =
+let implies ((hyp1, concl1, _, constr1)) ((hyp2, concl2, _, constr2)) =
   if List.length hyp1 > List.length hyp2 then false else
   (* let t0 = Unix.times() in *)
    try 
diff --git a/src/selfun.ml b/src/selfun.ml
index b94a9fb..c9b846f 100644
--- a/src/selfun.ml
+++ b/src/selfun.ml
@@ -37,15 +37,15 @@ let default_user_no_unif_weight = -6000
 let no_unif_set = ref ([] : (fact_format * int) list)
 let add_no_unif f n =
   let n =
-    if n >= 0 then default_user_no_unif_weight else 
+    if n >= 0 then default_user_no_unif_weight else
     if n <= never_select_weight then never_select_weight+1 else
     n
   in
 (*
   if !Param.verbose_term then
     begin
-      print_string "nounif "; 
-      display_fact_format f; 
+      print_string "nounif ";
+      display_fact_format f;
       print_string ("/" ^ (string_of_int n));
       Display.Text.newline()
     end;
@@ -61,7 +61,7 @@ let rec has_same_format_term t1 t2 =
    match (t1,t2) with
    | (FunApp(f1,l1), FFunApp(f2,l2)) ->
         (f1 == f2) && (List.for_all2 has_same_format_term l1 l2)
-   | (Var _, FVar v2) | (_, FAny v2) -> 
+   | (Var _, FVar v2) | (_, FAny v2) ->
        begin
 	 match v2.link with
 	   NoLink -> (Terms.link v2 (TLink t1)); true
@@ -85,7 +85,7 @@ let rec format_equal t1 t2 =
    match (t1,t2) with
    | (FFunApp(f1,l1), FFunApp(f2,l2)) ->
         (f1 == f2) && (List.for_all2 format_equal l1 l2)
-   | (FVar v1, FVar v2) | (FAny v1, FAny v2) -> 
+   | (FVar v1, FVar v2) | (FAny v1, FAny v2) ->
        begin
 	 match v2.link with
 	   NoLink -> Terms.link v2 (VLink v1); true
@@ -102,7 +102,7 @@ let rec compute_match_format t1 t2 =
    | (Var v1), (Var v2) -> FAny v1
    | (Var v1), _ -> FVar v1
    | (FunApp (f1,l1')), (FunApp (f2,l2')) ->
-       if f1 != f2 then 
+       if f1 != f2 then
 	 internal_error "terms do not match 3";
        FFunApp(f1,List.map2 compute_match_format l1' l2')
    | _,_ -> internal_error "terms do not match 4"
@@ -115,8 +115,8 @@ let compute_match_format_fact f1 f2 = match (f1,f2) with
 | _ -> internal_error "match format should be called only with Pred facts, since these facts should appear in conclusions"
 
 (* selection_fun rule returns -1 if no fact is selected in rule, and
-   the index of the selected hypothesis otherwise  (0 corresponds to 
-   the first hypothesis) 
+   the index of the selected hypothesis otherwise  (0 corresponds to
+   the first hypothesis)
 *)
 
 (* Standard, equivalent to the old version without selection function *)
@@ -145,9 +145,9 @@ let term_warning ((hyp, concl, _, _) as rule) =
 	end
     end
 
-let selection_fun_nounifset ((hyp, concl, _, _) as rule) = 
-  let rec sel (nold, wold) n = function 
-      [] -> 
+let selection_fun_nounifset ((hyp, concl, _, _) as rule) =
+  let rec sel (nold, wold) n = function
+      [] ->
         if (nold >= 0) && (matchafactstrict concl (List.nth hyp nold)) then
 	  term_warning(rule);
         nold
@@ -155,14 +155,14 @@ let selection_fun_nounifset ((hyp, concl, _, _) as rule) =
 	  (* Guarantee that p(x) is never selected when we decompose data
 	     constructors on p, except that we can select the conclusion when
 	     all hypotheses and the conclusion are of the form p(x) for
-	     such p. This is important for the soundness of 
+	     such p. This is important for the soundness of
 	     the decomposition of data constructors. *)
         sel (nold, wold) (n+1) l
     | (Pred(p,lp) as h::l) ->
 	let wnew = find_same_format (p,lp) (!no_unif_set) in
 	if wnew < 0 then
 	  if wnew > wold
- 	  then sel (n,wnew) (n+1) l 
+ 	  then sel (n,wnew) (n+1) l
           else sel (nold, wold) (n+1) l
 	else
 	  begin
@@ -170,7 +170,7 @@ let selection_fun_nounifset ((hyp, concl, _, _) as rule) =
 	    n
 	  end
     | _ -> Parsing_helper.internal_error "Selfun(1): added to avoid warning for non-exhaustive pattern-matching"
-  in 
+  in
   if is_unselectable concl then
     (* The conclusion is never selected if an hypothesis can be *)
     sel (-1, never_select_weight) 0 hyp
@@ -181,9 +181,9 @@ let selection_fun_nounifset ((hyp, concl, _, _) as rule) =
 
 (* Very good for skeme, but slightly slower for some other protocols *)
 
-let selection_fun_nounifset_maxsize ((hyp, concl, _, _) as rule) = 
-  let rec sel (nold, wold) n = function 
-      [] -> 
+let selection_fun_nounifset_maxsize ((hyp, concl, _, _) as rule) =
+  let rec sel (nold, wold) n = function
+      [] ->
 	if (nold >= 0) && (matchafactstrict concl (List.nth hyp nold)) then
 	  term_warning(rule);
 	nold
@@ -191,21 +191,21 @@ let selection_fun_nounifset_maxsize ((hyp, concl, _, _) as rule) =
 	  (* Guarantee that p(x) is never selected when we decompose data
 	     constructors on p, except that we can select the conclusion when
 	     all hypotheses and the conclusion are of the form p(x) for
-	     such p. This is important for the soundness of 
+	     such p. This is important for the soundness of
 	     the decomposition of data constructors. *)
         sel (nold, wold) (n+1) l
-    | (Pred(p,lp) as h::l) -> 
+    | (Pred(p,lp) as h::l) ->
 	let wtmp = find_same_format (p,lp) (!no_unif_set) in
-        let wnew = 
+        let wnew =
 	  if wtmp < 0
-	  then wtmp 
-	  else fact_size h 
+	  then wtmp
+	  else fact_size h
 	in
-        if wnew > wold 
-	then sel (n,wnew) (n+1) l 
+        if wnew > wold
+	then sel (n,wnew) (n+1) l
         else sel (nold, wold) (n+1) l
     | _ -> Parsing_helper.internal_error "Selfun(2): added to avoid warning for non-exhaustive pattern-matching"
-  in 
+  in
   if is_unselectable concl then
     (* The conclusion is never selected if an hypothesis can be *)
     sel (-1, never_select_weight) 0 hyp
@@ -218,7 +218,7 @@ let selection_fun_nounifset_maxsize ((hyp, concl, _, _) as rule) =
 
 let selection_fun_weight ((hyp, concl, _, _) as rule) =
   let rec sel (nold, wold) n = function
-      [] -> 
+      [] ->
 	if nold = -1 then (* conclusion selected *)
 	  begin
 	    List.iter (function h ->
@@ -230,8 +230,8 @@ let selection_fun_weight ((hyp, concl, _, _) as rule) =
 		      no_unif_set := (format, default_add_no_unif_weight) :: !no_unif_set;
 		      if !Param.verbose_term then
 			begin
-			  print_string "nounif "; 
-			  Display.Text.display_fact_format format; 
+			  print_string "nounif ";
+			  Display.Text.display_fact_format format;
 			  print_string ("/" ^ (string_of_int default_add_no_unif_weight));
 			  Display.Text.newline()
 			end
@@ -248,22 +248,22 @@ let selection_fun_weight ((hyp, concl, _, _) as rule) =
         nold
     | (f::l) when is_unselectable f ->
 	  (* Guarantee that p(x) is never selected when we decompose data
-	     constructors on p. This is important for the soundness of 
+	     constructors on p. This is important for the soundness of
 	     the decomposition of data constructors. *)
         sel (nold, wold) (n+1) l
-    | (Pred(p,lp) as h::l) -> 
+    | (Pred(p,lp) as h::l) ->
 	let wnew =
-	  if matchafactstrict concl h then match_concl_weight else 
+	  if matchafactstrict concl h then match_concl_weight else
 	  let wtmp = find_same_format (p,lp) (!no_unif_set) in
 	  if wtmp < 0 then wtmp else
 	  if !Param.select_fun == Param.TermMaxsize then fact_size h else 0
 	in
-        if wnew > wold 
-	then sel (n,wnew) (n+1) l 
+        if wnew > wold
+	then sel (n,wnew) (n+1) l
         else sel (nold, wold) (n+1) l
     | _ -> Parsing_helper.internal_error "Selfun(3): added to avoid warning for non-exhaustive pattern-matching"
-  in 
-  let wconcl = 
+  in
+  let wconcl =
     if is_unselectable concl then
       (* The conclusion is never selected if an hypothesis can be *)
       never_select_weight
@@ -281,13 +281,13 @@ let rec false_copy = function
   | FunApp(f,l) -> FunApp(f, List.map false_copy l)
 
 let inst_constra = function
-    Neq(Var v,t) -> 
-      if v.link = NoLink then 
+    Neq(Var v,t) ->
+      if v.link = NoLink then
 	Terms.link v (TLink (false_copy t))
   | _ -> ()
 
 let selection_fun ((hyp,concl,hist,constra) as rule) =
-  let r = 
+  let r =
    match !Param.select_fun with
      Param.NounifsetMaxsize -> selection_fun_nounifset_maxsize rule
    | Param.Term | Param.TermMaxsize -> selection_fun_weight rule
diff --git a/src/terms.ml b/src/terms.ml
index f8bed79..aacb35b 100644
--- a/src/terms.ml
+++ b/src/terms.ml
@@ -249,7 +249,7 @@ let equal_facts f1 f2 =
       (chann1 == chann2) && (List.for_all2 equal_terms t1 t2)
   | Out(t1,l1),Out(t2,l2) ->
       (equal_terms t1 t2) && (List.length l1 = List.length l2) 
-	&& (List.for_all2 equals_term_pair l1 l2)
+    && (List.for_all2 equals_term_pair l1 l2)
   | _ -> false
 
 let equals_simple_constraint c1 c2 = 
diff --git a/src/types.mli b/src/types.mli
index 25c13ff..a153418 100644
--- a/src/types.mli
+++ b/src/types.mli
@@ -104,6 +104,10 @@ and process =
   | Insert of term * process * occurrence
   | Get of pattern * term * process * occurrence
   | Phase of int * process * occurrence
+  | Lock of string list * process
+  | Unlock of string list * process
+  | ReadAs of (string * pattern) list * process
+  | Assign of (string * term) list * process
 
 and linktype = 
     NoLink
@@ -191,6 +195,8 @@ type hypspec =
   | OutputPTag of occurrence
   | InsertTag of occurrence
   | GetTag of occurrence
+  | AssignmentTag of int list (* cell indices *)
+  | ReadTag of int list (* cell indices *)
 
 type label =
     ProcessRule of hypspec list * term list 
