Back to Dawn Song's Index page



Athena

 I have been interested in security protocol analysis. Just imagine an intruder sitting on the network, observing and disturbing packets. If a security protocol is flawed (and many real protocols are), the intruder can easily learn the secret session key, or impersonate as another honest party, even without cracking the cryptographic primitives! What can we do?

I recently developed an automatic tool, Athena, which can verify whether a security protocol satisfies a given property. Athena outperforms other existing automatic tools for security protocol analysis in several aspects. It has the ability to analyze infinite state space. If a protocol satisfies a given property, Athena will provide a proof, otherwise, a counterexample will be generated. It also exploits several state-space reduction techniques which greatly reduces the state-space-explosion problem.

Maybe to your surprise, Athena is actually very easy to use. Hope you will be able to try it out soon!

For details about the theory and algorithm behind Athena: Athena, an Automatic Checker for Security Protocol Analysis (ps). In Proc. of 12th Computer Security Foundation Workshop, 1999 June.


Security & Cryptography

 Besides security protocol analysis, I have been pursuing solutions to general security problems. Here are two case studies that I have performed.

Secure Auctions:
How can we provide a real secure and scalable system for sealed-bid auction which can even tolerate byzantine failures? How can we prove an auction system always draw the correct winning bid and is a fair system? We try to give some answers: Secure Auctions in a Publish/Subscribe System (ps), with Jon Millen.

Hash Visualization:
It is a pain to remember long random strings. I have so many different IDs and passwords that I often confuse myself, or even worse, I pick the same passwords for many different logins -- not a good idea for security! How can we make our lives less troublesome and more secure? Our answer is to generate images when hashing: Hash Visualization: a way to improve real world security (ps), with Adrian Perrig. In Proc. of CrypTech'99.


PL & Software Engineering

 How do you know your program won't crash? How can you guarantee your program is doing the right thing? Ten years after the Morris Internet Worm, still over 80 per cent of the Internet attack now is owing to buffer overflow. I often ask myself what is an effective solution?


Networking

 Nothing is changing people's lives more than the fast-growing Internet. Urge for scalability and better services raise great challenge. I have looked at from one angle: secure multicast. How to distribute real-time stock quotes over the Internet? How to hold a secure video conferencing? Our general framework with scalable key management: SMIF: A Framework for Secure Multicast Intercommunication, with Yang-hua Chu and Adrian Perrig