Verified Implementations for Real-World Cryptographic Protocols