Abstract
Cryptographic protocols are the algorithms and programs used to establish secure communication. They are fragile and are the main point of entry for security attacks, as a few examples will show. They are also very difficult to analyze. Formal proof is increasingly seen as the best way (if not the only way) to ensure that these protocols work. It often requires the implementation of highly sophisticated techniques.