{ 
s:SES. (SecurityAxioms 
{ses-ordering'(s) 
PropertyNR PropertyNU}) }
{ Proof }
Definitions occuring in Statement :
ses-axioms: SecurityAxioms,
ses-NR: PropertyNR,
ses-NU: PropertyNU,
ses-ordering': ses-ordering'(s),
security-event-structure: SES,
guard: {T},
all: x:A. B[x],
implies: P Q,
and: P Q
Definitions :
equal: s = t,
member: t 
T,
function: x:A 
B[x],
all: x:A. B[x],
guard: {T},
subtype_rel: A 
r B,
strong-subtype: strong-subtype(A;B),
rev_implies: P 
Q,
iff: P Q,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
pi1: fst(t),
ifthenelse: if b then t else f fi ,
assert: 
b,
ses-key-rel: MatchingKeys(k1;k2),
sym: Sym(T;x,y.E[x; y]),
ses-K: PropertyK,
ses-S: PropertyS,
product: x:A 
B[x],
exists: 
x:A. B[x],
ses-D: PropertyD,
ses-R: PropertyR,
ses-V: PropertyV,
apply: f a,
ycomb: Y,
ses-flow: ses-flow(s;es;a;e1;e2),
ses-flow-axiom: PropertyF,
void: Void,
false: False,
not: 
A,
ses-nonce-disjoint: NoncesCiphersAndKeysDisjoint,
ses-disjoint: ActionsDisjoint,
security-event-structure: SES,
universe: Type,
prop: 
,
ses-ordering': ses-ordering'(s),
ses-NR: PropertyNR,
ses-NU: PropertyNU,
and: P Q,
ses-axioms: SecurityAxioms,
implies: P Q,
ses-ordering: PropertyO,
union: left + right,
or: P 
Q,
record-select: r.x,
infix_ap: x f y,
es-causl: (e < e'),
Auto: Error :Auto,
D: Error :D,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic
Lemmas :
ses-flow-axiom-ordering,
ses-ordering-implies,
ses-ordering-ordering',
ses-axioms_wf,
security-event-structure_wf,
ses-NU_wf,
ses-NR_wf,
ses-ordering'_wf,
guard_wf
\mforall{}s:SES. (SecurityAxioms {}\mRightarrow{} \{ses-ordering'(s) \mwedge{} PropertyNR \mwedge{} PropertyNU\})
Date html generated:
2011_08_17-PM-07_30_37
Last ObjectModification:
2010_09_24-PM-02_45_29
Home
Index