Full State and Session State Invariants

[cwaldm]

This is an update on the current state of "the state changes" for easier commenting. (Previous discussions are here #9)

Main conceptual changes

• introducing three levels for states of participants (single states, sessions, and full state)
• adding functions for setting/getting sessions and full states
• introducing invariants for all these three levels:

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

  Lines 52 to 56 in eb55a1d

  	pred: trace -> principal -> state_id -> state_raw -> prop;
  	// the session argument is the current session on the trace
  	// potentially there is no prior session on the trace for this sid (hence the option)
  	session_pred: trace -> sess:option session_raw -> principal -> state_id -> state_raw -> prop;
  	full_state_pred: trace -> full_state_raw -> principal -> state_id -> state_raw -> prop; // the full_state argument is the current full state on the trace

The key idea for showing the state invariants in the trace invariant is:
If there are no more SetState p _ _ entries , the full state of a principal stays the same:

                        states of p
                     here  and  here  are the same
                       |          |
                       v          v
-----------------------------------
| ... | SetState p _ _ | x | x | x|
-----------------------------------
                       [no more SetState 
                       entries for p here]

(and similarly for a specific session sid of p)
We then show that the operations send_msg, mk_rand and trigger_event don't add any SetState entries.

An Example Protocol

To show how the new state invariants can be used, there is a small example protocol in https://github.com/REPROSEC/dolev-yao-star-extrinsic/tree/cwaldm/experimental/examples/invariants .
In this example, we have a state type that contains two identifiers and a counter:

dolev-yao-star-extrinsic/examples/invariants/DY.Example.Invariants.Uniqueness.fst

Lines 20 to 21 in eb55a1d

	type p_state =
	| S: idn1:nat -> idn2:nat -> ctr: nat -> p_state

with the following invariants:

• within a session the identifiers must stay the same
• within a session the counter must increase
• across sessions the identifiers must be different

Previously, we were not able to express these. But now we can:

dolev-yao-star-extrinsic/examples/invariants/DY.Example.Invariants.Uniqueness.fst

Lines 196 to 231 in eb55a1d

	let p_state_pred: state_predicate_forall_sessions p_cinvs = {
	pred = (fun tr p sid cont -> is_knowable_by #p_cinvs (principal_state_label p sid) tr cont)
	; session_pred = (fun tr sess prin sid cont ->
	// within a session the idns should stay the same
	// and the counter must increase
	match parse p_state cont with
	| None -> False
	| Some (S the_idn1 the_idn2 the_ctr) -> (
	match sess with
	| None -> True
	| Some (Snoc init last) -> (
	match parse p_state last with
	| None -> False //True
	| Some last ->
	last.idn1 = the_idn1
	/\ last.idn2 = the_idn2
	/\ last.ctr < the_ctr
	)
	)
	)
	; full_state_pred = (fun tr sid_i sess_i p sid cont ->
	// across sessions the idns must be different
	match parse p_state cont with
	| None -> False
	| Some (S the_idn1 the_idn2 _) -> begin
	// using the new full_state_pred
	// we can make use of the fact that
	// sess_i is a Snoc
	// and we only talk about sid_i <> sid
	let Snoc _ last_i = sess_i in
	match parse p_state last_i with
	| None -> False
	| Some last_i ->
	last_i.idn1 <> the_idn1
	/\ last_i.idn2 <> the_idn2
	end

The protocol consists of two steps:

• an initialization step where a new state is set with counter 0 and new identifiers
• and a step where a previous state is read and the counter is increased by one. also a message is sent and other trace manipulations are performed

For each of the two steps, we show that the trace invariant (i.e., the global state predicate) is maintained ( init and next)

Further, we show that the identifiers are indeed identifiers, that is, if there are two state entries on the trace that have the same identifier, both of them must belong to the same session (see here)

What do we need this for?

Consider the following situation:
A participant "A" generates two fresh identifiers "id1" and "id2", stores them in a state and sends them to a participant "B", who stores both in his own state (where "id2" is again an identifier for states of "B").
At some later point "A" looks up his latest state that has "id1". Associated with this is a second identifier "id2_A". (Since the "id1" field is an identifier for states of A, we know that "id2_A" must be "id2" generated together with "id1".)
Suppose that at some point "B" uses the identifier "id2" to look up his latest state. Then again this state has an associated "id1_B".
We would now like to show that "id1_B" must be "id1", so that both "A" and "B" looked up a state that corresponds to "the same session" (identified by the pair ("id1", "id2")).

Next Steps

Right now, this is a first try and still very inconvenient for users and probably missing some properties that we need for actual use cases.

Some of the next steps are (not necessarily in order):

• adapt the split predicate method to the new state invariants (so that we can use the Typed state layer and get rid of all the parses in the invariants)
• add a simplified interface for cases where a user only wants to give an invariant for single states (as previously) -- this should probably be done after the adaption of the split predicate method
• find the right SMT patterns for the new lemmas
• show the motivating property (from "What do we need this for?") in a small example
• some cleanup things

[TWal]

Thanks, I look forward having a look at the code!

For now, I am trying to understand what is the end goal, but I'm not understanding the section "What do we need this for?". E.g. I don't understand in the first sentence whether id2 is generated by A (« A participant "A" generates two fresh identifiers "id1" and "id2" ») or B (« (where "id2" is again an identifier for states of "B") »)

Could you explain that in more details, and in particular how it would help proving new kind of security properties, or prove hidden assumptions?
Thanks!

[qaphla]

Thanks, I look forward having a look at the code!

For now, I am trying to understand what is the end goal, but I'm not understanding the section "What do we need this for?". E.g. I don't understand in the first sentence whether id2 is generated by A (« A participant "A" generates two fresh identifiers "id1" and "id2" ») or B (« (where "id2" is again an identifier for states of "B") »)

Could you explain that in more details, and in particular how it would help proving new kind of security properties, or prove hidden assumptions? Thanks!

In the example, A generates both id1 and id2 (in our more concrete motivation, A is an AS, generating session identifiers id1 and id2 for different portions of a session in a protocol with more than 2 parties), stores them together, and then sends both to B, who should also store these two IDs together.

The property that we want to ensure in this simple example is that A and B together have a coherent view of the "session data", in that they both agree that id1 and id2 are associated with one another as part of the same protocol session, rather than, for instance, A thinking that the session is defined by the pair id1, id2, while B thinks it is defined by the pair id1, id3 for some id3 <> id2.

In a two-party protocol, there may be some workarounds for this (we haven't examined it too closely), but this initially arose when trying to ensure that 3+ (honest) parties all share a coherent idea of what one session of the given protocol is, so that we can reasonably work with statements of the form "A knows that the data that C associates with session X of the protocol has property Y".

There were two problems that arose, both centering on how a participant identifies a session --- in many of the protocols we have looked at, there is some form of "session ID" (or possibly a few different session IDs shared between different subsets of the participants), and when a message is received, it will contain one of these session IDs, which can then be used to look up the corresponding state to work with. However, we have no guarantee that there is a unique such state --- our invariants are not expressive enough to state that a given session ID is used in at most one state at a given participant, and so it is difficult to guarantee that we actually have all of the needed information for that session stored coherently and in a way that avoids spurious mix-ups (between sessions sharing IDs, for instance, which we generally disregard in modelling, as long as the session IDs are generated centrally). The other problem is that we have no way to enforce that this session ID stays fixed for the lifetime of the session --- changing session IDs can again lead to mix-ups even if at any given time no two sessions share an ID, because they may have the same ID at different times, and again, these mix-ups are the sort of thing that we generally want to exclude in modelling unless the protocol explicitly allows for updating session IDs.

I'll also think further on a concrete simple example of a property that this enables proving, but the general class of properties that we want are about this ability to coherently and unambiguously reason about a session between honest parties, even if they are not all in direct communication with one another.

The specific tools that we seem to need for this are

1. uniqueness of a given value (e.g., session identifier) across all sessions of a participant and
2. immutability of a given value in a session
   although we incidentally also seem to be able to express some other temporal properties of a session (like the given example of a counter in the state being increasing).