Clarify the state model of DY*

[qaphla]

Based on some discussions with @cwaldm and @TWal (but anyone else with thoughts is more than welcome to add them).

Currently there are two main ways that we can interpret the state in DY* (maybe more --- if there's another model that I haven't included here, please mention it), centering on what the state_id stored on the trace means.

dolev-yao-star-extrinsic/src/core/DY.Core.Trace.Type.fst

Lines 52 to 53 in 652bf22

	// A principal stored some state.
	| SetState: prin:principal -> sess_id:state_id -> content:bytes -> trace_event_ label_t

Suppose we have a trace with two SetState entries fror the same id:
SetState Alice id contents1 and SetState Alice id contents2, on the trace in that order.

When Alice calls get_state with id, she will get contents2, and has no way to get to contents1 via the Trace API (other than via get_trace, which maybe we should also find a way to prevent the use of). This suggests that writing a new SetState entry to the trace "overwrites" any existing state with the same state ID, which seems to be the current model. This allows for participants to "forget" information, which is in principle useful, although with the current corruption model, it's not clear that this actually changes anything for the attacker, who is able to corrupt arbitrary trace entries.

However, we could also envision an "addition" model, where Alice retains access to both contents1 and contents2, perhaps via another argument to get_state. Broadly, the advantage of this model is that, for a long-running protocol where after each step we want to write some small state, we can "link" them all together via having the same state ID, and so once we have found the state ID for one of these states, it is easy to get to the rest of the information associated with that protocol flow. In the "overwrite" model, the most obvious alternative is to have a single large state object, where we gradually fill in more information after each step, which can result in some large state invariants.

I don't expect that we will necessarily change the model, but I think that we should at least have on record here whatever thoughts/discussion there is of how we handle state, and this can also lend itself to better documentation as that gets written up, and maybe some useful ideas will arise on how to address the drawbacks of whichever approach we take.

[TWal]

The fact that the attacker can corrupt any state at any time is useful to model properties such as "at time t1 the attacker corrupts some state, and stay passive until time t2". In DY* we model this as a corruption event at time t2 that corrupts the state at time t1. This can be used to model "post-compromise security"-style properties.

The "addition" model seems to be useful in some cases, but couldn't we have the best of both worlds by designing an "additive state" in DY.Lib that relies on the "overwrite" model? We cannot do it the other way hence I think DY.Core should stay in the "overwrite" model. The "overwrite" model also correspond more closely to the reality of computer programs, that can only access the latest value they stored, so I think it should be kept.

[qaphla]

Indeed, I think the attacker should be able to do this kind of arbitrary corruption, though I also think it should be possible with either model.

An "additive state" library should be very doable, either as-is or using some kind of core constraint on how states can be updated (as in #58 , conceptually, but in a simpler form?), depending on what guarantees we want to get for the additive state.