Abstract
A second-level security protocol is defined as a security protocol that relies on an underlying security protocol in order to achieve its goals. The verification of classical authentication protocols has become routine, but second-level protocols raise new challenges. These include the formalisation of appeals to the underlying protocols, the modification of the threat model, and the formalisation of the novel goals. These challenges have been met using Isabelle and the Inductive Approach [14]. The outcomes are demonstrated on a recent protocol for certified e-mail delivery by Abadi et al. [2].
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Blanchet, B.: Computer-Assisted Verification of a Protocol for Certified Email. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694. Springer, Heidelberg (2003)
Abadi, M., Glew, N., Horne, B., Pinkas, B.: Certified email with a light on-line trusted third party: Design and implementation. In: Proceedings of the 11th International Conference on Wold Wide Web (WWW 2002). ACM Press and Addison Wesley (2002)
Asokan, N., Shoup, V., Waidner, M.: Asynchronous protocols for optimistic fair exchange. In: Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp. Society Press, Los Alamitos (1998)
Aura, T.: Distributed access-rights management with delegation certificates. In: Vitek, J., Jensen, C. (eds.) Secure Internet Programming. LNCS, vol. 1603, pp. 211–235. Springer, Heidelberg (1999)
Bella, G.: Inductive verification of smart card protocols. J. of Comp. Sec. 11(1), 87–132 (2003)
Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET registration protocols. IEEE J. of Selected Areas in Communications 21(1), 77–87 (2003)
Bella, G., Paulson, L.C.: Mechanical proofs about a non-repudiation protocol. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 91–104. Springer, Heidelberg (2001)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. of the 14th IEEE Comp. Sec. Found. Workshop. IEEE Comp. Society Press, Los Alamitos (1998)
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. Proceedings of the Royal Society of London 426, 233–271 (1989)
Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0. Technical report, University of York, Department of Computer Science (November 1997), Available on the web at http://www-users.cs.york.ac.uk/~jac/ , A complete specification of the Clark-Jacob library in CAPSL is available at http://www.cs.sri.com/~millen/capsl/
Cohen, E.: TAPS: A first-order verifier for cryptographic protocols. In: Proc. of the 13th IEEE Comp. Sec. Found. Workshop, pp. 144–158. IEEE Comp. Society Press, Los Alamitos (2000)
Fábrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand Spaces: Why is a Security Protocol Correct? In: Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp. Society Press, Los Alamitos (1998)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. of Comp. Sec. 6, 85–128 (1998)
Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Trans. on Inform. and Sys. Sec. 2(3), 332–351 (1999)
Ryan, P.Y.A., Schneider, S.A.: The Modelling and Analysis of Security Protocols: the CSP Approach. Addison Wesley Publ. Co., Reading (2000)
Shmatikov, V., Mitchell, J.C.: Analysis of a fair exchange protocol. In: Network and Distributed System Security Symposium, NDSS 2000 (2000)
Zhou, J., Gollmann, D.: A fair non-repudiation protocol. In: Symposium on Security and Privacy. IEEE Computer Society, Los Alamitos (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bella, G., Longo, C., Paulson, L.C. (2003). Verifying Second-Level Security Protocols. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_23
Download citation
DOI: https://doi.org/10.1007/10930755_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40664-8
Online ISBN: 978-3-540-45130-3
eBook Packages: Springer Book Archive