Pinned Repositories
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-one-time-blt-signature
Verified Security of BLT Signature Scheme
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-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's Repositories
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-rewinding
Reflection, Rewinding, and Coin-Toss in EasyCrypt -- accompanying EasyCrypt code
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/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/jasmin-leakage-freeness
Formalization of leakage-freeness properties for Jasmin programs
dfirsov/m2o2c2
Multivariable calculus course materials
dfirsov/yul_to_easycrypt
Yul to EasyCrypt transpiler