Contribution: RSA

Correctness of RSA algorithm

Authors

Jose C. Almeida
Laurent Théry

Description

This directory contains the proof of correctness of RSA algorithm. It contains a proof of Fermat's little theorem

Keywords

rsa, chinese remainder, fermat's little theorem

README

This directory contains the proof of correctness of RSA algorithm 
that relies on Fermat's little theorem

To build the directory, do

  coq_makefile *.v > Makefile

Then

  make depend;make all
  

 Laurent Thery & Jose C. Almeida

Available files