Alin Tomescu

$ $ This post surveys some concerning attacks on TEEs.

tl;dr: Constructive cryptography (CC) is a definitional framework for security proofs by Uli Maurer. $ $ Introduction Constructive cryptography (CC)1 was developed in parallel with the abstract cryptography framework by Maurer and Renner2 and borrows from…

$ $ Common types in Lean (e.g., Bool) are not primitives of the language.

tl;dr: “Beware of bugs in the above code; I have only proved it correct, not tried it.”

tl;dr: I wish there was better stuff around than UC for modelling security of cryptosystems. $ $ Links Andrew Miller’s course List of papers that introduce UC functionalities, from a Google Doc in this course For future reference, equivalent AI-generated…

tl;dr: This is an incomplete and opinionated take on three different approaches to confidential payments (and beyond). $ $ Aptos Good: Encrypts balances under the owning user’s encryption key $\Rightarrow$ no one can see the balance, except the owning user

tl;dr: A bunch of resources I hope to get to. $ $ Cryptography Verified-zkEVM VCVio ArkLib clean zkDSL zkLean: A DSL for ZK statement verification Software engineering in Lean Why lean is faster than Rust Lean proved this program was correct; then I found…

tl;dr: When the discrete log $a$ of $a\cdot G$ is known to lie in a small range $[m)$, the baby-step giant-step (BSGS) algorithm recovers $a$ in $\ceil{\sqrt{m}}$ $\Gr$ additions using only a precomputed table of exactly $\ceil{\sqrt{m}}$ compressed point…

tl;dr: The good: Audit went well.

tl;dr: Running some secp256k1 MSM benchmarks. $ $ Background For ECDSA verification and pubkey recovery, the relevant MSM size is $n=2$.

tl;dr: Groth’s non-interactive distributed key generation paper1, which uses a novel approximate ZK range proofs to argue correct chunking, but inadvertantly increases share decryption time. $ % \def\ek{\mathsf{ek}} \def\dk{\mathsf{dk}} \def\Gone{G_1} \de…

tl;dr: a few notes on Move (and maybe on Aptos too). $ $ Misc Move 1 to Move 2, by Greg Nazario Keyless on-chain configs Learn more about Keyless here. 0x1::keyless_account::Groth16VerificationKey devnet VK testnet VK mainnet VK 0x1::keyless_account::Conf…

tl;dr: This is a “note to self” that there’s some interesting work out there on malleable NIZKs1$^,$2. $ $ References For cited works, see below 👇👇 Shorter Non-Interactive Zero-Knowledge Arguments and ZAPs for Algebraic Languages, by Geoffroy Couteau and…

tl;dr: Some notes to self on state-of-the-art witness encryption (WE) schemes. $ \def\adp{\mathsf{ADP}} \def\aadp{\mathsf{AADP}} \def\eval{\mathsf{eval}} \def\x{\mathbf{x}} \def\M{\mathsf{M}} \def\A{\mathbf{A}} \def\B{\mathbf{B}} \def\R{\mathbf{R}} \def\R…

tl;dr: What has happened in quantum computing over the years. $ $ A history In 2001, Vandersypen et al. claimed an “experimental realization” of Shor’s quantum factoring algorithm1.