================================================================
check bidding-price-secrecy for non-winning bidders
================================================================
We fix four prices - constants p1, p2, p3, p4 - as the price list.
We fix nextprice(p4)=p3, nextprice(p3)=p2, nextprice(p2)=p1, nextprice(p1)=tail.
It is assumed that there are two arbitrary bidders.
One of them bids for the highest price, as the winning bidder. 
----------------------------------------------------------------
(* Channel declaration *)

(*public channels*)
free pubch.          (*public channel*)
free ch1.            (*public channel between bidder 1 and auctioneer*)
free ch2.            (*public channel between bidder 2 and auctioneer*)

(*private channels*)
private free prvch.
private free untapch.


(* Signature *)
fun b1/0.            (*first bidder*)
fun b2/0.            (*second bidder*)
fun p1/0.            (*first price in price list*)
fun p2/0.            (*second price in price list*)
fun p3/0.            (*third price in price list*)
fun p4/0.            (*fourth price in price list*)
fun yes/0.           (*message "I bid"*)
fun no/0.            (*message "I do not bid"*)
fun true/0.          (*constant*)
fun pk/1.            (*public key*)
fun commit/3.        (*bit commitment*)
fun sign/2.          (*digital signature*)
fun checksign/2.     (*open digital signature*)
fun getmsg/1.        (*get original message from signed message*)
fun cmttuple/4.      (*a tuple with four elements, each stands for a bit commitment for one price*)
fun first/1.         (*first element in a tupple*)
fun snd/1.           (*second element in a tupple*)   
fun third/1.         (*third element in a tupple*)
fun fourth/1.          (*fourth element in a tupple*)


(* Equational theory *)
equation checksign(pk(sk),sign(m,sk))=true.
equation getmsg(sign(m,n))=m.
equation first(cmttuple(m,n,l,s))=m.
equation snd(cmttuple(m,n,l,s))=n.
equation third(cmttuple(m,n,l,s))=l.
equation fourth(cmttuple(m,n,l,s))=s.
equation open(commit(r,k,m), r, k)=m.

(* Property -- standard secrecy of vp1, vp2, vp3 *)
query attacker: vp1.
query attacker: vp2.
query attacker: vp3.

(* Property -- strong secrecy of vp1, vp2, vp3 *)
private free vp1,vp2,vp3,vp4.
noninterf vp1 among (yes,no), vp2 among (yes,no), vp3 among (yes,no). 


(*Process definitions*)

(*free variables: ch -- bidder's own public channel,
                  privch -- private channel for each bidder,
		  untapch -- untapped channel for each bidder,
		  sskb -- bidder's secret key as signature,
		  cmtp1,cmtp2,cmtp3,cmtp4 -- bit commitment generated by each bidder,
		  vp1,vp2,vp3,vp4 -- private variables *)
let processB= (*bidders signature private key*)
              in(privch,sskb);

              (*choose secret key*)
              new skb;

              (*publish public key*)          
              out(ch, sign(pk(skb),sskb));

              (*random choose secret seeds*)
              new rp1; new rp2; new rp3; new rp4;

              (*generate bit commitment*)
              let cmtp1=commit(rp1,pk(skb),vp1) in 
              let cmtp2=commit(rp2,pk(skb),vp2) in
              let cmtp3=commit(rp3,pk(skb),vp3) in
              let cmtp4=commit(rp4,pk(skb),vp4) in
              out(ch,  sign( cmttuple(cmtp1,cmtp2,cmtp3,cmtp4) ,sskb)  );
              out(untapch,(rp1,rp2,rp3,rp4));
              phase 1.


(*free variables: spkb1 -- public key for signature of bidder 1,
                  spkb2 -- public key for signature of bidder 2,
		  vpkb1 -- signatured public key of bidder 1,
		  vpkb2 -- signatured public key of bidder 2,
		  pkb1 --  public key of bidder 1,
		  pkb2 --  public key of bidder 2,
		  vcmt1 -- commitment tuple for bidder 1,
		  vcmt2 -- commitment tuple for bidder 2,
                  synch -- private channel *)
