Abstract
NetBill is an electronic commerce protocol, which allows customers to purchase information goods from merchants over the Internet. It supports goods delivery as well as payment, while many other electronic commerce protocols do not take care of goods delivery. In this paper, we describe the case study in which NetBill has been analyzed with the OTS/CafeOBJ method.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56, 131–133 (1995)
Ogata, K., Futatsugi, K.: Flaw and modification of the iKP electronic payment protocols. Information Processing Letters 86, 57–62 (2003)
Abadi, M., Burrows, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems 8, 18–36 (1990)
Fábrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7, 191–230 (1999)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: WRLA 2002. ENTCS, vol. 71. Elsevier Science Publishers, Amsterdam (2002)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
MasterCard/Visa: SET secure electronic transactions protocol. Book One: Business Specifications, Book Two: Technical Specification, Book Three: Formal Protocol Definition (1997), http://www.setco.org/set_specifications.html
Cox, B., Tygar, J.D., Sirbu, M.: NetBill security and transaction protocol. In: First USENIX Workshop on Electronic Commerce, pp. 77–88 (1995)
Ogata, K., Futatsugi, K.: Formal analysis of the iKP electronic payment protocols. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 441–460. Springer, Heidelberg (2003)
Ogata, K., Futatsugi, K.: Formal verification of the Horn-Preneel micropayment protocol. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 238–252. Springer, Heidelberg (2002)
CafeOBJ: CafeOBJ homepage (2001), http://www.ldl.jaist.ac.jp/cafeobj/
Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, 6. World Scientific, Singapore (1998)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29, 198–208 (1983)
Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)
Heintze, N., Tygar, J., Wing, J., Wong, H.C.: Model checking electronic commerce protocols. In: Second USENIX Workshop on Electronic Commerce, pp. 147–164 (1996)
Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Transactions on Information and System Security 2, 332–351 (1999)
Bella, G., Massacci, F., Paulson, L.C., Tramontano, P.: Formal verification of Cardholder Registration in SET. In: ESORICS 2000. LNCS, vol. 1709, pp. 159–174. Springer, Heidelberg (1997)
Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET registration protocols. IEEE Journal on Selected Area in Communications 21, 77–87 (2003)
Bella, G., Massacci, F., Paulson, L.C.: The verification of an industrial payment protocol: The SET purchase phase. In: 9th ACM CCS, pp. 12–20. ACM Press, New York (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ogata, K., Futatsugi, K. (2004). Formal Analysis of the NetBill Electronic Commerce Protocol. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds) Software Security - Theories and Systems. ISSS 2003. Lecture Notes in Computer Science, vol 3233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-37621-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-37621-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23635-1
Online ISBN: 978-3-540-37621-7
eBook Packages: Springer Book Archive