search

REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs
https://reprosec.org/
Mozilla Public License 2.0
10 stars 0 forks source link

Split the `_invariant` lemmas in two parts (with and without `trace_invariant` requirement) #80

Open cwaldm opened 2 days ago

cwaldm commented 2 days ago

I think, we should revisit the _invariant lemmas ( fore example in https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/main/src/core/DY.Core.Trace.Manipulation.fst ) and pull out things, that do not need the trace invariant. For example, for trace entries: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/47c7c65f0cef3ab2622029f4105e10991bf78ba6/src/core/DY.Core.Trace.Manipulation.fst#L121-L133 the part event_exists ... is true even without the trace invariant. Similarly, for state_was_set ... in set_state_invariant and so on. Sometimes it is useful to get state_was_set, or that the trace stays the same when receiving a message without knowing that the trace invariant holds. Also, I think it is a bit easier to understand what we need the invariant for, if we only require it where we really need it.

My suggestion: have two version of each _invariant lemma: one with all properties that require the trace invariant, and another one with properties that are true even without the invariant.

TWal commented 2 days ago

That makes sense!