Nuprl Definition : oar-crypto
The sign and verify classes S and V satisfy the assumptions that
for every V-event there was a previous matching S-event.
And the location of a correct S-event is correct.⋅
oar-crypto(es;M;V;S;correct) ==
(∀n:ℕ. ∀sndr:Id. ∀msg:M. ∀x:Id. ∀sig:Atom1. ∀e:E.
(<x, sig, sndr, n, msg> ∈ V(e) ⇒ (↓∃e':E. ((e' < e) ∧ <x, sig, sndr, n, msg> ∈ S(e')))))
∧ (∀n:ℕ. ∀sndr:Id. ∀msg:M. ∀x:Id. ∀sig:Atom1. ∀e:E.
(<x, sig, sndr, n, msg> ∈ S(e) ⇒ (correct x) ⇒ (loc(e) = x ∈ Id)))
Definitions occuring in Statement :
classrel: v ∈ X(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
nat: ℕ,
atom: Atom$n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
pair: <a, b>,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
oar-crypto
Latex:
oar-crypto(es;M;V;S;correct) ==
(\mforall{}n:\mBbbN{}. \mforall{}sndr:Id. \mforall{}msg:M. \mforall{}x:Id. \mforall{}sig:Atom1. \mforall{}e:E.
(<x, sig, sndr, n, msg> \mmember{} V(e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <x, sig, sndr, n, msg> \mmember{} S(e')))))
\mwedge{} (\mforall{}n:\mBbbN{}. \mforall{}sndr:Id. \mforall{}msg:M. \mforall{}x:Id. \mforall{}sig:Atom1. \mforall{}e:E.
(<x, sig, sndr, n, msg> \mmember{} S(e) {}\mRightarrow{} (correct x) {}\mRightarrow{} (loc(e) = x)))
Date html generated:
2015_07_23-PM-00_27_00
Last ObjectModification:
2014_07_07-PM-02_08_49
Home
Index