law kex_agree_if

bend-osdev-crypto@0.1.0.0 · LAWS.bend:301

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-crypto@0.1.0.0/kex.bend as Kx

301# two parties agree from each other's public-key bytes, for every scheme and
302# pair of secret keys, when the keys parse (hx, hy), the public keys survive
303# their bytes (hfx, hfy) and the scheme's agree law holds for them (h)
304law kex_agree_if:
305  for ~SK: Data
306  for ~PK: Data
307  for ~secret: B.Octets -> Result<&2, &2, Cr.CrError, SK>
308  for ~public: SK -> PK
309  for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
310  for ~pk_to: PK -> B.Octets
311  for ~shared: SK -> PK -> Result<&2, &2, Cr.CrError, B.Octets>
312  for +a: B.Octets
313  for +b: B.Octets
314  for +x: SK
315  for +y: SK
316  for hx: {secret(a) == Done{x} : Result<&2, &2, Cr.CrError, SK>}
317  for hy: {secret(b) == Done{y} : Result<&2, &2, Cr.CrError, SK>}
318  for hfx: {pk_of(pk_to(public(x))) == Done{public(x)} : Result<&2, &2, Cr.CrError, PK>}
319  for hfy: {pk_of(pk_to(public(y))) == Done{public(y)} : Result<&2, &2, Cr.CrError, PK>}
320  for h: {shared(x, public(y)) == shared(y, public(x)) : Result<&2, &2, Cr.CrError, B.Octets>}
321  {Kx.CrKex.agree(~SK, ~PK, ~secret, ~pk_of, ~shared, a, pk_to(public(y))) == Kx.CrKex.agree(~SK, ~PK, ~secret, ~pk_of, ~shared, b, pk_to(public(x))) : Result<&2, &2, Cr.CrError, B.Octets>}