2 papers
cs.CR2025
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…
math.LO2024
Kleene algebra with commutativity conditions is undecidable
Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in…