Morpheus

This is a research project for non-compliance checking of PKCS#1-v1.5 signature verification implementations. The corresponding paper has been submitted to CCS'21 and is under review.

Content structure:

• oracle: This folder contains formally verified implementation of PKCS#1-v1.5 signature verification in Coq language.