Cryptis: Cryptographic Reasoning in Separation Logic

Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi

We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of sep…