(* Generated script of the protocol Plutus with 1 versions, corrected, private readfs *)

param redundantHypElim = true.
param traceBacktracking = false.

(** FUNCTION SYMBOLS **)

(* exponents *)
fun e/2.
fun d/2.

(* modulus; a random RSA seed (p,q) is modeled as a fresh name s *)
fun N/1.

(* exponentiation modulo *)
fun exp/2.

(* symmetric encryption *)
fun enc/2.

(* hash function *)
fun hash/1.

(** ALGORITHMS AND EQUATIONS *)

(* derive seed given RSA exponents and modulus *)
reduc crack(e(x,y),d(x,y),N(x)) = x.                             

(* verify RSA signature, etc. *)
equation exp(exp(z,(d(x,y),N(x))),(e(x,y),N(x))) = z.            
equation exp(exp(z,(e(x,y),N(x))),(d(x,y),N(x))) = z.            

(* derive exponent from modulus and base *)
reduc genExp(N(x),y) = e(x,y).                                    

(* decrypt symmetric encryption *)
reduc dec(enc(x,y),y) = x.                                        

(** VERSION NUMBERS *)

data zero/0.
data succ/1.

pred geq/2.
clauses
        geq:x,x;
	geq:x,y -> geq:succ(x),y.

(** ACCESS CONTROL LISTS *)

data cons/2.
data nil/0.

pred member/2.
clauses
  member:x,cons(x,y);
  member:x,y -> member:x,cons(z,y).

(** CHANNEL DECLARATIONS *)

(* The network is under control of the adversary. *)
free net.

(* The adversary can choose actions. *)
free newgroup.
free revoke.
free rkeyreq, wkeyreq.
free corrupt. 

(* Keys are communicated securely to users. *)
private fun rprivchannel/1.
private fun wprivchannel/1.

(* Tokens and contents are communicated securely to the file system *)
private fun tokenprivchannel/1.
private fun writefs/0.

(* Contents can be retrieved securely from the file system *)
private fun readfs/0.

(** QUERIES *)

(* rx is a reader of group gx at version vx only if it belongs to the readers rlx of gx at vx. *) 
query ev:isreader(rx,gx,vx) ==>
                  ev:isgroup(gx)   
                & ev:isstate(gx,vx,rlx,wlx)
	        & member:rx,rlx.

(* wx is a writer of group gx at version vx only if it belongs to the writers wlx of gx at vx. *) 
query ev:iswriter(wx,gx,vx) ==>
                  ev:isgroup(gx)   
                & ev:isstate(gx,vx,rlx,wlx)
  	        & member:wx,wlx.

(* See definition of secrecy. *)
query let mx = m[g = gx; v = vy]; 
      attacker:mx ==> 
		  ev:corrupt(rx,gx,vx)
		& geq:vx,vy
      	      	& (ev:isreader(rx,gx,vx) | ev:iswriter(rx,gx,vx)).  

(* See definition of strong integrity. *)
query ev:gets(rx,mx,gx,vx,vz) ==> 
                  ev:iswriter(wx,gx,vx) 
                & (ev:puts(wx,mx,gx,vx) | ev:corrupt(wx,gx,vx))
                & (vx = vz | (geq:vz,vx & ev:iswriter(wz,gx,vz)
				& ev:corrupt(wz,gx,vz))).

(* If the server authenticates a write with token tx at version vx, then tx belongs to vx and there is a writer at vx. *)
(* By a manual argument it can be proved that here vx is the current version. *)
query ev:authwrite(gx,vx,tx) ==> 
                  ev:iswriter(wx,gx,vx)
	        & ev:istoken(tx,gx,vx).

(** CODE FOR OWNERS *)

