Modelling Oblivious Transfer in EasyCrypt

We describe how to construct an oblivious transfer protocol which security is based on subset membership problems and smooth projective hash functions. A specific protocol based on the two-message oblivious transfer protocols of Kalai (2005) and the encryption schemes presented by Cramer and Shoup (2002) is presented. In addition, the protocol is modelled in EasyCrypt and we use the program to prove the security, which is based on the Decisional Diffie-Hellman assumption. We encountered challenges using the program, which is under development. The stability of EasyCrypt was a problem. Axioms that were important for our implementation were not available, and the necessary information on syntax needed to define new modules and lemmas was inadequate. We had to rewrite existent- and compose many new lemmas. We also found a critical error in EasyCrypt, which was given high priority by the team behind EasyCrypt, and has now been corrected. However, our proofs had to surround the problem and became more complicated. We also concluded that EasyCrypt is not developed primarily for doing algebra, resulting in unnecessary complicated codes for the proof of our protocol