law sign_verify_bytes_if

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

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/sign.bend as Sg

281# Signatures and key agreement (sign.bend, kex.bend): the generic helpers
282# keep the interface laws (README.md); the instances (RSA, DH, ECDSA, ECDH,
283# SM2, EC-RDSA) and their laws are in bend-osdev-pubkey. A signature
284# checked from the public key's bytes is accepted, for every scheme, secret
285# key and message, when the scheme's pk_format and accepts laws hold there
286# (hf, ha)
287law sign_verify_bytes_if:
288  for ~SK: Data
289  for ~PK: Data
290  for ~public: SK -> PK
291  for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
292  for ~pk_to: PK -> B.Octets
293  for ~sign: SK -> B.Octets -> B.Octets
294  for ~verify: PK -> B.Octets -> B.Octets -> Bool
295  for +sk: SK
296  for +m: B.Octets
297  for hf: {pk_of(pk_to(public(sk))) == Done{public(sk)} : Result<&2, &2, Cr.CrError, PK>}
298  for ha: {verify(public(sk), m, sign(sk, m)) == True{} : Bool}
299  {Sg.CrSign.verify_bytes(~PK, ~pk_of, ~verify, pk_to(public(sk)), m, sign(sk, m)) == True{} : Bool}