35 lines
1.6 KiB
Plaintext
35 lines
1.6 KiB
Plaintext
|
Interm constraints
|
||
|
|
------------------
|
||
|
|
|
||
|
|
- Broadly cf. Berezin; I've already proven somewhere a similar procedure
|
||
|
|
terminates, as it is similar to set inclusion constraints.
|
||
|
|
- On unif of st with non-basic variable bt, add constraint
|
||
|
|
(st,bt) to constraint list. Interpretation: st is always a non-tuple,
|
||
|
|
because we don't seek variable goals, and so we have that
|
||
|
|
st in unpair(bt)
|
||
|
|
- Constraints must remain 'solvable'. Once bt becomes a non-tuple, we
|
||
|
|
can unify. If bt becomes a tuple, we can split the constraint into
|
||
|
|
two.
|
||
|
|
- Problem: constraints destroy simple relations between realizable and
|
||
|
|
traces, etc. Trace generation becomes more difficult, and maybe the
|
||
|
|
whole 'classes' concept becomes a bit more vague, as the only clear
|
||
|
|
way out is to
|
||
|
|
- When testing for occurrence of say, terms in out(e) or in(e), we can
|
||
|
|
take the constaints into account. That way we can ensure that the
|
||
|
|
pattern is realizable in the end, if the constraints are met.
|
||
|
|
|
||
|
|
Channels
|
||
|
|
--------
|
||
|
|
|
||
|
|
- Define specific channel types; go in after (a,b,[ChType,] message)
|
||
|
|
- Auth channels: incoming recv on auth channel must come from
|
||
|
|
non-intruder and must match identically. Note: first-binding may be
|
||
|
|
violated by this; and hence 'first occurrence on this type of channel'
|
||
|
|
seems a better constraint.
|
||
|
|
- Conf channels: outgoing send on conf channel may not be bound to
|
||
|
|
incoming node of intruder, but also taking care of avoiding tupling.
|
||
|
|
Hence, send(x,y) may not connect to recv(x), because that would imply
|
||
|
|
the intruder did the projection. These side cases need thorough
|
||
|
|
investigation and sane definitions in the semantics.
|
||
|
|
|