Protocol Validation

µCRL is a specification language based on process algebra together with abstract data types. The toolset of µCRL allows the user to automatically transform a µCRL specification into a graph representing process behaviour. The French toolset CADP can be used to analyse this graph.

First an overview is given of abstract data types and process algebra. The specification language µCRL is explained in detail. Next network protocols like the Bounded Retransmission Protocol, the IEEE 1394 Tree Identify Protocol, the Sliding Window Protocol and the Needham-Schroeder Protocol are treated. In the lectures these protocols will be explained and specified algebraically, while in the labs these protocols are analysed using the µCRL and CADP toolsets.

Model checking is an automated technique to verify properties of process graphs. Several model checking logics will be explained, together with model checking algorithms. In the labs, model checking will be applied on some of the protocols, using CADP.

There is a homework exercise, consisting of an analysis of the Sliding Window Protocol, using the µCRL and CADP tools.

There is a set of lecture notes, which can be downloaded from the web. Relevant literature is:

• M. Bezem and J.F. Groote, A correctness proof of a one bit sliding window protocol in µCRL, The Computer Journal, 37(4):289-307, 1994
• E.M. Clarke, O. Grumberg and D.A. Peled, Model Checking, MIT Press, 1999
• W. Fokkink, Introduction to process algebra, Springer-Verlag, 2000
• J.F. Groote and A. Ponse, Syntax and semantics of µCRL, In Proceedings 1st Workshop on the Algebra of Communicating Processes (ACP'94), Workshops in Computing, pp. 26-62 Springer-Verlag, 1995
• J.F. Groote and J. van de Pol, A bounded retransmission protocol for large data packets: a case study in computer checked verification, In Proceedings 5th Conference on Algebraic Methodology and Software Technology (AMAST'96)}, LNCS 1101, pp. 536-550. Springer-Verlag, 1996
• M.R.A. Huth and M.D. Ryan, Logic in Computer Science: Modelling and reasoning about systems, Cambridge University Press, 2000
• G. Lowe, An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, 56(3):131-133, 1995.
• C. Shankland and M. van der Zwaag, The tree identify protocol of IEEE 1394 in µCRL, Formal Aspects of Computing, 10(6):509-531, 1998
• A. Tanenbaum, Computer Networks, Prentice Hall, 1981