The Coinductive Approach to Verifying Cryptographic Protocols
We look at a new way of specifying and verifying cryptographic protocols using the Coalgebraic Class Specification Language. Protocols are specified into CCSL (with temporal operators for ”free”) and translated by the CCSL compiler into theories for the theorem prover PVS. Within PVS, the desired security conditions can then be (dis)proved.
In addition, we are interested in using assumptions which are reflected in real-life networks. However, as a result, we present only a partial solution here. We have not proved full correctness of a protocol under such loose restrictions. This prompts discussion of what assumptions are acceptable in protocol verification, and when practical concerns may outweigh theoretical motivations.
KeywordsMessage Passing Security Protocol Practical Concern Cryptographic Protocol Protocol Message
Unable to display preview. Download preview PDF.
- 1.Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: Proceedings of the Fourth ACM Conference on Computer and Communications Security, April 1997, pp. 36–47. ACM Press, New York (1997)Google Scholar
- 3.Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature, version 1.0 (1997), available at http://www-users.cs.york.ac.uk/~jac/papers/drareview.ps.gz
- 4.Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(6) (1983)Google Scholar
- 6.Lowe, G.: Casper: A compiler for the analysis of security protocols. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
- 7.Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communication Security, ACM SIGSAC, November 2001, pp. 166–175 (2001)Google Scholar
- 12.Rothe, J., Tews, H., Jacobs, B.: The coalgebraic class specification language CCSL. Journal of Universal Comp. Sci. 7(2) (2001)Google Scholar
- 13.Shanker, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.: PVS prover guide, Version 2.3 (1999)Google Scholar
- 14.Tews, H.: Coalgebraic Methods for Object Oriented Specification. PhD thesis, Technical University of Dresden (October 2002)Google Scholar
- 15.Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(1) (1999)Google Scholar