Issues

• [Communication Layer] Remove dependence on default crypto usages

  REPROSEC/dolev-yao-star-extrinsic#121 · Filter by author qaphla opened on Nov 19, 2025

• Fix verify_message not being opaque

  REPROSEC/dolev-yao-star-extrinsic#119 · Filter by author qaphla opened on Sep 15, 2025

• Replace communication layer metadata with a hidden state

  REPROSEC/dolev-yao-star-extrinsic#106 · Filter by author qaphla opened on Apr 1, 2025
  2

• Can we strengthen the traceful / traceful+option bind?

  enhancement
  REPROSEC/dolev-yao-star-extrinsic#90 · Filter by author cwaldm opened on Nov 21, 2024
  1

• Make some of the API really opaque

  cleanup
  REPROSEC/dolev-yao-star-extrinsic#71 · Filter by author TWal opened on Sep 30, 2024

• Clarify the state model of DY*

  documentation
  REPROSEC/dolev-yao-star-extrinsic#70 · Filter by author qaphla opened on Sep 30, 2024
  2

• Document and regroup flags that enable SMT patterns

  cleanup
  REPROSEC/dolev-yao-star-extrinsic#64 · Filter by author TWal opened on Sep 23, 2024

• Simplify code using latest F* features

  cleanup
  REPROSEC/dolev-yao-star-extrinsic#63 · Filter by author TWal opened on Sep 18, 2024
  2

• Invariants on kdf_extract are too strict

  bug
  REPROSEC/dolev-yao-star-extrinsic#62 · Filter by author TWal opened on Sep 18, 2024

• Dynamic Labelling

  enhancement
  REPROSEC/dolev-yao-star-extrinsic#23 · Filter by author qaphla opened on May 7, 2024
  6

• Do a holistic renaming of the various predicates

  cleanup
  REPROSEC/dolev-yao-star-extrinsic#22 · Filter by author TWal opened on May 7, 2024
  5

• Monotonic states and states with unique values

  enhancement
  REPROSEC/dolev-yao-star-extrinsic#9 · Filter by author TWal opened on Apr 25, 2024
  13

• Decide between "state" and "session"

  cleanup
  REPROSEC/dolev-yao-star-extrinsic#6 · Filter by author TWal opened on Apr 23, 2024
  3