Na Seminaru za matematičku logiku i osnove matematike, u ponedjeljak 13.
studenog 2017. u 17 sati, u predavaonici 105, PMF-MO, Lovro Rožić će
održati predavanje

Formalni kriptografski dokazi u Coq-u

Sažetak: Dokaziva sigurnost (engl. provable security) je matematički
pristup kriptografiji gdje se sigurnost nekog sustava dokazuje iz zadanog
skupa pretpostavki. Jedan od pristupa je modeliranje protokola i napadača
pomoću probabilističkih programa. Dokazi sigurnosti slijede iz redukcije
sigurnosti nekog "teškog problema" (programa čija sigurnost je
pretpostavljena ili dokazana) na sigurnost programa koji promatramo.
U seminaru se prvo daju osnovne definicije sigurnosti i sigurnosnih
pretpostavki a zatim se pojašnjava pristup kakav se koristi u FCF
(Foundational Cryptography Framework) biblioteci za Coq: denotacijska
semantika u paru s probabilističkom relacijskom Hoareovom logikom (pRHL).
Reference:
A. Petcher, G. Morrisett, The Foundational Cryptography Framework
G. Barthe, S. Z. Beguelin, Formal Cerfitication of Code-Based Cryptograph

Predavanje se može pratiti i on-line na sljedećoj adresi:
https://meduza.carnet.hr/index.php/media/watch/11640.