tamarin-prover / manual

Tamarin prover manual: source files
https://tamarin-prover.github.io/manual
24 stars 39 forks source link

Guardedness explanation in manual is inaccurate #78

Open cascremers opened 3 years ago

cascremers commented 3 years ago

The manual currently explains guardedness only in terms of actions, but omits the case of quantified equations. Notably, these don't need binding to an action, but the quantified variables should only occur on one side of the equation. (Cf. e.g. the definition in Benedikt's thesis)