Suitability of a Classical Analysis Method for E-commerce Protocols

摘要: We present the adaptation of our model for validation key distribution and authentication protocols to address specific needs electronic commerce. The two models defer in both threat scenario formalization. demonstrate suitability by analyzing a version Internet Billing Server protocol introduced Carnegie Mellon University. Our analysis shows that, while security properties or shall provide are well understood, it is often not clear what an commerce can provide. methods rely on automatic theorem proving tools. Specifically, we used "Otter", software developed at Argonne National Laboratories.