Abstract
In this paper we propose a novel approach to the analysis of security protocols, using the process algebra CSP to model such protocols and verifying security properties using a combination of the FDR model checker and the PVS theorem prover. Although FDR and PVS have enjoyed success individually in this domain, each suffers from its own deficiency: the model checker is subject to state space explosion, but superior in finding attacks in a system with finite states; the theorem prover can reason about systems with massive or infinite states spaces, but requires considerable human direction. Using FDR and PVS together makes for a practical and interesting way to attack problems that would remain out of reach for either tool on its own.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proceedings of 8th IEEE Computer Security Foundations Workshop (1995)
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)
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: The Modelling and Analysis of Security Protocols. Addison Wesley, Reading (2000)
Dutertre, B., Schneider, S.A.: Embedding CSP in PVS: an application to authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275. Springer, Heidelberg (1997)
Paulson, L.C.: Verifying the SET protocol: Overview. In: Abdallah, A.E., Ryan, P.Y.A., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 4–14. Springer, Heidelberg (2003)
Cohen, E.: Taps: A first-order verifier for cryptographic protocols. In: 13th IEEE Computer Security Foundations Workshop — CSFW 2000, Cambridge, UK, July 3-5, pp. 144–158. IEEE Computer Society Press, Los Alamitos (2000)
Song, D.X.: Athena: a new efficient checker for security protocol analysis. In: Proceedings of 12th IEEE Computer Security Foundations Workshop (1999)
Thayer, J., Herzog, J., Guttman, J.: Strand spaces: Proving security protocols correct. Journal of Computer Security (1999)
Heather, J.A.: Oh! ... Is it really you?—Using rank functions to verify authentication protocols. Department of Computer Science, Royal Holloway, University of London (2000)
Heather, J.A., Schneider, S.A.: Towards automatic verification of authentication protocols on an unbounded network. Technical Report 00-04. Royal Holloway, University of London (2000)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Englewood Cliffs (1998)
Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons, Chichester (1999)
Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 10\(^{\mbox{20}}\) dining philosophers for deadlock. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heather, J., Wei, K. (2009). Where Next for Formal Methods?. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds) Security Protocols. Security Protocols 2006. Lecture Notes in Computer Science, vol 5087. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04904-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-04904-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04903-3
Online ISBN: 978-3-642-04904-0
eBook Packages: Computer ScienceComputer Science (R0)