Common verification procedures for digital signatures return a
decision (accept/reject) only at the very end of the execution. If
interrupted prematurely, however, the verification process cannot
infer any meaningful information about the validity of the given
signature. This limitation is due to the algorithm design solely,
and it is not inherit to signature verification. In this talk, I
will present a formal framework to handle interruptions during
signature verification and a generic way to devise alternative
verification procedures that progressively build confidence on the
final decision. Our transformation applies to a wide range of
post-quantum secure schemes including the NIST finalist Rainbow.
High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of …