[SECURITY] Fedora 45 Update: ocaml-bin-prot-0.17.0-14.fc45

This library contains functionality for reading and writing OCaml values in a type-safe binary protocol. These functions are extremely efficient and provide users with a convenient and safe way of performing I/O on any extensionally defined data type. This means that functions, objects, and value...

Understanding the Usability of Cryptographic Verification Tools

Cryptographic protocol verification tools are widely used to analyze the security of complex protocols, yet how users interact with these tools remains comparatively understudied. We present an exploratory human-centered study of experienced users of Tamarin, ProVerif, and related protocol...

CVE-2026-72703

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. finduniformparameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes th...

CVE-2026-72704

CVE-2026-72704 affects the guard checker in Rocq Prover through 9.2.0 . The checker does not re-validate the recursive tree of an inductive type parameter after a transport -induced rewrite. A fixpoint can apply a type-equality rewrite to its recursive argument; the guard checker accepts the resu...

CVE-2026-72704 Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport

The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because...

CVE-2026-72704 Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport

The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because...

CVE-2026-72703 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. finduniformparameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes th...

CVE-2026-72703 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. finduniformparameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes th...

PT-2026-81017

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find uniform parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes...