Code

ProVerif Handshake Model#98

Code

Merged

jschneider-bensch merged 52 commits intomaincryspen/bertie:mainfrom jonas/pv-handshake-annotationscryspen/bertie:jonas/pv-handshake-annotationsCopy head branch name to clipboardApr 2, 2024

+3,659-1,406

Commits

Commits on Mar 11, 2024

• Handwritten lib is not part of extraction

  jschneider-bensch

  committed
  9cd1b62

  Copy full SHA for 9cd1b62

• Depend on hax-lib-macros

  Show description for 1d11fb3
  jschneider-bensch

  committed
  1d11fb3

  Copy full SHA for 1d11fb3

• Annotate handwritten / constructor fns, update driver command

  jschneider-bensch

  committed
  2cc2414

  Copy full SHA for 2cc2414

Commits on Mar 12, 2024

• Latest generated model

  jschneider-bensch

  committed
  578f757

  Copy full SHA for 578f757

• Include models for tls13utils

  jschneider-bensch

  committed
  70e1a0a

  Copy full SHA for 70e1a0a

• Insert tls13format models

  jschneider-bensch

  committed
  0aa98fb

  Copy full SHA for 0aa98fb

• Insert tls13crypto models

  jschneider-bensch

  committed
  ca9920d

  Copy full SHA for ca9920d

• Insert tls13cert models

  jschneider-bensch

  committed
  2fc12cb

  Copy full SHA for 2fc12cb

• Zeroes should be a constructor

  jschneider-bensch

  committed
  549ebd3

  Copy full SHA for 549ebd3

Commits on Mar 13, 2024

• Replace macro paths by use

  jschneider-bensch

  committed
  02fa23b

  Copy full SHA for 02fa23b

• Repair kem_keygen model

  jschneider-bensch

  committed
  00e2986

  Copy full SHA for 00e2986

Commits on Mar 18, 2024

• check_eq handwritten

  jschneider-bensch

  committed
  3fbab7e

  Copy full SHA for 3fbab7e

• handwritten HandshakeData concat

  jschneider-bensch

  committed
  e43cbe4

  Copy full SHA for e43cbe4

• HandshakeData to_two & to_four rewrite

  jschneider-bensch

  committed
  46b21f7

  Copy full SHA for 46b21f7

• Transcript add handwritten

  jschneider-bensch

  committed
  dae8a65

  Copy full SHA for dae8a65

• Simplify length constants

  jschneider-bensch

  committed
  9e291cc

  Copy full SHA for 9e291cc

• Workaround for memory issues: simplify large integer

  jschneider-bensch

  committed
  d76379d

  Copy full SHA for d76379d

• Simplify length constants

  jschneider-bensch

  committed
  598541c

  Copy full SHA for 598541c

• Concat any HandshakeData

  jschneider-bensch

  committed
  8de6553

  Copy full SHA for 8de6553

Commits on Mar 19, 2024

• Make hkdf_expand_label a constructor

  jschneider-bensch

  committed
  b247a26

  Copy full SHA for b247a26

Commits on Mar 20, 2024

• Remove auto-generated events

  jschneider-bensch

  committed
  c125242

  Copy full SHA for c125242

• Fix HandshakeData__to_four

  jschneider-bensch

  committed
  76013e0

  Copy full SHA for 76013e0

• Fix parse_certificate_verify

  jschneider-bensch

  committed
  de34fd8

  Copy full SHA for de34fd8

• Fix parse_encrypted_extensions

  jschneider-bensch

  committed
  7fd0649

  Copy full SHA for 7fd0649

• Fix parse_server_certificate

  jschneider-bensch

  committed
  97ef62e

  Copy full SHA for 97ef62e

• Remove auto-generated event

  jschneider-bensch

  committed
  455cd07

  Copy full SHA for 455cd07

• More specific reduc for ECDSA signature verification

  jschneider-bensch

  committed
  bb70be6

  Copy full SHA for bb70be6

• Certificate constructor

  jschneider-bensch

  committed
  4352fcf

  Copy full SHA for 4352fcf

• Simple reachability event

  jschneider-bensch

  committed
  8710793

  Copy full SHA for 8710793

• Treat HandshakeData as bytes

  jschneider-bensch

  committed
  83061af

  Copy full SHA for 83061af

• Introduce server name and certificate signing key free names

  jschneider-bensch

  committed
  f7a4fcd

  Copy full SHA for f7a4fcd

• Full handshake reachability analysis

  jschneider-bensch

  committed
  c546f9c

  Copy full SHA for c546f9c

Commits on Mar 23, 2024

• len functions can actually be extracted

  jschneider-bensch

  committed
  cf216c5

  Copy full SHA for cf216c5

• More conservative hkdf_expand_label

  jschneider-bensch

  committed
  561051c

  Copy full SHA for 561051c

• Remove unnecessary newlines

  jschneider-bensch

  committed
  d0fe172

  Copy full SHA for d0fe172

Commits on Mar 25, 2024

• auth/secrecy queries

  karthikbhargavan

  committed
  cbafa66

  Copy full SHA for cbafa66

• Certificate verification crutch

  jschneider-bensch

  committed
  80be87f

  Copy full SHA for 80be87f

• hmac_tag should not be [data]

  jschneider-bensch

  committed
  2a612f4

  Copy full SHA for 2a612f4

• Server key compromise event

  jschneider-bensch

  committed
  018b166

  Copy full SHA for 018b166

• Server key compromise queries

  jschneider-bensch

  committed
  9ddf065

  Copy full SHA for 9ddf065

Commits on Mar 27, 2024

• Allow specification of algs and psk-mode for server/client processes

  jschneider-bensch

  committed
  faad1f9

  Copy full SHA for faad1f9

• Fix put_client_hello

  Show description for a1ec30d
  jschneider-bensch

  committed
  a1ec30d

  Copy full SHA for a1ec30d

• Fix RSA certificate verification

  jschneider-bensch

  committed
  889a4df

  Copy full SHA for 889a4df

• Fix PSK mode

  jschneider-bensch

  committed
  9aadae3

  Copy full SHA for 9aadae3

Commits on Mar 28, 2024

• Separating out PSK and cert_sk compromise scenarios

  jschneider-bensch

  committed
  ad607a3

  Copy full SHA for ad607a3

• Remove dependency on non-main hax branch

  jschneider-bensch

  committed
  99da441

  Copy full SHA for 99da441

Commits on Mar 29, 2024

• Store model patches in separate directory

  Show description for a6de9bd
  jschneider-bensch

  committed
  a6de9bd

  Copy full SHA for a6de9bd

• Make proofs/proverif/extraction track unmodified extraction output

  jschneider-bensch

  committed
  1835378

  Copy full SHA for 1835378

Commits on Apr 2, 2024

• Move hax-lib-macros dependency to a feature

  jschneider-bensch

  committed
  0336128

  Copy full SHA for 0336128

• Merge pull request #102 from cryspen/jonas/hax-pv-feature

  Show description for e87410c
  jschneider-bensch

  authored
  e87410c

  Copy full SHA for e87410c

• Merge branch 'main' into jonas/pv-handshake-annotations

  jschneider-bensch

  authored
  9050ddb

  Copy full SHA for 9050ddb

• Merge branch 'main' into jonas/pv-handshake-annotations

  jschneider-bensch

  authored
  d7e9a5b

  Copy full SHA for d7e9a5b