Verify IND-CCA unpacked functions - Githubissues

cryspen / libcrux

The formally verified crypto library for Rust

https://cryspen.com/libcrux

Apache License 2.0

88 stars 14 forks source link

Verify IND-CCA unpacked functions #641

Open mamonet opened 2 weeks ago

mamonet commented 2 weeks ago

This issue implies the following changes

Write spec functions for ind-cca unpacked functions
Create pre/post-conditions for the functions
Prove these conditions and have the functions verified

mamonet commented 1 day ago

Addressed in https://github.com/cryspen/libcrux/pull/652