dfirsov

agda-noetherianness

Variations on Noetherianness

agda-programming-with-finite-sets

Dependently Typed Programming with Finite Sets

commitments-non-malleability-ec

Formal Analysis of Non-Malleability for Commitments in EasyCrypt

comparison-based-non-malleabiltiy-unsat

EasyCrypt proof of unsatisfiability of comparison-based definition of non-malleability for commitments

cut-free

easycrypt-multiple-time-blt-signature

Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping

easycrypt-rewinding

Reflection, Rewinding, and Coin-Toss in EasyCrypt -- accompanying EasyCrypt code

easycrypt-zk-code

EasyCrypt formalization of definitions and derivations associated with zero-knowledge (sigma protocols).

jasmin-leakage-freeness

Formalization of leakage-freeness properties for Jasmin programs

jasmin-zk

We implement the Schnorr proof system in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge) and the absence of leakage through timing side-channels of that implementation in EasyCrypt.

dfirsov/jasmin-zk

We implement the Schnorr proof system in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge) and the absence of leakage through timing side-channels of that implementation in EasyCrypt.

dfirsov/easycrypt-zk-code

EasyCrypt formalization of definitions and derivations associated with zero-knowledge (sigma protocols).

dfirsov/agda-noetherianness

Variations on Noetherianness

dfirsov/agda-programming-with-finite-sets

Dependently Typed Programming with Finite Sets

dfirsov/easycrypt-rewinding

Reflection, Rewinding, and Coin-Toss in EasyCrypt -- accompanying EasyCrypt code

dfirsov/jasmin-leakage-freeness

Formalization of leakage-freeness properties for Jasmin programs

dfirsov/commitments-non-malleability-ec

Formal Analysis of Non-Malleability for Commitments in EasyCrypt

dfirsov/comparison-based-non-malleabiltiy-unsat

EasyCrypt proof of unsatisfiability of comparison-based definition of non-malleability for commitments

dfirsov/cut-free

dfirsov/easycrypt-multiple-time-blt-signature

Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping

dfirsov/easycrypt-one-time-blt-signature

Verified Security of BLT Signature Scheme

dfirsov/m2o2c2

Multivariable calculus course materials

dfirsov/yul_to_easycrypt

Yul to EasyCrypt transpiler