Abstract
Motivated by Murray’s work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP’s theory of refinement, enabling subsequent step-wise refinement of the CSP model. Moreover, we improve upon existing CSP models of fair exchange protocols by proposing a revised intruder model inspired by the one of Cederquist and Dashti. Our intruder model is stronger as we use a weaker fairness constraint.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Gardiner, P., Goldsmith, M., Hulance, J., Jackson, D., Roscoe, B., Scattergood, B., Armstrong, P.: FDR Manual. Oxford University (2010)
Lowe, G.: Specification of communicating processes: Temporal logic versus refusals-based refinement. Formal Aspects of Computing 20, 277–294 (2008)
Murray, T.: On the limits of refinement-testing for model-checking CSP. Formal Aspects of Computing (to appear, 2012)
Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Software Tools for Technology Transfer 12, 9–21 (2010)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29, 198–208 (1983)
Kremer, S., Markowitch, O., Zhou, J.: An intensive survey of fair non-repudiation protocols. Computer Communications 25, 1606–1621 (2002)
Asokan, N.: Fairness in electronic commerce. Technical report, University of Waterloo (1998)
Cederquist, J., Torabi Dashti, M.: An intruder model for verifying liveness in security protocols. In: Proc. FMSE 2006, pp. 23–32. ACM (2006)
Roscoe, A.: Understanding Concurrent Systems. Springer (2010)
Francez, N.: Fairness. Springer (1986)
Puhakka, A., Valmari, A.: Liveness and Fairness in Process-Algebraic Verification. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 202–217. Springer, Heidelberg (2001)
Torabi Dashti, M.: Keeping Fairness Alive. PhD thesis, VU University Amsterdam (2008)
Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Software Tools for Technology Transfer 10, 185–203 (2008)
Fokkink, W.J.: Modelling Distributed Systems. Springer (2007)
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model checking for regular alternation-free mu-calculus. Science of Computer Programming 46, 255–281 (2003)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall (1998)
Schneider, S.: Formal analysis of a non-repudiation protocol. In: Proc. CSF 1998, pp. 54–65. IEEE (1998)
Evans, N., Schneider, S.: Verifying security protocols with PVS: Widening the rank function approach. Journal of Logic and Algebraic Programming 64, 253–284 (2005)
Zhou, J., Gollman, D.: A fair non-repudiation protocol. In: S&P 1996, pp. 55–61. IEEE (1996)
Wei, K., Heather, J.: Towards Verification of Timed Non-repudiation Protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 244–257. Springer, Heidelberg (2006)
Wei, K., Heather, J.: A Theorem-Proving Approach to Verification of Fair Non-repudiation Protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 202–219. Springer, Heidelberg (2007)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Williams, D.M., de Ruiter, J., Fokkink, W. (2012). Model Checking under Fairness in ProB and Its Application to Fair Exchange Protocols. In: Roychoudhury, A., D’Souza, M. (eds) Theoretical Aspects of Computing – ICTAC 2012. ICTAC 2012. Lecture Notes in Computer Science, vol 7521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32943-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-32943-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32942-5
Online ISBN: 978-3-642-32943-2
eBook Packages: Computer ScienceComputer Science (R0)