---

Step * of Lemma cabal-theorem

∀s:SecurityTheory. ∀es:EO+(Info). ∀C:Id List.
  ∀ns:Atom1 List. (C is a cabal for ns ⇒ Only agents in C have atoms in ns) supposing (∀A∈C.Honest(A))
BY
{ (Auto
   THEN D 1
   THEN D 2
   THEN All
   (RepUR ``sth-es``)⋅
   THEN UnfoldTopAb (-1)
   THEN UnfoldTopAb 0
   THEN (Assert PropertyF BY
               Auto)
   THEN CausalInd'
   THEN Auto
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN D -1
   THEN Auto
   THEN RenameVar `s' 1) }

1
1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
                  ((loc(e) = i ∈ Id)
                  ∧ (((↑e ∈b New) ∧ (a = New(e) ∈ Atom1))
                    ∨ ((↑e ∈b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))
      ∧ (∀e:E(Send). ((loc(e) ∈ C) ⇒ (¬(e has a))))
      ∧ (∀e:E(Encrypt)
           ((loc(e) ∈ C)
           ⇒ (e has a)
           ⇒ ((∃A∈C. key(e) = PublicKey(A) ∈ Key)
              ∨ (∃k∈ns. key(e) = symmetric-key(k) ∈ Key)
              ∨ (cipherText(e) ∈ ns)))))@i
9. PropertyF
10. e : E@i
11. ∀e1:E. ((e1 < e) ⇒ (∃a∈ns. (e1 has a)) ⇒ (loc(e1) ∈ C))
12. a : Atom1
13. (a ∈ ns)
14. (e has a)
⊢ (loc(e) ∈ C)

---

Latex:

---

Latex:
\mforall{}s:SecurityTheory.  \mforall{}es:EO+(Info).  \mforall{}C:Id  List.
    \mforall{}ns:Atom1  List.  (C  is  a  cabal  for  ns  {}\mRightarrow{}  Only  agents  in  C  have  atoms  in  ns) 
    supposing  (\mforall{}A\mmember{}C.Honest(A))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  D  2
  THEN  All
  (RepUR  ``sth-es``)\mcdot{}
  THEN  UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  0
  THEN  (Assert  PropertyF  BY
                          Auto)
  THEN  CausalInd'
  THEN  Auto
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  RenameVar  `s'  1)

---

Home Index