Formal Proof for the Correctness of RSA-PSS.
Christina Lindenberg, Kai Wirt, Johannes A Buchmann · 2006
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. This paper is one step to provide a tool box allowing the use of formal methods in every aspect of cryptography. In this paper we give a formal specification of the RSA probabilistic signature scheme (RSA-PSS) [4] which is used as algorithm for digital signatures in the PKCS #1 v2.1 standard [7]. Additionally we show the correctness of RSA-PSS. This includes the correctness of RSA, the formal treatment of SHA-1 and the correctness of the PSS encoding method. Moreover we present a proof of concept for the feasibility of verification techniques to a standard signature algorithm. Keywords: cryptography, specification, verification, digital signature 1 Motivation Todays software often contains many errors which are not discovered during the development. Although erroneous software is mostly only annoying, bugs may lead to severe security issues as well. Moreover bugs even can have huge impacts if they appear in software used for critical applications such as controlling software in nuclear power plants. There are various examples of computer related accidents which led to loss of lives like the crash of the Korean Air Lines B747 in Guam 1997 or the Therac-25 radiation-therapy machine which gave patients massive overdoses between 1985 and 1987 [11], [9], [16]. The reason for such poor software is, that not all errors can be found by tests. Even if programs are very intensively tested they may still contain several more or less severe bugs. A possible solution to this dilemma is the formal verification of software. The goal of the application of formal methods in program verification is to prove the corre...