Machine-checked security proof of Yao’s SFE protocol

EasyCrypt formalization and corresponding verified implementation of the Yao’s Secure Function Evaluation protocol.

Yao’s SFE EasyCrypt formalization

Link to paper