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
GitHub#31

\todo

LeanLean anchor pending
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
GitHub#29

\todo

LeanLean anchor pending
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
GitHub#32

\todo

LeanLean anchor pending

References: