We have used AGVIto automatically generate and implement authentication and key distribution protocols involving two parties with or without a trusted third party. In one experiment, we vary the system aspects: one system specication has a low computation overhead but a high communication overhead and another system specication has a low communication overhead and a high computation overhead. The AGVIfound different optimal protocols for metric functions used in the two different cases. In another experiment, we vary the security properties required by the system. Key distribution protocols normally have a long list of possile security properties and an application might only require a subset of the list. The AGVIalso found different optimal protocols for different security requirements. In both experiments, AGVIfound new protocols that are more efficient or as efficient as the protocols documented in the literature. More details can be found in [PS00a, PS00b].
Acknowledgments: We would like to thank Doug Tygar and Jon Millen for their encouragement and stimulating discussions.