## Certifying RSA correct for breakfast

** Published:**

Reasoning on *the correctness* of the RSA cryptosystem is much easier with a little bit of algebra: this is a perfect example of a case where the ``practical’’ applications of proof assistants can be helped with libraries dealing with abstract algebra, including SSReflect. The proof we are going to build in the present post is based on a stock SSReflect version 1.3pl1, and is available on github. It can be compared with the RSA contribution to Coq, made on the basis of the standard library (note this is not a code golf, but rather a tentative to demonstrate that a big mathematical library helps).