Our Publications

by Dawn Song, Adrian Perrig, and Doantam Phan
Abstract:
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 toolkit 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. AGVIwill then 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.
Reference:
AGVI — Automatic Generation, Verification, and Implementation of Security Protocols. Dawn Song, Adrian Perrig, and Doantam Phan. In Proceedings of the Conference on Computer Aided Verification (CAV) 2001.
Bibtex Entry:
@InProceedings{SoPePh2001,
    author =       {Dawn Song and Adrian Perrig and Doantam Phan},
    title =        {{AGVI} --- Automatic Generation, Verification, and Implementation of Security Protocols},
    url = {/publications/papers/cav01.pdf},
    booktitle =    {Proceedings of the Conference on Computer Aided Verification (CAV)},
    year =         2001,
    month =        jul,
    abstract =     {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 toolkit 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. AGVIwill then 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.}
}