A Formal Model for Systematic Design of Key Establishment Protocols

摘要

We present an abstract formal model for protocols, based on abstract logical secure channels. Unlike other models it is not primarily intended for protocol analysis but to serve as the top layer of a layered top-down design method for protocols. We show examples of key establishment protocols for which this model can be used. Modular design of protocols is supported with a concatenation theorem for protocols.