Analysis of Offline Fair Exchange Protocols in Strand Spaces

Formal and efficient protocol analysis by pen and paper is highly desired when informal and model-checking methods are not trusted in proving correctness of complicated e-commerce protocols. Based on strand spaces, this paper presents a method for fairness analysis of offline fair exchange protocols. With the new method, this paper formally analyzes an important offline fair exchange protocol -- the ASW certified email protocol, detects two flaws, and makes an improvement. The security analysis shows that such protocols as complicated as fair exchanges can be formally analyzed by pen and paper.