(* Options to decide which script to generate *)

let detailed_lockbox = ref false
let corrected = ref false
let private_readfs = ref false
let signhash_without_enc = ref false

let rec succ n s =
  if n = 0 then print_string s else
  begin
    print_string "succ(";
    succ (n-1) s;
    print_string ")"
  end

let revoke n = 
  print_string "

      (* Next, we move from version "; print_int n; print_string " to version "; print_int (n+1); print_string ". *) 
      |
       ( 
         (* 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 "; print_int n; print_string " *)
         in(currentstate, (=";
  succ n "zero";
  print_string ",oldreaders,oldwriters,oldlk,oldsk,oldt));

         (* choose new RSA seed *)
         new seed3;";
  if !private_readfs then (print_string "

         (* create new token *)
	 new newt;           

         (* send new token's hash to server *)                                 
	 in(tokenprivchannel(g), (hashx,vx)); 
         out(tokenprivchannel(g), (hash(newt),";
  succ (n+1) "zero";
  print_string "));    ")
  else print_string "

         (* create new token *)
	 new newt;                                            

         (* send new token's hash to server *)                                 
	 in(tokenprivchannel(g), hashx); 
         out(tokenprivchannel(g), hash(newt));";
  print_string "

         (* 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 "; print_int (n+1); print_string " *)
         event isstate(g,";
  succ (n+1) "zero";
  print_string ",newreaders,newwriters);
	 event istoken(newt,g,";
  succ (n+1) "zero";
  print_string ");

         (* store state for version "; print_int (n+1); print_string " on channel currentstate *)
         out(currentstate, (";
  succ (n+1) "zero";
  print_string ",newreaders,newwriters,newlk,newsk,newt))
       )"

let rec revokeTill n = 
  if n = 0 then () else 
    begin
      revokeTill (n-1);
      revoke (n-1)
    end

let rec repeat k s = 
  if k = 0 then () else 
    begin
      print_string s;
      repeat (k-1) s
    end

let rec unwind n k s = 
  print_string "         if v = "; succ k "zero"; print_string " then (\n";
  repeat (n-k) 
"            (* unwind lk *)
            let lk = exp(lk,ownerpubkey) in\n";
  print_string s;
  if k < n then 
    begin
      print_string "         )\n        |\n";
      unwind n (k+1) s
    end
  else
    print_string "         )\n"

let rec unwindTill n s = 
  if n > 0 then 
    begin
      print_string "      if vx = "; succ n "zero"; print_string " then (\n";
      unwind n 0 s;
      print_string "      )\n      |\n";
      unwindTill (n-1) s
    end
  else
    begin
      print_string "      if vx = zero then (
         if v = zero then (\n";
      print_string s;
      print_string "      ))"
    end

let plutus n =
  print_string "(* Generated script of the protocol Plutus with ";
  print_int n;
  print_string " versions";
  if !corrected then
    print_string ", corrected"
  else
    print_string ", original";
  if !detailed_lockbox then
    print_string ", detailed lockbox";
  if !signhash_without_enc then
    print_string ", contents hashed and signed unencrypted";
  if !private_readfs then
    print_string ", private readfs";
  print_string " *)

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.";
  if !private_readfs then print_string "

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

(* Contents cannot be retrieved securely from the file system *)
free readfs.";
print_string "

(** 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:corrupt(rx,gx,vx)
		& geq:vx,vy
      	      	& ev:iswriter(rx,gx,vx).  ";
  if !private_readfs then print_string "

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

(* 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).
" else print_string "

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

(* If the server authenticates a write with token tx, then tx belongs to version 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,tx) ==> 
                  ev:iswriter(wx,gx,vx)
	        & ev:istoken(tx,gx,vx).
";
  print_string "
(** 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; ";                                          
 if !private_readfs then print_string "

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

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

         (* 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))
       )";
    revokeTill n;
    print_string "
      |
       (
       ! (* 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";
    if !corrected then
      print_string " let sn = exp(hash((n,g,v)),ownerprivkey) in"
    else
      print_string " let sn = exp(hash(n),ownerprivkey) in";
    print_string "

             (* 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 *)";
  if !detailed_lockbox then 
    print_string "
    new k;
    let encx = (enc(k,lk),enc(m,k)) in

    (* sign *)"
  else
    print_string "
    let encx = enc(m,lk) in

    (* sign *)";
  if !signhash_without_enc then print_string "
    let sencx = exp(hash(m),sk) in"
  else print_string "
    let sencx = exp(hash(encx),sk) in";
  print_string "

    (* 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)).                           
";
 if !private_readfs then print_string "
(** 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))                  
     )
    ).
" else print_string "    
let processServer = 
  ! (* initiate a group g *)
    in(net, g);

    (
     (
     ! (* receive a hash of the current token from g's owner *)
       in(tokenprivchannel(g), hashx);
       
       (* carry the hash of the current token for g *)
       out(tokenprivchannel(g), hashx)
     )
    |
     (
     ! (* 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 *)
       in(tokenprivchannel(g), hashx);
       out(tokenprivchannel(g), hashx);

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

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

       (* write server-verified content *)
       ! out(readfs, content)                         
     )
    ).
";

print_string "
(** 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));  ";
 if !private_readfs then print_string "

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

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

    (* verify signature in header *)";
  if !corrected then
    print_string "
    if hash((n,g,v)) = exp(sn,ownerpubkey) then"
  else
    print_string "
    if hash(n) = exp(sn,ownerpubkey) then";
  print_string "
    (
";
  let evgets = (if !private_readfs then "gets(r,x,g,v,vz)\n" else "gets(r,x,g,v)\n") in
    unwindTill n
	((if ((!signhash_without_enc) && (!detailed_lockbox)) then
"            (* derive vk *) 
            let vk = (genExp(n,lk),n) in

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

            (* verify signature of data *)
            if hash(x) = exp(sencx,vk) then

            (* assert that reader r read data x for group g and version v *)
            event "
	 else if ((!signhash_without_enc) && (not (!detailed_lockbox))) then
"            (* derive vk *)            
            let vk = (genExp(n,lk),n) in

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

            (* verify signature of data *)
            if hash(x) = exp(sencx,vk) then

            (* assert that reader r read data x for group g and version v *)
            event "
         else if (!detailed_lockbox) 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 (encl,encf) = encx in
            let k = dec(encl,lk) in
	    let x = dec(encf,k) in

            (* assert that reader r read data x for group g and version v *)
            event "
         else
"            (* 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 ")^evgets);
    print_string "
    ).

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  
         ) 
"

let _ =
  Arg.parse 
    [ "-corrected", Arg.Set corrected, "\t\tcorrected script, with modulus, version, and group signed";
      "-signhashwithoutenc", Arg.Set signhash_without_enc, "\t\tcontents are hashed and signed unencrypted";
      "-detailedlockbox", Arg.Set detailed_lockbox, "\t\tthe lockbox key encrypts a fresh key, not the file itself";
      "-privatereadfs", Arg.Set private_readfs, "\t\treadfs is a private channel"]
 (fun s -> 
  try 
    plutus (int_of_string s)
  with _ ->
    print_string "Error. Usage: plutusgen [options] n\nwhere n is an integer\n")
  "Plutus script generator"