let processA=
              (*first bidder*)
	      (*read public key for bidder's signature from public channel*)
	      in(pubch,spkb1); 
         
              (*read bidder's own generated public key from bidder's public channel*)
              in(ch1,vpkb1);
              (*check signature and get public key*)
              if checksign(spkb1,vpkb1)=true 
              then let pkb1=getmsg(vpkb1) in 

	      (*read commitments from bidder's public channel*)	
              in(ch1,vcmt1);
	      (*check signature and get commitments tuple*)
              if checksign(spkb1,vcmt1)=true         
              then let cmtb1=getmsg(vcmt1) in 

              (*read secret shares from bidder's untapped channel*)
              in(untapch1,(ssb1r1,ssb1r2,ssb1r3,ssb1r4));out(synch,b1)|

	      (*second bidder, process is the same as the first bidder *)
              in(pubch,spkb2);
              in(ch2,vpkb2);
              if checksign(spkb2,vpkb2)=true 
              then let pkb2=getmsg(vpkb2) in 
              in(ch2,vcmt2);
              if checksign(spkb2,vcmt2)=true 
              then let cmtb2=getmsg(vcmt2) in 
              in(untapch2,(ssb2r1,ssb2r2,ssb2r3,ssb2r4));out(synch,b2)|
              
	      (*read finishing signal from each bidder *)
              in(synch,v1);in(synch,v2);phase 1;

	      (*open commitments, find winning price *)

	      (*checking price P4 *)
              if fourth(cmtb1)=commit(ssb1r4,pkb1,yes)
              then out(pubch,(p4,b1));
                   if fourth(cmtb2)=commit(ssb2r4,pkb2,yes)
                   then out(pubch,(p4,b2));0
                   else 0
              else if fourth(cmtb2)=commit(ssb2r4,pkb2,yes)
                   then out(pubch,(p4,b2));0

	      (*checking price P3 *)                   
                   else if third(cmtb1)=commit(ssb1r3,pkb1,yes)
                        then out(pubch,(p3,b1));
                             if third(cmtb2)=commit(ssb2r3,pkb2,yes)
                             then out(pubch,(p3,b2));0
                             else 0
                        else if third(cmtb2)=commit(ssb2r3,pkb2,yes)
                             then out(pubch,(p3,b2));0

	      (*checking price P2 *)     
                             else if snd(cmtb1)=commit(ssb1r2,pkb1,yes)
                                  then out(pubch,(p2,b1));
                                       if snd(cmtb2)=commit(ssb2r2,pkb2,yes)
                                       then out(pubch,(p2,b2));0 
                                       else 0                                                  
                                  else if snd(cmtb2)=commit(ssb2r2,pkb2,yes)
                                       then out(pubch,(p2,b2));0

	      (*checking price P1 *)      
                                       else if first(cmtb1)=commit(ssb1r1,pkb1,yes)
                                            then out(pubch,(p1,b1));
                                                 if first(cmtb2)=commit(ssb2r1,pkb2,yes)
                                                 then out(pubch,(p1,b2));0
                                                 else 0
                                            else if first(cmtb2)=commit(ssb2r1,pkb2,yes)
                                                 then out(pubch,(p1,b2));0.
                                                                   
      
(* Protocol *)
process 
	(*private channels*)
	new untapch1;new untapch2; new privchb1; new privchb2;new synch;

	(*private keys*)
	new sskb1;new sskb2;

	(*public keys*)
	let spkb1=pk(sskb1) in
	let spkb2=pk(sskb2) in

	(
	(*keys disclosure on private channals*)
	out(pubch,spkb1)|out(pubch,spkb2)|
	out(privchb1,sskb1)|out(privchb2,sskb2)|

	(*one bidder*)   
        let vp4=no in
	let privch=privchb1 in
	let untapch=untapch1 in
	let ch=ch1 in
	processB|

	(*winning bidder*)
        let vp1=no in
	let vp2=no in
	let vp3=no in
	let vp4=yes in
	let privch=privchb2 in
	let untapch=untapch2 in
	let ch=ch2 in
	processB|
	
	(*auctioneer*)
        processA

	)





============================================================================
For checking the second equivalence of reciept-freeness of the AS02 protocol
=============================================================================
We fix three prices - constants p1, p2, p3 - as the price list. We do not need
four prices. Three prices is enough. Price p3 represents the highest price, which
the winning bidder bids for. Price p1 represents the lowest price, which the 
adversary asks the bidder to bid for. Price p2 represents the price that the bidder 
actually bids for. Price p2 is lower than p3, therefore, p2 is not the wining price.
Price p2 is higher than p1, therefore, the bidder bids higher than what he is cocered
to bid.It is assumed that there are two arbitrary bidders.One of them bids for 
the highest price, as the winning bidder. In the auctionner process, we stop
the process after cheching price p3, because we know the process will stop, given 
the auctioneer is honest as assumption. 
-------------------------------------------------------------------
(* Channel declaration *)
free pubch.             (*public channel*)
free pubch1.            (*public channel between bidder 1 and auctioneer*)
free pubch2.            (*public channel between bidder 2 and auctioneer*)


private free prvch.
private free untapch.



(* Signature *)
fun b1/0.            (*first bidder*)
fun b2/0.            (*second bidder*)
fun p1/0.            (*first price in price list*)
fun p2/0.            (*second price in price list*)
fun p3/0.            (*third price in price list*)
fun yes/0.           (*message "I bid"*)
fun no/0.            (*message "I do not bid"*)



fun pk/1.            (*public key*)
fun commit/3.        (*bit commitment*)
fun sign/2.          (*digital signature*)
fun checksign/2.     (*open digital signature*)
fun cmttuple/3.      (*a tuple with four elements, each stands for a bit commitment for one price*)
fun first/1.         (*first element in a tuple*)
fun snd/1.           (*second element in a tuple*)   
fun third/1.         (*third element in a tuple*)
fun f/1.             (*generate a fake random number in order to send to coercer*)

(* Equational theory *)
equation checksign(pk(sk),sign(m,sk))=m.
equation first(cmttuple(m,n,l))=m.
equation snd(cmttuple(m,n,l))=n.
equation third(cmttuple(m,n,l))=l.
equation commit(f(r),k,no)=commit(r,k,yes).
equation commit(f(r),k,yes)=commit(r,k,no).
equation open(commit(r,k,m), r, k)=m.

(* Protocol *)
process 
	(*private channels*)
        new privchb1; new privchb2; 
	new untapch1; new untapch2; new synch;

	(*private keys*)
	new sskb1;new sskb2;

	(*public keys*)
	let spkb1=pk(sskb1) in
	let spkb2=pk(sskb2) in

	(
	(*keys disclosure on private channals*)
	out(pubch,spkb1)|out(pubch,spkb2)|
	out(privchb1,sskb1)|out(privchb2,sskb2)|
        
              (*bidders signature private key*)
              in(privchb1,sskb1);
              out(pubch,sskb1);

              (*choose secret key*)
              new skb1;
              out(pubch,skb1);

              (*publish public key*)          
             (* out(pubch1, sign(pk(skb1),sskb1));*)
              out(pubch, sign(pk(skb1),sskb1));

              (*random choose secret seeds*)
              new rp1; new rp2; new rp3;

              (*generate bit commitment*)
              let cmtp1=commit(rp1,pk(skb1),yes) in 
              let cmtp2=commit(rp2,pk(skb1),no) in
              let cmtp3=commit(rp3,pk(skb1),no) in
              let frp1=f(rp1) in
              let frp2=f(rp2) in
              out(pubch1, sign(cmttuple(cmtp1,cmtp2,cmtp3),sskb1));
              out(pubch, sign(cmttuple(cmtp1,cmtp2,cmtp3),sskb1));
              out(untapch1, choice[cmttuple(frp1,frp2,rp3),cmttuple(rp1,rp2,rp3)]);
              out(pubch,cmttuple(rp1,rp2,rp3));
              phase 1
             | 
              (*winning bidder signature private key*)
              in(privchb2,sskb2);

              (*choose secret key*)
              new skb2;

              (*publish public key*)          
              out(pubch2, sign(pk(skb2),sskb2));

              (*random choose secret seeds*)
              new wrp1; new wrp2; new wrp3;

              (*generate bit commitment*)
              let wcmtp1=commit(wrp1,pk(skb2),no) in 
              let wcmtp2=commit(wrp2,pk(skb2),no) in
              let wcmtp3=commit(wrp3,pk(skb2),yes) in
              out(pubch, sign(cmttuple(wcmtp1,wcmtp2,wcmtp3),sskb2)  );
              out(untapch2, cmttuple(wrp1,wrp2,wrp3));
              phase 1
             |
              (*first bidder*)
	      (*read public key for bidder's signature from public channel*)
	      in(pubch,spkb1); 
         
              (*read bidder's own generated public key from bidder's public channel*)
              in(pubch1,vpkb1);

              (*check signature and get public key*)
              let pkb1=checksign(spkb1,vpkb1) in 

	      (*read commitments from bidder's public channel*)	
              in(pubch1,vcmt1);
	      (*check signature and get commitments tuple*)    
              let cmtb1=checksign(spkb1,vcmt1) in 

              (*read secret shares from bidder's untapped channel*)
              in(untapch1,vssb1);out(synch,b1)|

	      (*second bidder, process is the same as the first bidder *)
              in(pubch,spkb2);
              in(pubch2,vpkb2);   
              let pkb2=checksign(spkb2,vpkb2) in 
              in(pubch2,vcmt2);
              let cmtb2=checksign(spkb2,vcmt2) in 
              in(untapch2,vssb2);out(synch,b2)|
              
	      (*read finishing signal from each bidder *)
              in(synch,v1);in(synch,v2);phase 1;

	      (*open commitments, find winning price *)

	      (*checking price p3 *)
              out(pubch,third(vssb1));
              out(pubch,third(vssb2));
              if third(cmtb1)=commit(third(vssb1),pkb1,yes)
              then out(pubch,p3);
                   out(pubch,b1)
              else if third(cmtb2)=commit(third(vssb2),pkb2,yes)
                   then out(pubch,p3);
                        out(pubch,b2)
      )