This project is no longer active.
A typical security protocol is designed by experts, checked for correctness, and then implemented by developers in their applications. This division of labor is assumed to be robust, but actually it isn’t. Protocols have been formally verified and faithfully implemented (with each protocol action correctly coded), and then later found to have serious vulnerabilities.
How can this happen? The problem is that some platforms introduce new behaviors, causing traditional modular reasoning to fail. In web apps, for example, cross-site request forgeries can undermine a protocol, making the security guarantees of the designed actions worthless.
To prevent this, we designed a framework called Poirot that allows a protocol to be analyzed in the context of a particular platform. The developer needs only to provide a mapping that indicates how protocol actions are mapped to platform operations — for example, that the sending of a message is mapped to an HTTP request. Using a built-in repertoire of platform models, the framework reanalyzes the abstract protocol to find vulnerabilities under that mapping.
The approach has successfully identified vulnerabilities in commercial applications, and has been used (in an extension) to synthesize mappings for two versions of OAuth.