let processOwr =
    (* create owner's RSA key pair *)
    new seed1; new seed2;
    let ownerpubkey = (e(seed1,seed2),N(seed1)) in                
    let ownerprivkey = (d(seed1,seed2),N(seed1)) in

    (* publish owner's RSA public key *)
    out(net,ownerpubkey);
    (
    ! (* receive a new group creation request;
         initreaders and initwriters are the initial lists of allowed readers and writers, respectively *)
      in(net, (=newgroup,initreaders,initwriters));         
      
      (* create a new group g *)
      new g;

      (* assert that g is a group *)
      event isgroup(g);

      (* publish the name g *)
      out(net,g);

      (* create a private channel for the current state for group g *)
      new currentstate;

      (
       ( (* choose new RSA seed *)
	 new seed3; 

         (* create initial token *)
	 new initt; 

         (* send initial token's hash to server *)
	 out(tokenprivchannel(g), (hash(initt),zero));

         (* create initial lk *)
         new initlk;                                            

         (* generate initial sk *)
         let initsk = (d(seed3,initlk),N(seed3)) in      

	 (* assert the state at version 0 *)
	 event isstate(g,zero,initreaders,initwriters);
	 event istoken(initt,g,zero);

	 (* store state for version 0 on channel currentstate *)
         out(currentstate, (zero,initreaders,initwriters,initlk,initsk,initt))
       )

      (* Next, we move from version 0 to version 1. *) 
      |
       ( 
         (* receive a revoke request for group g; 
            newreaders and newwriters and the new lists of allowed readers and writers *)
         in(net, (=revoke,=g,newreaders,newwriters));       

         (* read state for version 0 *)
         in(currentstate, (=zero,oldreaders,oldwriters,oldlk,oldsk,oldt));

         (* choose new RSA seed *)
         new seed3;

         (* create new token *)
	 new newt;           

         (* send new token's hash to server *)                                 
	 in(tokenprivchannel(g), (hashx,vx)); 
         out(tokenprivchannel(g), (hash(newt),succ(zero)));    

         (* wind old lk to new lk *)
         let newlk = exp(oldlk,ownerprivkey) in              

         (* generate new sk *)
         let newsk = (d(seed3,newlk),N(seed3)) in             

         (* assert the state at version 1 *)
         event isstate(g,succ(zero),newreaders,newwriters);
	 event istoken(newt,g,succ(zero));

         (* store state for version 1 on channel currentstate *)
         out(currentstate, (succ(zero),newreaders,newwriters,newlk,newsk,newt))
       )
      |
       (
       ! (* receive read key request for reader r and group g *)
         in(net, (=rkeyreq,r,=g));                                

         (* get the current state *)    
         in(currentstate, (v,readers,writers,lk,sk,t));
         out(currentstate, (v,readers,writers,lk,sk,t));

         (* check that the reader r is allowed *)
         if member:r,readers then (               

            (* assert that r is a reader for group g and version v *)              
            event isreader(r,g,v); 

            (* send lk and owner's public key to r *)
            out(rprivchannel(r), (g,v,lk,ownerpubkey)) )
       )
      |
       (
       ! (* receive write key request for writer w and group g *)
         in(net, (=wkeyreq,w,=g));                                

         (* get the current state *)   
         in(currentstate, (v,readers,writers,lk,sk,t));
         out(currentstate, (v,readers,writers,lk,sk,t));

         (* check that the writer w is allowed *)
         if member:w,writers then (                             
                                                               
             (* sign the modulus *)  
             let (dx,n) = sk in let sn = exp(hash((n,g,v)),ownerprivkey) in

             (* assert that w is a writer for group g and version v *)
	     event iswriter(w,g,v);

             (* send lk, sk, and signed modulus to w *)
             out(wprivchannel(w), (g,v,lk,sk,sn,t)) )
       )
      )
    ).

(** CODE FOR WRITERS *)

let processGoodWtr =
  ! (* initiate a writer w for group g *)
    in(net, (w,g)); 

    (* send write key request *)
    out(net, (wkeyreq,w,g));    

    (* obtain lk, sk, and signed modulus *)
    in(wprivchannel(w), (=g,v,lk,sk,sn,t));      

    (* create data to write *)
    new m;

    (* encrypt *)
    let encx = enc(m,lk) in

    (* sign *)
    let sencx = exp(hash(encx),sk) in

    (* assert that data m has been written by w for group g at version v *)
    event puts(w,m,g,v);
    
    (* send content to the file system *)
    let (dx,n) = sk in out(writefs, (t,(g,v,n,sn,encx,sencx))).

let processBadWtr = 
  ! (* initiate a writer w for group g *)
    in(net, (w,g));

    (* send write key request *)
    out(net, (wkeyreq,w,g));    

    (* obtain lk, sk, and signed modulus *)
    in(wprivchannel(w), (=g,v,lk,sk,sn,t));

    (* receive corrupt request for w *)            
    in(net, =(corrupt,w));             

    (* assert that w has been corrupted for group g at version v *)                           
    event corrupt(w,g,v);

    (* leak lk, sk, and signed modulus *)
    out(net, (lk,sk,sn,t)).              

let processAdvWtr =
    (* allow the adversary to send content to the server *)
    ! in(net, (t, content));
      out(writefs, (t,content)).                           

(** CODE FOR SERVER *)

let processServer = 
  ! (* initiate a group g *)
    in(net, g);

    (
     (
     ! (* receive a hash of the current token from g's owner *)
       in(tokenprivchannel(g), (hashx,vx));

       (* carry the hash of the current token for g *)
       out(tokenprivchannel(g), (hashx,vx))
     )
    |
     (
     ! (* receive content sent with token t *)
       in(writefs, (t,content));                       

       (* leak the content *)
       out(net,content);   

       (* get the hash of the token at (the current version) vx *)
       in(tokenprivchannel(g), (hashx,vx));
       out(tokenprivchannel(g), (hashx,vx));

       (* check that t hashes to the same string as the token at vx *)
       if hash(t) = hashx then    

       (* assert that content sent with token t is verified for g at vx *)
       event authwrite(g,vx,t);

       (* write server-verified content for g at vx *)
       ! out(readfs, (content,g,vx))                  
     )
    ).

(** CODE FOR READERS *)

let processGoodRdr = 
  ! (* initiate a reader r for group g *)
    in(net, (r,g));

    (* send read key request *)    
    out(net, (rkeyreq,r,g));   

    (* obtain lk and owner's public key *)
    in(rprivchannel(r), (=g,vx,lk,ownerpubkey));  

    (* obtain header and content from file system *)
    in(readfs, ((=g,v,n,sn,encx,sencx),=g,vz));            

    (* verify signature in header *)
    if hash((n,g,v)) = exp(sn,ownerpubkey) then
    (
      if vx = succ(zero) then (
         if v = zero then (
            (* unwind lk *)
            let lk = exp(lk,ownerpubkey) in
            (* derive vk *)                       
            let vk = (genExp(n,lk),n) in

            (* verify signature of encryption *)
            if hash(encx) = exp(sencx,vk) then

            (* decrypt to obtain data *)
            let x = dec(encx,lk) in

            (* assert that reader r read data x for group g and version v *)
            event gets(r,x,g,v,vz)
         )
        |
         if v = succ(zero) then (
            (* derive vk *)                       
            let vk = (genExp(n,lk),n) in

            (* verify signature of encryption *)
            if hash(encx) = exp(sencx,vk) then

            (* decrypt to obtain data *)
            let x = dec(encx,lk) in

            (* assert that reader r read data x for group g and version v *)
            event gets(r,x,g,v,vz)
         )
      )
      |
      if vx = zero then (
         if v = zero then (
            (* derive vk *)                       
            let vk = (genExp(n,lk),n) in

            (* verify signature of encryption *)
            if hash(encx) = exp(sencx,vk) then

            (* decrypt to obtain data *)
            let x = dec(encx,lk) in

            (* assert that reader r read data x for group g and version v *)
            event gets(r,x,g,v,vz)
      ))
    ).

let processBadRdr =
  ! (* initiate a reader r for group g *)
    in(net, (r,g));

    (* send read key request *)
    out(net, (rkeyreq,r,g)); 

    (* obtain lk and owner's public key *)
    in(rprivchannel(r), (=g,v,lk,ownerpubkey));

    (* receive corrupt request for r *)
    in(net, =(corrupt,r));                    

    (* assert that r has been corrupted for group g at version v *)
    event corrupt(r,g,v);

    (* leak lk *)
    out(net,lk).   

(** TOP LEVEL PROCESS *)

process
         ( processOwr
         | processGoodWtr | processBadWtr | processAdvWtr 
         | processServer 
         | processGoodRdr | processBadRdr  
         )