Download on the CryptoVerif page
Changes since the last release:
- Ghost types; computations of ghost types and useless events and tables are removed when generating F* or OCaml implementations.
- cv2fstar:
- add an invariant preserved by all oracle functions, to be defined and proved by the user (by default, always True)
- axiomatize that the adversary may call oracle functions concurrently (can be disabled by setting fstarConcurrent = false)
- setting fstarDebug to allow printing the internal state of the game
- modified deserialization to allow dealing with a stream in which messages are not separated
- better lemmas for equality functions
- Allow: move array “no collisions”.
- Allow using {_} as regular expression for occurrence numbers.
- Replace channels with oracles in the internal representation of games, by Charlie Jacomme. That may change occurrence numbers in proofs.
- Fixed bug: make sure the arity of oracles is preserved by all game transformations.
- Fixed bug: prevent inserting events inside variable terms, which could cause an internal error.
- Fixed infinite loop when applying KEMs, by using different function symbol in the right-hand the equiv statements.
