Rob Simmons
Junior Independent Work: Professor 

Abstract:
Automated theorem proving is a powerful tool for expressing and verifying 
mathematical proofs. Besides its applications in representing mathematical 
assertions in a format that can be checked by computers, the idea of a 
computer checked proof can then be applied to understanding properties of
computer programs. One application of this studied by Konrad Slind is proving
the functional correctness of encoding and decoding algorithms*. 

The goal of this project is first to incorporate into an existing higher order
logic framework concepts needed for understanding RSA encryption, and then to 
attempt to prove properties of RSA encryption in the automated theorem proving
framework, with a focus on proving not just functional correctness, but also
potentially proving security properties.

* Slind's paper, "A Verification of AES", can be found at
http://www.cs.utah.edu/~slind/papers/aes.pdf