Applying Spi-calculus for PayWord
László Aszalós, Andrea Huszti · University of Debrecen Electronic Archive (University of Debrecen) · 2011
Achieving strong security properties is a core part of wide acceptance of electronic commerce, hence it is essential to provide detailed security analysis for cryptographic protocols. There are protocols considered secure for a long time, still it is shown they contain flaws. Therefore it has been recognized that informal arguments about protocol correctness are not reliable. Formal methods offer a promising way for automated security analysis. Spi-calculus is designed for describing and analyzing cryptographic protocols. In this article we present how to employ this method for formalizing the micropayment scheme PayWord developed by Ronald L. Rivest and Adi Shamir.