--- Rivest's Oblivious Transfer Protocol, based on the quantum protocol BBCS 
--- see Ronald L. Rivest. "Unconditionally secure commitment and oblivious transfer schemes 
---     using private channels and a trusted initializer." 
---     Unpublished, but available at http://theory.lcs.mit.edu/~rivest/publications.html, November 1999. 


-- Alice has two messages m0, m1 (here, three bits long) unknown to Bob  
-- Bob requests one of the messages 
-- Requirements:
--    1. Bob learns the value of the message requested, but not the other 
--    2. Alice does not learn which message Bob requested


-- Alices two messages: 
m0: Bool[3]
m1: Bool[3]

-- c is Bob's choice of message to receive  
c: Bool

-- Bob's reception buffer 
mc: Bool[3]


-- Random numbers generated by Ted, a trusted third party who sets up 
-- some initial secrets shared by Alice and Bob (but is offline during the protocol)  
r0 : Bool[3]
r1 : Bool[3]
d : Bool
-- rd = if d then r1 else r0 
rd : Bool[3]

-- a value computed by Bob and sent to Alice 
e : Bool
-- values computed by Alice and sent to Bob 
f0 : Bool[3]
f1 : Bool[3]




-- The initial condition says (1) rd = if d then r1 else r0  and (2) not r0=r1
init_cond =   (neg d => ((r0[0] <=> rd[0]) /\ (r0[1] <=> rd[1]) /\ (r0[2] <=> rd[2]))) 
           /\ (d => ((r1[0] <=> rd[0]) /\ (r1[1] <=> rd[1]) /\ (r1[2] <=> rd[2]))) 
           /\ (neg (r0[0] <=> r1[0]) \/ neg (r0[1] <=> r1[1]) \/ neg (r0[2] <=> r1[2]))
           /\ (neg (m0[0] <=> m1[0]) \/ neg (m0[1] <=> m1[1]) \/ neg (m0[2] <=> m1[2]))




agent Alice "alice" (r0, r1, m0, m1, f0, f1, e)

agent Bob "bob" (rd, d, c, f0, f1, mc)



transitions
begin
  if
     Bob.SendRequest   -> e := d xor c
  -- Alice sends f0 = m0 xor r_e and f1 = m1 xor r_{1-e} 
  [] Alice.SendMessages /\ neg e  -> begin
				      f0[0]:= m0[0] xor r0[0];
				      f0[1]:= m0[1] xor r0[1];
				      f0[2]:= m0[2] xor r0[2];
				      f1[0]:= m1[0] xor r1[0];
				      f1[1]:= m1[1] xor r1[1];
				      f1[2]:= m1[2] xor r1[2]	   
				     end
  [] Alice.SendMessages /\ e      -> begin
				      f0[0]:= m0[0] xor r1[0];
				      f0[1]:= m0[1] xor r1[1];
				      f0[2]:= m0[2] xor r1[2];
				      f1[0]:= m1[0] xor r0[0];
				      f1[1]:= m1[1] xor r0[1];
				      f1[2]:= m1[2] xor r0[2]	   
				     end
  -- Bob copmputes mc = f_c xor rd 
  [] Bob.Compute /\ neg c         -> begin
				      mc[0]:= f0[0] xor rd[0];
				      mc[1]:= f0[1] xor rd[1];
				      mc[2]:= f0[2] xor rd[2]	   
				     end
  [] Bob.Compute /\     c         -> begin
				      mc[0]:= f1[0] xor rd[0];
				      mc[1]:= f1[1] xor rd[1];
				      mc[2]:= f1[2] xor rd[2]	   
				     end
  fi
end 

--- specification 


-- If Bob chose m1, then after Alice's transmission, he already knows m1: 
-- (which he computes explicitly in step 3) 
spec_spr_xn = X 2 ( c =>     ((Knows Bob m1[0]) \/ Knows Bob neg m1[0]) /\ 
                             ((Knows Bob m1[1]) \/ Knows Bob neg m1[1]) /\
                             ((Knows Bob m1[2]) \/ Knows Bob neg m1[2])) 


-- Bob's computation in step 3 is correct: 
spec_obs_ltl = X 3 (    c =>   m1[0]==mc[0] /\ m1[1]==mc[1] /\ m1[2]==mc[2])
spec_obs_ltl = X 3 (neg c =>   m0[0]==mc[0] /\ m0[1]==mc[1] /\ m0[2]==mc[2]) 


-- so Bob knows this: 
spec_spr_xn = X 3 ( c => Knows Bob (m1[0]==mc[0] /\ m1[1]==mc[1] /\ m1[2]==mc[2]))
spec_spr_xn = X 3 ( neg c => Knows Bob (m0[0]==mc[0] /\ m0[1]==mc[1] /\ m0[2]==mc[2]))


-- If Bob chose m1 then at the end, he does not know any bit of m0  
spec_spr_xn = X 2 ( c => neg (Knows Bob m0[0]) /\ neg (Knows Bob neg m0[0]) /\ 
                         neg (Knows Bob m0[1]) /\ neg (Knows Bob neg m0[1]) /\ 
                         neg (Knows Bob m0[2]) /\ neg (Knows Bob neg m0[2])) 


-- Alice does not learn Bob's choice: 
spec_spr_xn = X 3 ( (neg Knows Alice c) /\ (neg Knows Alice neg c ) )



spec_spr_xn = X 3 ( neg (Knows Alice (m1[0]==mc[0] /\ m1[1]==mc[1] /\ m1[2]==mc[2])) /\
                    neg  Knows Alice (m0[0]==mc[0] /\ m0[1]==mc[1] /\ m0[2]==mc[2])) 
   
spec_obs_ltl = X 3 neg Knows Alice (Knows Bob (m1[0]==mc[0] /\ m1[1]==mc[1] /\ m1[2]==mc[2]))



-- ALice and Bob's protocols (most of the action is represented in the transitions clause) 


protocol "alice" (r0 : observable Bool[3], r1: observable Bool[3],
                  m0 : observable Bool[3], m1: observable Bool[3], 
                  f0 : observable Bool[3], f1: observable Bool[3], e: observable Bool)

begin
  skip; << SendMessages >>; skip
end


protocol "bob" (rd: observable Bool[3], d: observable Bool, c: observable Bool, 
                f0: observable Bool[3], f1: observable Bool[3], mc: observable Bool[3])
begin
 << SendRequest >>; skip; << Compute >>
end