From 27521d0e8709feebf2e7f88b653e0cb1290768f0 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 13 Mar 2008 10:24:13 +0100 Subject: [PATCH] Added notes. --- src/NOTES.txt | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/NOTES.txt diff --git a/src/NOTES.txt b/src/NOTES.txt new file mode 100644 index 0000000..d1b11fc --- /dev/null +++ b/src/NOTES.txt @@ -0,0 +1,34 @@ +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. +