201 Wilson Commons, Rochester, 14611


Cryptis: Cryptographic Reasoning in Separation Logic


In this presentation, I'll talk about Cryptis, a tool we have been developing
for verifying systems that feature cryptographic components, such as a key-value
store server that connects to clients using some encryption protocol.  Cryptis
is a separation logic embedded in the Coq proof assistant, which can be used to
describe the implementation of protocols and systems that use these protocols.
Cryptis can check proofs of correctness involving arguments in the symbolic
model of cryptography, thus guaranteeing that protocols can deliver strong
security guarantees.



Arthur Azevedo de Amorim joined the Department of Computer Science at RIT in
2023 as an assistant professor.  His research interests revolve around the use
of programming-language and software-verification techniques to improve the
security and reliability of software.

Event Details

  • Melwyn Saldanha
  • David Agbertey

2 people are interested in this event



Meeting ID: 947 8259 2234

User Activity

No recent activity