Paper 2006/011

Formal Proof for the Correctness of RSA-PSS

Christina Lindenberg, Kai Wirt, and Johannes Buchmann

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. 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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Keywords
specificationverificationdigital signature
Contact author(s)
wirt @ informatik tu-darmstadt de
History
2006-01-10: received
Short URL
https://ia.cr/2006/011
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2006/011,
      author = {Christina Lindenberg and Kai Wirt and Johannes Buchmann},
      title = {Formal Proof for the Correctness of RSA-PSS},
      howpublished = {Cryptology ePrint Archive, Paper 2006/011},
      year = {2006},
      note = {\url{https://eprint.iacr.org/2006/011}},
      url = {https://eprint.iacr.org/2006/011}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.