skip to main content
10.1145/1066677.1066864acmconferencesArticle/Chapter ViewAbstractPublication PagessacConference Proceedingsconference-collections
Article

An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol

Published: 13 March 2005 Publication History

Abstract

In this work we describe an approach to deal with systems having at the same time probabilistic and real-time behaviors. The main goal in the paper is to show the automatic translation from a real time model based on UPPAAL tool, which makes automatic verification of Real Time Systems, to the RAPTURE tool, which makes verification of probabilistic systems.Furthermore, this approach allows us to use the best techniques developed in both tools (abstraction, refinement, state space reduction, etc). Finally, this translation is applied to verify a case study, the SET internet protocol.

References

[1]
K. Larsen B. Jonsson and W. Yi. Probabilistic process algebra. E-HPA, chapter 4: Extensions, pages 685--710. 2001.]]
[2]
J. Bengtsson, K. Larsen, F. Larsson, P. Petterson, Yi Wang, and C. Weise. New Generation of UPPAAL. In Int. Workshop on Software Tools for Technology Transfer, June 1998.]]
[3]
D. Bolignano. Towards the formal verification of electronic commerce protocols. In Proc. 10th IEEE Computer Security Foundations Workshop, 1997.]]
[4]
P. Broadfoot and G. Lowe. On distributed security transactions that use secure transport protocols, 2003.]]
[5]
P. D'Argenio, B., H. Jensen, and K. Larsen. Reduction and refinement strategies for probabilistic analysis. In Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBMIV 2002, volume 2399 of LNCS, Copenhagen (Denmark), July 2002.]]
[6]
P. D'Argenio, B. Jeannet, H. Jensen, and K. Larsen. Reachability analysis of probabilistic systems by successive refinements. In PAPM-PROBM 2001, volume 2165 of LNCS, Aachen (Germany).]]
[7]
G. Díaz, D. Cazorla, F. Pelayo, F. Cuartero, and V. Valero. Verifying and capturing probabilistic bechaviours of real-time systems. In 19th Annual UK Performance Engineering Workshop, 2003.]]
[8]
G. Díaz, F. Cuartero, V. Valero, and F. L. Pelayo. Automatic verification of the tls handshake protocol. In Proceedings of the 19th ACM Symposium on Applied Computing (SAC 2004), Nicosia (Cyprus).]]
[9]
B. Jeannet, P. D'Argenio, and K. Larsen. RAPTURE: A tool for verifying markov decision processes. In Tools Day, International Conference on Concurrency Theory, CONCUR'02, Brno (Czech Republic), August 2002. Technical Report, Faculty of Informatics at Masaryk University Brno.]]
[10]
K. Larsen, P. Pettersson, and Wang Yi. UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2):134--152, October 1997.]]
[11]
F. Larsson, K. Larsen, P. Pettersson, and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, 1997.]]
[12]
G. Lowe. Towards a completeness result for model checking of security protocols. In Proc. of The 11th Computer Security Foundations Workshop, 1999.]]
[13]
M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Willey series in probability and mathematical statistics. Jhon Wiley and Sons, 1994.]]
[14]
A. W. Roscoe. Proving security protocols with model checkers by data independence techniques. In Proceedings of the IEEE Computer Security Foundations Workshop, 1998.]]
[15]
P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and Analysis of Security Protocols. Addison Wesley, 2001.]]
[16]
Mastercard & VISA. Set secure electronic transaction specification: Business description, 1997.]]
[17]
Mastercard & VISA. Set secure electronic transaction specification: Formal protocol definition, 1997.]]
[18]
Mastercard & VISA. Set secure electronic transaction specification: Programmer's guide, 1997.]]

Cited By

View all
  • (2006)Timed automata for web services verificationProceedings of the 6th WSEAS international conference on Applied computer science10.5555/1973812.1973921(531-536)Online publication date: 16-Dec-2006
  • (2006)Verification of Web Services with Timed AutomataElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.12.042157:2(19-34)Online publication date: 1-May-2006
  • (2005)Automatic translation of WS-CDL choreographies to timed automataProceedings of the 2005 international conference on European Performance Engineering, and Web Services and Formal Methods, international conference on Formal Techniques for Computer Systems and Business Processes10.1007/11549970_17(230-242)Online publication date: 1-Sep-2005

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
SAC '05: Proceedings of the 2005 ACM symposium on Applied computing
March 2005
1814 pages
ISBN:1581139640
DOI:10.1145/1066677
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 March 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. authentication protocols
  2. authentication protocols and model checking
  3. e-commerce
  4. security
  5. system verification and model checking

Qualifiers

  • Article

Conference

SAC05
Sponsor:
SAC05: The 2005 ACM Symposium on Applied Computing
March 13 - 17, 2005
New Mexico, Santa Fe

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25
The 40th ACM/SIGAPP Symposium on Applied Computing
March 31 - April 4, 2025
Catania , Italy

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 12 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2006)Timed automata for web services verificationProceedings of the 6th WSEAS international conference on Applied computer science10.5555/1973812.1973921(531-536)Online publication date: 16-Dec-2006
  • (2006)Verification of Web Services with Timed AutomataElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.12.042157:2(19-34)Online publication date: 1-May-2006
  • (2005)Automatic translation of WS-CDL choreographies to timed automataProceedings of the 2005 international conference on European Performance Engineering, and Web Services and Formal Methods, international conference on Formal Techniques for Computer Systems and Business Processes10.1007/11549970_17(230-242)Online publication date: 1-Sep-2005

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media