search

REPROSEC / dolev-yao-star-extrinsic

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

Decide between "state" and "session" #6

Open TWal opened 2 months ago

TWal commented 2 months ago

The code is currently using both names, we should decide between one of them and stick to it.

I think I prefer "state".

fabian-hk commented 2 months ago

Can't a state store multiple sessions inside of it? So, I would also think that state makes more sense.

cwaldm commented 2 months ago

I think that depends on what we are referring to.

We previously proposed the following structure and terms:

The idea being, that we keep the history of a session represented by the versions in the session_state. (That's on a conceptual level and independent of how we represent that on the trace (e.g., whether we store the full states or just the diffs).)

That means, on the lowest level we would have versions, which I think correspond to what we currently call session/state, e.g., https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/23023afadde09e8bd4b5833bd32843617e6ea3bc/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst#L17-L21

TWal commented 2 months ago

Ah, I think I now see the difference: in general, principals store "states", which can be of different purpose, for example one state for the local PKI, or one state for storing long-term private keys. In most protocols, one of these states will be of type "session", representing the state machine for one of (maybe several) protocol executions.

Then the full state of a participant is a grid as @cwaldm is saying, one axis being state id and the other is state version.

What do you think about it?