Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/RSAPSS/document/   (Sammlung formaler Beweise Version 2026-5©)  Datei vom 29.4.2026 mit Größe 5 kB image not shown  

Quelle  root.bib

  Sprache: Latech
 

@inproceedings{ Backes-Pfitzmann:04Symmetric,
  author    = {Michael Backes and Birgit Pfitzmann},
  title     = {Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library.},
  booktitle = {CSFW},
  year      = {2004},
  pages     = {204-218},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.20}
}

@Article{ Bellare-Rogaway:96Exact,
  author = "{Mihir Bellare and Phillip Rogaway}",
  title = "{The Exact Security of Digital Signatures --- How to Sign with RSA and Rabin}",
  journal = "{Lecture Notes in Computer Science}",
  volume = "{1070}",
  pages = "{399--416}",
  year = "{1996}",
  url = "{http://www.cs.ucdavis.edu/~rogaway/papers/exactsigs-abstract.html}"
}

@Article{ Bellare-Rogaway:98PSS,
  author = "{Mihir Bellare and Phillip Rogaway}",
  title = "{{PSS}: Provably Secure Encoding Method for Digital Signatures}",
  journal = "{Submission to IEEE P1363}",
  year = "{1998}",
  url = "{http://www.cs.ucdavis.edu/~rogaway/papers/exactsigs-abstract.html}"
}

@inproceedings{ Bellare-Rogaway:93Randomoracle,
  author    = {Mihir Bellare and Phillip Rogaway},
  title     = {Random Oracles are Practical: A Paradigm for Designing Efficient
               Protocols.},
  booktitle = {ACM Conference on Computer and Communications Security},
  year      = {1993},
  pages     = {62-73},
  ee        = {http://doi.acm.org/10.1145/168588.168596},
}

@TechReport{ Boyer-Moore:82RSA,
  author =   {Robert S. Boyer and J. Strother Moore},
  title =   {Proof Checking the RSA Public Key Encryption Algorithm},
  institution =  {Institute for Computing Science and Computer Applications, University of Texas},
  year =   {1982},
  number =   {33}
}

@Book{ Buchmann:04Kryptographie,
  ALTauthor =   {Johannes Buchmann},
  title =   {Einführung in die Kryptographie},
  publisher =   {Springer},
  year =   {2004}
}


@Article{ Dolev-Yao:83SecurityPKP,
  author =   {Danny Dolev and Andrew C. Yao},
  title =   {On the Security of Public Key Protocols},
  journal =   {IEEE Transactions on Information Theory},
  year =   {1983},
  volume =   {29},
  number =   {2},
  pages =   {198-208}
}

@inproceedings{ Fujisaki-Okamoto-Pointcheval-Stern:01OAEP,
  author    = {Eiichiro Fujisaki and
               Tatsuaki Okamoto and
               David Pointcheval and
               Jacques Stern},
  title     = {{RSA-OAEP} Is Secure under the {RSA} Assumption.},
  booktitle = {CRYPTO},
  year      = {2001},
  pages     = {260-274},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2139/21390260.htm},
}

@TechReport{ Kaiser-Lindenberg-Wirt:04SHA1,
  author =   {Markus Kaiser and Christina Lindenberg and Kai Wirt},
  title =   {Formal specification of the Secure Hash Algorithm},
  institution =  {Verisoft Projekt, TU Darmstadt},
  year =   {2004},
  number =   {49},
}

@TechReport{ Lindenberg-Wirt:04RSA,
  author =   {Christina Lindenberg and Kai Wirt},
  title =   {Formaler Korrektheitsbeweis von RSA mit Hilfe von Isabelle/HOL},
  institution =  {Verisoft Projekt, TU Darmstadt},
  year =   {2004},
  number =   {16},
}

@TechReport{Lindenberg-Wirt:04PSS,
  author =   {Christina Lindenberg and Kai Wirt},
  title =   {Das RSA - PSS Signaturverfahren},
  institution =  {Verisoft Projekt, TU Darmstadt},
  year =   {2004},
  number =   {17},
}

@Book{ Nipkow-Paulson-Wenzel:02Isabelle,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title  = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher = {Springer},
  series = {LNCS},
  volume = 2283,
  year  = 2002}

@Book{ Menezes:97Handbook,
  title = {Handbook of Applied Cryptography},
  author = {Alfred J. Menezes and Paul van Oorschot and Scott Vanstone},
  publisher = {{CRC} Press},
  year = {1997},
  url = {http://www.cacr.math.uwaterloo.ca/hac/},
}

@Techreport{ PKCS,
  author = {PKCS Editor},
  institution = "{RSA Laboratories}",
  title = "{PKCS\#1 v$2.1$: RSA Cryptography Standard}",
  year = "{2002}",
  url = "{http://www.rsasecurity.com/rsalabs/node.asp?id=2125}"
}


@Article{ Rivest-Shamir-Adleman:78RSA,
  author    = {Ronald L. Rivest and Adi Shamir and Leonard M. Adleman},
  title     = {A Method for Obtaining Digital Signatures and Public-Key Cryptosystems.},
  journal   = {Commun. ACM},
  volume    = {21},
  number    = {2},
  year      = {1978},
  pages     = {120-126}
}

@misc{ TU-Munich:05Isabelle,
  title     = {Development Website of Isabelle at the TU Munich},
  howpublished = {http://isabelle.in.tum.de},
  key       = {Isabelle},
}

@techreport{ fips:02SHA,
  title     = {Secure Hash Standard},
  author    = {Federal Information Processing Standards},
  institution = {National Institute of Standards and Technology},
  year      = {2002},
  number    = {FIPS 180-2},
}

@misc{ computeraircraft,
  title     = {Computer Related Incidents with Commercial Aircraft},
  author    = {Peter B. Ladkin},
  institution = {University of Bielefeld, Faculty of Technology - Networks and Distributed Systems},
  howpublished = {http://www.rvs.uni-bielefeld.de/publications/Incidents/},
}

@misc{ softwarebugs,
  title     = {Collection of Software Bugs},
  author    = {Thomas Huckle},
  institution = {TU München, Institut für Informatik},
  howpublished = {http://www5.in.tum.de/\~{}huckle/bugse.html},
  year      = {2004},
}

@misc{ wikipedia,
  title     = {Article Computer Bug},
  howpublished = {http://en.wikipedia.org/wiki/Computer\_bug},
  key       = {Wikipedia}
}

@misc{ wang-yin-yu:05sha,
  author    = {Xiaoyun Wang and Yiqun Lisa Yin and Hongbo Yu},
  title     = {Collision Search Attacks on SHA1},
  year      = {2005},
  howpublished = {http://theory.csail.mit.edu/\~{}yiqun/shanote.pdf},
}

Messung V0.5 in Prozent
C=100 H=100 G=100

¤ Dauer der Verarbeitung: 0.2 Sekunden  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.