Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
G2C: Cryptographic Protocols from Goal-Driven Specifications
Erschienen in: Theory of Security and Applications
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present
G2C
, a goal-driven specification language for distributed applications. This language offers support for the declarative specification of functionality goals and security properties. The former comprise the parties, their inputs, and the goal of the communication protocol. The latter comprise secrecy, access control, and anonymity requirements. A key feature of our language is that it abstracts away from
how
the intended functionality is achieved, but instead lets the system designer concentrate on
which
functional features and security properties should be achieved. Our framework provides a compilation method for transforming
G2C
specifications into symbolic cryptographic protocols, which are shown to be optimal. We provide a technique to automatically verify the correctness and security of these protocols using ProVerif, a state-of-the-art automated theorem-prover for cryptographic protocols. We have implemented a
G2C
compiler to demonstrate the feasibility of our approach.