{ 
s:SES. es:EO+(Info). e1,e2:E. a:Atom1.
(ses-flow(s;es;a;e1;e2)
((e1 
loc e2 
(e2 has a))
(
snd:E(Send). (e1 loc snd (snd < e2) snd has* a)))) }
{ Proof }
Definitions occuring in Statement :
event-has*: e has* a,
ses-flow: ses-flow(s;es;a;e1;e2),
event-has: (e has a),
ses-send: Send,
ses-info: Info,
security-event-structure: SES,
es-E-interface: E(X),
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-causl: (e < e'),
es-E: E,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
or: P Q,
and: P Q,
atom: Atom$n
Definitions :
member: t 
T,
security-event-structure: SES,
equal: s = t,
dep-isect: Error :dep-isect,
event_ordering: EO,
ses-info: Info,
es-E: E,
function: x:A 
B[x],
universe: Type,
top: Top,
token: "$token",
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
atom: Atom,
subtype_rel: A 
r B,
all: x:A. B[x],
eq_atom: eq_atom$n(x;y),
record-select: r.x,
record+: record+,
event-ordering+: EO+(Info),
product: x:A 
B[x],
apply: f a,
atom: Atom$n,
encryption-key: Key,
sdata: SecurityData,
void: Void,
isect: 
x:A. B[x],
ses-encrypt: Encrypt,
implies: P Q,
eclass: EClass(A[eo; e]),
es-E-interface: E(X),
so_lambda: 
x y.t[x; y],
set: {x:A| B[x]} ,
assert: 
b,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ses-decrypt: Decrypt,
es-locl: (e <loc e'),
es-causle: e c e',
es-causl: (e < e'),
and: P Q,
not: 
A,
union: left + right,
or: P Q,
es-le: e loc e' ,
event-has*: e has* a,
prop: 
,
ses-key-rel: MatchingKeys(k1;k2),
ses-encrypted: plainText(e),
ses-decrypted: plainText(e),
ses-crypt: cipherText(e),
ses-cipher: cipherText(e),
cand: A c B,
false: False,
pi1: fst(t),
infix_ap: x f y,
rec: rec(x.A[x]),
tree: Tree(E),
ses-send: Send,
exists: x:A. B[x],
event-has: (e has a),
symmetric-key: symmetric-key(a),
ses-decryption-key: key(e),
limited-type: LimitedType,
ses-encryption-key: key(e),
decidable: Dec(P),
iff: P 
Q,
less_than: a < b,
le: A B,
int_seg: {i..j
},
divides: b | a,
assoced: a ~ b,
set_leq: Error :set_leq,
set_lt: Error :set_lt,
grp_lt: Error :grp_lt,
l_all: (xL.P[x]),
l_exists: (xL. P[x]),
l_member: (x l),
l_contains: A B,
inject: Inj(A;B;f),
reducible: reducible(a),
prime: prime(a),
squash: 
T,
l_disjoint: l_disjoint(T;l1;l2),
nat: 
,
fun-connected: y is f*(x),
qle: r s,
qless: r < s,
q-rel: q-rel(r;x),
list: type List,
p-outcome: Outcome,
fset-member: a s,
f-subset: xs ys,
fset-closed: (s closed under fs),
cs-not-completed: in state s, a has not completed inning i,
cs-archived: by state s, a archived v in inning i,
cs-passed: by state s, a passed inning i without archiving a value,
cs-inning-committed: in state s, inning i has committed v,
cs-inning-committable: in state s, inning i could commit v ,
cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i,
cs-precondition: state s may consider v in inning i,
existse-before: e<e'.P[e],
existse-le: ee'.P[e],
alle-lt: e<e'.P[e],
alle-le: ee'.P[e],
alle-between1: e[e1,e2).P[e],
existse-between1: e[e1,e2).P[e],
alle-between2: e[e1,e2].P[e],
existse-between2: e[e1,e2].P[e],
existse-between3: e(e1,e2].P[e],
es-fset-loc: i locs(s),
unit: Unit,
collect-event: collect-event(es;X;n;v.num[v];L.P[L];e),
cut-order: a (X;f) b,
path-goes-thru: x-f*-y thru i,
es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),
same-thread: same-thread(es;p;e;e'),
ses-action: Action(e),
rel_star: R^*,
class-value-has: X(e) has a,
bool: 
,
strong-subtype: strong-subtype(A;B),
IdLnk: IdLnk,
Knd: Knd,
Id: Id,
so_apply: x[s],
guard: {T},
fpf: a:A fp-> B[a],
ses-rcv: Rcv,
eclass-val: X(e),
sq_type: SQType(T),
in-eclass: e 
X,
true: True,
isl: isl(x),
can-apply: can-apply(f;x),
subtype: S T,
lambda: x.A[x],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
ses-flow: ses-flow(s;es;a;e1;e2),
pair: <a, b>,
ses-info-flow: ->>,
es-p-le: e p e',
causal-predecessor: causal-predecessor(es;p),
es-p-locl: e p< e',
es-loc: loc(e),
lsrc: source(l),
ldst: destination(l),
es-interface-val: val(X,e),
es-pred: pred(e),
alle-between3: e(e1,e2].P[e],
btrue: tt,
rev_implies: P Q
Lemmas :
event-has*-iff,
event-has*-transitive-encrypt,
es-causl_weakening,
es-le_transitivity,
es-causle_transitivity,
es-causl_transitivity1,
es-causle-le,
sdata_sq,
es-le-loc,
es-loc-pred,
false_wf,
Id_wf,
es-loc_wf,
es-causle_weakening,
es-causle_weakening_locl,
es-causl_transitivity2,
rel_star_weakening,
rel_star_wf,
ses-info-flow_wf,
security-event-structure_wf,
ses-flow_wf,
ses-flow-implies,
eclass-val_wf,
event-ordering+_inc,
event-ordering+_wf,
assert_wf,
bool_sq,
assert_elim,
in-eclass_wf,
ses-rcv_wf,
decidable__cand,
decidable__es-le,
es-locl_wf,
es-causle_wf,
ses-decrypted_wf,
ses-encrypted_wf,
ses-cipher_wf,
ses-key-rel_wf,
ses-encryption-key_wf,
not_wf,
ses-decryption-key_wf,
symmetric-key_wf,
ses-crypt_wf,
event-has_wf,
ses-send_wf,
es-le_wf,
es-causl_wf,
event-has*_wf,
ses-decrypt_wf,
es-E-interface_wf,
eclass_wf,
member_wf,
es-interface-top,
es-interface-subtype_rel,
ses-encrypt_wf,
subtype_rel_wf,
sdata_wf,
encryption-key_wf,
top_wf,
ses-info_wf,
es-E_wf,
subtype_rel_self
\mforall{}s:SES. \mforall{}es:EO+(Info). \mforall{}e1,e2:E. \mforall{}a:Atom1.
(ses-flow(s;es;a;e1;e2)
{}\mRightarrow{} ((e1 \mleq{}loc e2 \mwedge{} (e2 has a)) \mvee{} (\mexists{}snd:E(Send). (e1 \mleq{}loc snd \mwedge{} (snd < e2) \mwedge{} snd has* a))))
Date html generated:
2010_08_28-AM-02_08_34
Last ObjectModification:
2010_03_11-PM-12_17_15
Home
Index