## Author: Christoph Walther

## Paper Information

Title: | Formally Verified Montgomery Multiplication |

Authors: | Christoph Walther |

Proceedings: | CAV All Papers |

Editors: | Georg Weissenbacher, Hana Chockler and Igor Konnov |

Keywords: | Modular Arithmetic, Montgomery Multiplication, Program Verification, Theorem Proving by Induction |

Abstract: | ABSTRACT. We report on a machine assisted verification of an efficient implementation of Montgomery Multiplication which is a widely used method in cryptography for efficient computation of modular exponentiation. We shortly describe the method, give a brief survey of the VeriFun system used for verification, verify a classical as well as a more recent algorithm for computing multiplicative inverses, illustrate proof-technical obstacles encountered upon verification, present the formal proofs and finally report on the effort when creating the proofs. Our work uncovered a serious fault in a state-of-the-art algorithm for computing multiplicative inverses based on Newton-Raphson iteration, thus providing further evidence for the benefit of computer-aided verification. |

Pages: | 17 |

Talk: | Jul 17 17:15 (Session 122A: CPS, Hardware, Industrial Applications) |

Paper: |