Formal analysis of secure contracting protocol for e-tendering

ABSTRACT

Formal specification and verification of protocols have been credited for uncovering protocol flaws; revealing inadequacies in protocol design of the Initial Stage and Negotiation Stage; and proved that improved protocol performs in the desired manner while under modelled attacks from dishonest players. It also shows how formal methods can be used by protocol designer to achieve a better design of a complex system. Formal methods can also populate an abstract concept with a more complete and consistent protocol specification. Complex system protocol can be easily specified with simplifying assumptions for a high level of protocol verification. This set of assumptions can then be used to further explore the protocol. Using formal methods for complex secure system protocol design will provide not only better quality protocol but could also be the first step in advancing an abstract concept to a more practical stage for development.

REFERENCES

• 1: Colin Boyd , Peter Kearney, Exploring Fair Exchange Protocols Using Specification Animation, Proceedings of the Third International Workshop on Information Security, p.209-223, December 20-21, 2000
• 2: Du, R., Foo, E., Boyd, C., & Fitzgerald, B. (2004). Secure communication protocol for preserving e-tendering integrity. In Fifth asia-pacific industrial engineering and management systems conference (apiems'2004) (Vol. 14, p. 16.1-16.15). Asian Pacific Industrial Engineering and Management Society.
• 3: Gürgens, S., & Rudolph, C.(2002). Security analysis of (un-) fair non-repudiation protocols. In P. R. A.E. Abdallah & S. Schneider (Eds.), Formal aspects of security 2002-bcs fasec 2002 (Vol. LNCS 2629, p. 97-114). Berlin Heidelberg: Springer-Verlag.
• 4: Sigrid Gürgens , Peter Ochsenschläger , Carsten Rudolph, Role Based Specification and Security Analysis of Cryptographic Protocols Using Asynchronous Product Automata, Proceedings of the 13th International Workshop on Database and Expert Systems Applications, p.473-482, September 02-06, 2002
• 5: Catherine Meadows, Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis, Proceedings of the 12th International Conference on Computer Aided Verification, p.2, July 15-19, 2000
• 6: Meadows, C. (2003). Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communications, 21, 44-54.
• 7: Alfred J. Menezes , Scott A. Vanstone , Paul C. Van Oorschot, Handbook of Applied Cryptography, CRC Press, Inc., Boca Raton, FL, 1996
• 8: Ochsenschläger, P., Repp, J., Rieke, R., & Nitsche, U. (1999). The SH-Verification Tool-Abstraction-Based Verification of Co-operating Systems. Formal Aspects of Computing, The Int. Journal of Formal Methods, 11, 1-24.

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Security

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services
          Subjects: Web-based services
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.3 Group and Organization Interfaces

  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Electronic data interchange (EDI)

General Terms:
Algorithms, Security, Verification

Keywords:
e-commerce security, e-tendering, secure e-contract