Cryptis: Cryptographic Reasoning in Separation Logic

TL;DR

Cryptis extends Iris separation logic to enable formal verification of cryptographic protocols and systems, combining cryptographic reasoning with separation logic to improve correctness proofs and reusability.

Contribution

We introduce Cryptis, a novel extension of Iris logic that integrates cryptographic reasoning, allowing formal verification of cryptographic components and protocols within a unified framework.

Findings

Verified multiple authentication protocols

Validated a key-value store server using Cryptis

Formalized results in Coq

Abstract

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 separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq.