Software Verification and Analysis Using Z3

We provide a technical introduction on how to leverage the Z3 Theorem Prover to reason about the correctness of cryptographic software, protocols and otherwise, and to identify potential security vulnerabilities. We cover two distinct use cases: modeling and analysis of an algorithm documented in an old version of the QUIC Transport protocol IETF draft; modeling of specific finite field arithmetic operations for elliptic curve cryptography, with integers represented using a uniform saturated limb schedule, to prove equivalence with arbitrary-precision arithmetic, and for test cases generation.

Double-odd Elliptic Curves

This post is about some new (or sort of new) elliptic curves for use in cryptographic protocols. They were made public in mid-December 2020, on a dedicated Web site: https://doubleodd.group/There is also a complete whitepaper, full of mathematical demonstrations, and several implementations. Oh noes, more curves! Will this never end? It is true that there … Continue reading Double-odd Elliptic Curves

Faster Modular Inversion and Legendre Symbol, and an X25519 Speed Record

Elliptic curves are commonly used to implement asymmetric cryptographic operations such as key exchange and signatures. These operations are used in many places, in particular to initiate secure network connections within protocols such as TLS and Noise. However, they are relatively expensive in terms of computing resources, especially for low-end embedded systems, which run on … Continue reading Faster Modular Inversion and Legendre Symbol, and an X25519 Speed Record

Pairing over BLS12-381, Part 2: Curves

This is the second of three code-centric blog posts on pairing based cryptography. The first post [1] covered modular arithmetic, finite fields, the embedding degree, and presented an implementation of a 12-degree prime extension field tower. The series will ultimately conclude with a detailed review of the popular BLS12-381 pairing operations found in a variety … Continue reading Pairing over BLS12-381, Part 2: Curves

Curve9767 and Fast Signature Verification

This post is about elliptic curves as they are used in cryptography, in particular for signatures. There are many ways to define specific elliptic curves that strive to offer a good balance between security and performance; here, I am talking about specific contributions of mine: a new curve definition, and some algorithmic improvements that target … Continue reading Curve9767 and Fast Signature Verification