I can give a talk *after* Jan 28, based on a recent paper with Bruno
"Automated formal analysis of a protocol for secure file sharing on
Abstract: We study formal security properties of a state-of-the-art
protocol for secure file sharing on untrusted storage, in the
automatic protocol verifier ProVerif. As far as we know, this is the
first automated formal analysis of a secure storage protocol.
The protocol, designed as the basis for the file system Plutus,
features a number of interesting schemes like lazy revocation and key
rotation. These schemes improve the protocol's performance, but
complicate its security properties. Our analysis clarifies several
ambiguities in the design and reveals some unknown attacks on the
protocol. We propose corrections, and prove precise security
guarantees for the corrected protocol.