Theorem Proving in Higher Order Logics 16th International Conference
This volume constitutes the proceedings of the16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003) held September 8–12, 2003 in Rome, Italy. TPHOLs covers all aspects of theorem proving in higher order logics as well as re
- PDF / 189,788 Bytes
- 15 Pages / 430 x 660 pts Page_size
- 97 Downloads / 186 Views
2
Computer Laboratory, University of Cambridge 15 JJ Thomson Avenue, Cambridge CB3 0FD (UK) {gb221,lcp}@cl.cam.ac.uk Dipartimento di Matematica e Informatica, Universit` a di Catania Viale A. Doria 6, I-95125 Catania (ITALY) {giamp,longo}@dmi.unict.it
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].
1
Introduction
The development of security protocols during the last two and a half decades has mainly focused on the fundamental goals of authentication, which confirms the identity of a peer, and of confidentiality, which confirms that a message is kept from attackers. Somewhat simplistically, security protocols have often been referred to as authentication protocols [9,10]. However, the growth of Internet transactions and distributed computing in general require more sophisticated goals such as anonymity, non-repudiation [18], delegation [4] and certified delivery [2]. No one can predict what security goals will become important next year. Many recent protocols rely on some other protocol as a primitive. For example, the fair-exchange protocol by Asokan et al. [3] presupposes that the peers authenticate each other by means of an authentication protocol before they engage in a transaction whereby they commit to a contract. The certified e-mail protocol by Abadi et al. requires the establishment of a secure channel between the e-mail recipient and the trusted third party: “in practice, such a channel might be an SSL connection” [2]. But SSL is already rather complicated [15], hence a protocol that employs it becomes even more complicated as a whole, unless we assume that SSL works correctly. These observations inspire our definition of second-level protocols. Definition 1 (Second-Level Protocol). A second-level security protocol is a security protocol that relies on the goals of underlying authentication protocols in order to achieve its goals. D. Basin and B. Wolff (Eds.): TPHOLs 2003, LNCS 2758, pp. 352–366, 2003. c Springer-Verlag Berlin Heidelberg 2003
Verifying Second-Level Security Protocols
353
This concept is natural. Any kind of construction customarily makes use of existing constructions, and this process can be iterated. Likewise, our definition can be trivially generalised for nth -level protocols, which employ (n − 1)st -level protocols. In turn, classical authentication protocols can be seen as first-level protocols, which adopt 0th -level protocols, the transfer protocols. The verification of authentication protocols can be considered mature. Innumerable a
Data Loading...
