cryspen/bertie

Issues

• Backport F* proofs to Rust and remove patches

  #115 opened 7 months ago by karthikbhargavan
  2

• Speedup hax CI job

  #123 opened 4 months ago by franziskuskiefer
  1

• Implement PQ hybrid handshake

  #122 opened 4 months ago by jschneider-bensch
  0

• [ProVerif] Extraction / analysis is not on CI

  #106 opened 7 months ago by jschneider-bensch
  0

• [ProVerif] Incorporate code changes from Proving Panic Freedom in F* #112 into ProVerif model

  #116 opened 7 months ago by jschneider-bensch
  1

• Security Proofs

  #15 opened 7 months ago by franziskuskiefer
  1

• [Feature request]

  #114 opened 7 months ago by karthikbhargavan
  2

• [Feature request] Gate extractions to F* and ProVerif behind a single feature `hax`

  #109 opened 7 months ago by jschneider-bensch
  1

• Lax typecheck

  #86 opened 7 months ago by franziskuskiefer
  3

• Typecheck Bertie

  #28 opened 7 months ago by franziskuskiefer
  0

• This would look nicer with a `range` instead of `start` and `end` arguments. Not sure if hax/F* can handle that though.

  #113 opened 7 months ago by franziskuskiefer
  0

• [Bug] Record protocol counters may overflow

  #111 opened 7 months ago by karthikbhargavan
  0

• [Bug] Trunc Length in Client Hello

  #110 opened 7 months ago by karthikbhargavan
  0

• [ProVerif] Remove unnecessary auto-generated events from model

  #104 opened 7 months ago by jschneider-bensch
  1

• [ProVerif] Insert handwritten model parts automatically instead of manual patching

  #105 opened 7 months ago by jschneider-bensch
  0

• [ProVerif] Demonstrate the ProVerif model is working via reachability analysis

  #100 opened 7 months ago by jschneider-bensch
  1

• Bertie Verification Workplan

  #89 opened 7 months ago by karthikbhargavan
  0

• Clean up state machines

  #82 opened 7 months ago by franziskuskiefer
  1

• Correctness Proofs

  #14 opened 2 years ago by franziskuskiefer
  0

• Disable audit CI

  #95 opened 8 months ago by franziskuskiefer
  1

• Pin Bogo

  #97 opened 8 months ago by franziskuskiefer
  0

• API Documentation

  #6 opened 9 months ago by franziskuskiefer
  0

• Improve Performance

  #12 opened 9 months ago by franziskuskiefer
  0

• Benchmarks

  #10 opened 9 months ago by franziskuskiefer
  0

• Performance comparison

  #11 opened 9 months ago by franziskuskiefer
  0

• Integrate BoringSSL test suite (BoGo)

  #30 opened 2 years ago by duesee
  2

• Continuous Integration

  #8 opened 2 years ago by franziskuskiefer
  0

• Interop tests

  #9 opened a year ago by franziskuskiefer
  0

• Add F* extraction to CI

  #63 opened a year ago by franziskuskiefer
  1

• [meta] TLS test suite

  #7 opened a year ago by franziskuskiefer
  0

• https://github.com/xvzcf/tls-interop-runner

  #48 opened a year ago by franziskuskiefer
  1

• [Bug] Incorrect parsing of large handshake messages

  #74 opened a year ago by franziskuskiefer
  1

• Rework handling of randomness

  #73 opened a year ago by jschneider-bensch
  0

• [Feature request] Support ciphersuite / algorithms argument for `simple_https_server`

  #66 opened a year ago by jschneider-bensch
  2

• Rework RSA privkey handling

  #72 opened a year ago by jschneider-bensch
  0

• [Feature request] Support multiple ciphersuites in Bertie

  #51 opened 2 years ago by franziskuskiefer
  1

• Add F* typechecking to CI

  #64 opened a year ago by franziskuskiefer
  0

• Evaluate (and integrate) TLS-Anvil.

  #31 opened 2 years ago by duesee
  0

• Add Bertie to TLS-Docker-Library.

  #32 opened 2 years ago by duesee
  0

• Record payload protection

  #54 opened 2 years ago by franziskuskiefer
  0

• Clippy: Fix "this is a decimal constant"

  #53 opened 2 years ago by duesee
  0

• Connection issues

  #52 opened 2 years ago by franziskuskiefer
  0

• Cleanup `simple_https_server`.

  #50 opened 2 years ago by duesee
  0

• https://github.com/tlsfuzzer/tlsfuzzer

  #49 opened 2 years ago by franziskuskiefer
  1

• [Bug] Broken build.

  #37 opened 2 years ago by duesee
  0

• Add Readme

  #19 opened 2 years ago by franziskuskiefer
  1

• Setup contribution guidelines

  #5 opened 2 years ago by franziskuskiefer
  0

• Add license

  #20 opened 2 years ago by franziskuskiefer
  0

• Cleanup cryptolibs and make them public

  #16 opened 2 years ago by franziskuskiefer
  0

• TLS 1.3 Formal Specification

  #13 opened 2 years ago by franziskuskiefer
  0