Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL. David Butler, David Aspinall and Adria Gascon. To appear in CPP 2020.
David Butler, Andreas Lochbihler, David Aspinall, Adria Gascon, Formalising Sigma-Protocols and Commitment Schemes using CryptHOL, Cryptography ePrint Archive, Report 2019/1185, https://eprint.iacr.org/2019/1185.pdf