Verification Contributions

• Gidon Ernst and Lukas Rieger
  Information Flow Testing of a PGP Keyserver
  • Abstract
  • Resources: https://github.com/gernst/verifythis2020
• Diego Diverio, Cláudio Lourenço and Claude Marché
  "You-Know-Why": an Early-Stage Prototype of a Key Server Developed using Why3
  • Abstract
  • Resources: https://gitlab.inria.fr/why3/verifythis2020
• Stijn de Gouw, Mattias Ulbrich and Alexander Weigl
  The KeY Approach on Hagrid
  • Abstract
  • Resources:
    • Keyserver -- A simplified single-class version of the Keyserver using arrays.
    • Map -- A multi-class version using map data types.
• Claire Dross, Johannes Kanig, and Yannick Moy
  A Solution to the Long-Term Challenge in SPARK
  • Abstract
  • Resources: https://github.com/AdaCore/Lumos_Maxima
• Gidon Ernst, Toby Murray and Mukesh Tiwari
  Verifying the Security of a PGP Keyserver
  • Abstract
  • Resources:
    • Case Study (tiny-email.c)
    • paper
    • or the easy-to-access slides
• Mattias Ulbrich
  Event-B Formalisation of the key manager
  • [PDF documentation of the Event-B model
  • Event-B (RODIN) sources are available on request. Just send me a mail (ulbrich@kit.edu).

Alternative Implementations

• in Scala
• in Java