Secure Messaging

5.2. FS-AEAD from AEAD and PRG🔗

Definition5.2.1
Group: FS-AEAD from AEAD and PRG. (2)
Group member previews
Preview
Theorem 5.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N

\todo

LeanLean anchor pending

uses Definition 5.1.1 · Definition 2.1.1 · Definition 7.1.1 · github #31

Theorem5.2.2
Group: FS-AEAD from AEAD and PRG. (2)
Group member previews
Preview
Definition 5.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N

\todo

LeanLean anchor pending

uses Definition 5.2.1 · Definition 5.1.1 · Definition 2.1.3 · Definition 7.1.1 · github #29

Theorem5.2.3
Group: FS-AEAD from AEAD and PRG. (2)
Group member previews
Preview
Definition 5.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Definition 2.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N

\todo

LeanLean anchor pending

uses Definition 5.2.1 · Definition 5.1.1 · Definition 5.1.2 · Definition 2.1.4 · Definition 7.1.2 · github #32

References: