A Brief Look at the EasyUC Mechanized Proof Framework

  • Tagung:

    A Brief Look at the EasyUC Mechanized Proof Framework

  • Tagungsort:

    252 / BBB

  • Datum:

    2026-06-09

  • Referent:

    Christian Martin

  • Zeit:

    15:45

  • In the Universally Composable Security framework, proofs are often complex and prone to errors. Petrovic et al. are developing the EasyUC architecture [1] in order to mechanize the verification of such proofs with the EasyCrypt proof assistant. In this talk, I will give an overview of EasyUC based on the introductory paper [2].

    [1] https://github.com/easyuc/EasyUC/
    [2] R. Canetti, A. Stoughton and M. Varia, "EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security", 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), Hoboken, NJ, USA, 2019, pp. 167-16716, doi: 10.1109/CSF.2019.00019, eprint: 2019/582.