From 4e78a1d3fa82f7f479a0c80f5eb84ea4f77a2e50 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Sat, 5 Oct 2013 23:47:51 +0100 Subject: [PATCH] Removing obsolete file. --- src/NOTES.txt | 34 ---------------------------------- 1 file changed, 34 deletions(-) delete mode 100644 src/NOTES.txt diff --git a/src/NOTES.txt b/src/NOTES.txt deleted file mode 100644 index d1b11fc..0000000 --- a/src/NOTES.txt +++ /dev/null @@ -1,34 +0,0 @@ -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. -