SHA1, RSA, PSS and more

 

Title:	SHA1, RSA, PSS and more
Author:	Christina Lindenberg and Kai Wirt
Submission date:	2005-05-02
Abstract:	Formal verification is getting more and more important in computer science. However the state of the art formal verification methods in cryptography are very rudimentary. These theories are one step to provide a tool box allowing the use of formal methods in every aspect of cryptography. Moreover we present a proof of concept for the feasibility of verification techniques to a standard signature algorithm.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-RSAPSS-2009-04-29.tar.gz Isabelle 2008: afp-RSAPSS-2008-06-10.tar.gz Isabelle 2007: afp-RSAPSS-2007-11-27.tar.gz Isabelle 2005: afp-RSAPSS-2005-10-14.tar.gz