google / asylo

An open and flexible framework for developing enclave applications
https://asylo.dev
Apache License 2.0
967 stars 126 forks source link

Add a formal EKEP analysis and discussion. #73

Closed tmroeder closed 2 years ago

tmroeder commented 2 years ago

This directory contains a formal analysis of the EKEP protocol in ProVerif, showing that this protocol satisfies useful security properties.

This directory also contains some useful tools for writing and testing modular ProVerif code, including a script for using the C Preprocessor to write macros, and a simple unit-test framework.