Nuprl Lemma : CR-protocol-fresh
∀s:SES
(ActionsDisjoint
⇒ FreshSignatures([CR-initiator1{i:l}(s);
CR-initiator2{i:l}(s);
CR-initiator3;
CR-responder1{i:l}(s);
CR-responder2{i:l}(s);
CR-responder3]))
Proof
Definitions occuring in Statement :
CR-responder3: CR-responder3,
CR-responder2: CR-responder2{i:l}(s),
CR-responder1: CR-responder1{i:l}(s),
CR-initiator3: CR-initiator3,
CR-initiator2: CR-initiator2{i:l}(s),
CR-initiator1: CR-initiator1{i:l}(s),
fresh-sig-protocol1: FreshSignatures(bss),
ses-disjoint: ActionsDisjoint,
security-event-structure: SES,
cons: [a / b],
nil: [],
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
fresh-sig-protocol1: FreshSignatures(bss),
exists: ∃x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
exposed-bfalse: exposed-bfalse,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A,
prop: ℙ,
bfalse: ff,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
ses-protocol1-thread: (thr is one of bss at A),
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
so_apply: x[s],
iff: P ⇐⇒ Q,
CR-initiator1: CR-initiator1{i:l}(s),
basic-seq-1-1: A ⟶ B: pas[A; B; m],
is-basic-seq: thr[A;B] |= bs,
ses-is-fresh: ses-is-fresh(f;A;pas),
isl: isl(x),
decidable-ses-fresh-sequence,
decidable__all_int_seg,
decidable__exists_int_seg,
length: ||as||,
list_ind: list_ind,
cons: [a / b],
nil: [],
int_seg_decide: int_seg_decide(d;i;j),
decidable__not,
decidable__implies,
decidable__pa-is-sign-implies,
select: L[n],
mk-pa: n(v),
decidable__atom_equal,
decidable__false,
subtract: n - m,
true: True,
CR-initiator2: CR-initiator2{i:l}(s),
basic-seq-1-3: A ⟶ B: pas[A; B; m; n; x],
append: as @ bs,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
CR-initiator3: CR-initiator3,
basic-seq-1-5: A ⟶ B: pas[A;B;m;n;x;y;z],
CR-responder1: CR-responder1{i:l}(s),
CR-responder2: CR-responder2{i:l}(s),
basic-seq-1-4: A ⟶ B: pas[A;B;m;n;x;y],
CR-responder3: CR-responder3,
decidable__implies_better,
decidable__cand,
decidable__equal_Id,
experimental: experimental{allFunctionality}(possibleextract),
decidable_functionality,
iff_preserves_decidability,
decidable__assert,
eq_id: a = b,
id-deq: IdDeq,
atom2-deq: Atom2Deq,
eq_atom: eq_atom$n(x;y),
pi1: fst(t),
pi2: snd(t),
Id: Id,
decidable__pa-is-new-and,
lt_int: i <z j,
sdata-atoms: sdata-atoms(d),
tree_ind: tree_ind,
sdata-pair: <d1, d2>,
tree_node: tree_node(left;right),
atom-sdata: data(a),
tree_leaf: tree_leaf(value),
id-sdata: data(x),
decidable__atom_equal_1,
outl: outl(x),
outr: outr(x)
Latex:
\mforall{}s:SES
(ActionsDisjoint
{}\mRightarrow{} FreshSignatures([CR-initiator1\{i:l\}(s);
CR-initiator2\{i:l\}(s);
CR-initiator3;
CR-responder1\{i:l\}(s);
CR-responder2\{i:l\}(s);
CR-responder3]))
Date html generated:
2016_05_17-PM-00_48_48
Last ObjectModification:
2015_12_29-PM-06_35_36
Theory : event-logic-applications
Home
Index