As new Internet applications emerge, new security protocols and systems need
to be designed and implemented. Unfortunately the current protocol design and
implementation process is often ad-hoc and error prone. To solve this problem,
we have designed and implemented a toolbox AGVI, Automatic
Generation, Verification, and Implementation of security protocols. With
AGVI, the protocol designer inputs the system specification (such as
cryptographic key setup) and security requirements, AGVI will automatically
find the near-optimal protocols for the specific application, proves the
correctness of the protocols and implement the protocols in Java. Our
experiments have successfully generated new and even simpler protocols than
the ones documented in the literature.
