Decryption errors play a crucial role in the security of KEMs based on Fujisaki-Okamoto because the concrete security guarantees provided by this transformation directly depend on the probability of such an event being bounded by a small real number. In this paper we present an approach to formally verify the claims of statistical probabilistic bounds for incorrect decryption in lattice-based KEM constructions. Our main motivating example is the PKE encryption scheme underlying ML-KEM. We formalize the statistical event that is used in the literature to heuristically approximate ML-KEM decryption errors and confirm that the upper bounds given in the literature for this event are correct. We consider FrodoKEM as an additional example, to demonstrate the wider applicability of the approach and the verification of a correctness bound without heuristic approximations. We also discuss other (non-approximate) approaches to bounding the probability of ML-KEM decryption.

The isogeny-based scheme CSIDH is a promising candidate for quantum-resistant static-static key exchanges with very small public keys, but is inherently difficult to implement in constant time. In the current literature, there are two directions for constant-time implementations: algorithms containing dummy computations and dummy-free algorithms. While the dummy-free implementations come with a 2x slowdown, they offer by design more resistance against fault attacks. In this work, we evaluate how practical fault injection attacks are on the constant-time implementations containing dummy calculations. We present three different fault attacker models. We evaluate our fault models both in simulations and in practical attacks. We then present novel countermeasures to protect the dummy isogeny computations against fault injections. The implemented countermeasures result in an overhead of 7% on the Cortex-M4 target, falling well short of the 2x slowdown for dummy-less variants.