Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols. (English) Zbl 1137.68431
Summary: We investigate the applicability of a bottom-up evaluation strategy for a first-order fragment of affine linear logic that we introduced in [Theory Pract. Log. Program. 4, No. 5-6, 573–619 (2004; Zbl 1088.68102)] for the purposes of automated verification of secrecy in cryptographic protocols. Following [I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, A. Scedrov, A meta-notation for protocol analysis. In: Proceedings 12th Computer Security Foundations Workshop, CSFW’99, Mordano, Italy. IEEE Computer Society Press, pp. 55–69 (1999)], we use multi-conclusion clauses to represent the behaviour of agents in a protocol session, and we adopt the Dolev-Yao intruder model. In addition, universal quantification provides a formal and declarative way to express creation of nonces. Our approach is well suited to verifying properties which can be specified by means of minimal conditions. Unlike traditional approaches based on model checking, we can reason about parametric, infinite-state systems; thus we do not pose any limitation on the number of parallel runs of a protocol. Furthermore, our approach can be used both to find attacks and to verify secrecy for a protocol. We apply our method to analyse several classical examples of authentication protocols. Among them we consider the ffgg protocol [Proceedings of the Workshop on Formal Methods and Security Protocols (1999)]. This protocol is a challenging case study in that it is free from sequential attacks, whereas it suffers from parallel attacks that occur only when at least two sessions are run in parallel. The other case studies are of the Otway-Rees protocol and several formulations of the Needham-Schroeder protocol.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68M12 | Network protocols |
| 94A60 | Cryptography |
Citations:
Zbl 1088.68102References:
| [1] | Abdulla, P. A.; Cerans, K.; Jonsson, B.; Tsay, Y.-K., Algorithmic analysis of programs with well quasi-ordered domains, Information and Computation, 160, 1-2, 109-127 (2000) · Zbl 1046.68567 |
| [2] | Amadio, R.; Lugiez, D., On the reachability problem in cryptographic protocols, (Palamidessi, C., Proceedings 11th International Conference on Concurrency Theory. Proceedings 11th International Conference on Concurrency Theory, CONCUR’00, University Park, Pennsylvania. Proceedings 11th International Conference on Concurrency Theory. Proceedings 11th International Conference on Concurrency Theory, CONCUR’00, University Park, Pennsylvania, LNCS, vol. 1877 (2000), Springer-Verlag), 380-394 · Zbl 0999.94538 |
| [3] | Andreoli, J.-M., Logic programming with focusing proofs in linear logic, Journal of Logic and Computation, 2, 3, 297-347 (1992) · Zbl 0764.03020 |
| [4] | Andreoli, J.-M.; Pareschi, R., Linear objects: logical processes with built-in inheritance, New Generation Computing, 9, 3-4, 445-473 (1991) · Zbl 0731.68022 |
| [5] | Armando, A.; Compagna, L., Abstraction-driven SAT-based analysis of security protocols, (Giunchiglia, E.; Tacchella, A., Proceedings 6th International Conference on Theory and Applications of Satisfiability Testing. Proceedings 6th International Conference on Theory and Applications of Satisfiability Testing, SAT’2003, S. Margherita Ligure, Italy. Proceedings 6th International Conference on Theory and Applications of Satisfiability Testing. Proceedings 6th International Conference on Theory and Applications of Satisfiability Testing, SAT’2003, S. Margherita Ligure, Italy, LNCS, vol. 2919 (2003), Springer-Verlag), 257-271 · Zbl 1204.68031 |
| [6] | Armando, A.; Compagna, L.; Ganty, P., SAT-based model-checking of security protocols using planning graph analysis, (Araki, K.; Gnesi, S.; Mandrioli, D., Proceedings 12th International FME Symposium. Proceedings 12th International FME Symposium, FM’2003, Pisa, Italy. Proceedings 12th International FME Symposium. Proceedings 12th International FME Symposium, FM’2003, Pisa, Italy, LNCS, vol. 2805 (2003), Springer-Verlag), 875-893 |
| [7] | Basin, D., Lazy infinite-state analysis of security protocols, (Baumgart, R., Proceedings International Exhibition and Congress on Secure Networking. Proceedings International Exhibition and Congress on Secure Networking, Cqre Secure’99, Dusseldorf, Germany. Proceedings International Exhibition and Congress on Secure Networking. Proceedings International Exhibition and Congress on Secure Networking, Cqre Secure’99, Dusseldorf, Germany, LNCS, vol. 1740 (1999), Springer-Verlag), 30-42 |
| [8] | Blanchet, B., An efficient cryptographic protocol verifier based on Prolog rules, (Proceedings 14th Computer Security Foundations Workshop. Proceedings 14th Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada (2001), IEEE Computer Society Press), 82-96 |
| [9] | Boreale, M., Symbolic trace analysis of cryptographic protocols, (Orejas, F.; Spirakis, P. G.; van Leeuwen, J., Proceedings 28th International Colloquium on Automata, Languages and Programming, ICALP’01. Proceedings 28th International Colloquium on Automata, Languages and Programming, ICALP’01, Heraklion, Crete, Greece. Proceedings 28th International Colloquium on Automata, Languages and Programming, ICALP’01. Proceedings 28th International Colloquium on Automata, Languages and Programming, ICALP’01, Heraklion, Crete, Greece, LNCS, vol. 2076 (2001), Springer-Verlag), 667-681 · Zbl 0986.94022 |
| [10] | Bozzano, M., Ensuring security through model checking in a logical environment (Preliminary Results), (Proceedings Workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic. Proceedings Workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic, SAVE’01, Paphos, Cyprus (2001)) |
| [11] | Bozzano, M., 2002. A logic-based approach to model checking of parameterized and infinite-state systems. Ph.D. Thesis, Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova; Bozzano, M., 2002. A logic-based approach to model checking of parameterized and infinite-state systems. Ph.D. Thesis, Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova |
| [12] | Bozzano, M.; Delzanno, G., Automated protocol verification in linear logic, (Proceedings 4th International Conference on Principles and Practice of Declarative Programming. Proceedings 4th International Conference on Principles and Practice of Declarative Programming, PPDP’02, Pittsburgh, Pennsylvania (2002), ACM Press), 38-49 |
| [13] | Bozzano, M.; Delzanno, G.; Martelli, M., A bottom-up semantics for linear logic programs, (Proceedings 2nd International Conference on Principles and Practice of Declarative Programming. Proceedings 2nd International Conference on Principles and Practice of Declarative Programming, PPDP’00, Montreal, Canada (2000), ACM Press), 92-102 |
| [14] | Bozzano, M.; Delzanno, G.; Martelli, M., An effective fixpoint semantics for linear logic programs, Theory and Practice of Logic Programming, 2, 1, 85-122 (2002) · Zbl 1087.68578 |
| [15] | Bozzano, M.; Delzanno, G.; Martelli, M., Model checking linear logic specifications, Theory and Practice of Logic Programming, 4, 5, 1-47 (2004) |
| [16] | Burrows, M., Abadi, M., Needham, R., 1989. A logic of authentication. Technical Report 39, Digital Equipment Corporation Systems Research Center; Burrows, M., Abadi, M., Needham, R., 1989. A logic of authentication. Technical Report 39, Digital Equipment Corporation Systems Research Center · Zbl 0687.68007 |
| [17] | Cervesato, I., Petri nets and linear logic: a case study for logic programming, (Alpuente, M.; Sessa, M. I., Proceedings Joint Conference on Declarative Programming. Proceedings Joint Conference on Declarative Programming, GULP-PRODE’95, Marina di Vietri, Italy (1995), Palladio Press), 313-318 |
| [18] | Cervesato, I., The Dolev-Yao intruder is the most powerful attacker, (Halpern, J., Proceedings 16th Annual International Symposium on Logic in Computer Science. Proceedings 16th Annual International Symposium on Logic in Computer Science, LICS’01, Boston, Massachusetts (2001)), (Short paper) |
| [19] | Cervesato, I., Typed multiset rewriting specifications of security protocols, (Seda, A., Proceedings 1st Irish Conference on the Mathematical Foundations of Computer Science and Information Technology. Proceedings 1st Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT’00, Cork, Ireland (2001)) · Zbl 1264.68075 |
| [20] | Cervesato, I.; Durgin, N. A.; Lincoln, P. D.; Mitchell, J. C.; Scedrov, A., A meta-notation for protocol analysis, (Proceedings 12th Computer Security Foundations Workshop. Proceedings 12th Computer Security Foundations Workshop, CSFW’99, Mordano, Italy (1999), IEEE Computer Society Press), 55-69 |
| [21] | Chevalier, Y.; Vigneron, L., Automated unbounded verification of security protocols, (Brinksma, E.; Larsen, K. G., Proceedings 14th International Conference on Computer Aided Verification. Proceedings 14th International Conference on Computer Aided Verification, CAV’02, Copenhagen, Denmark. Proceedings 14th International Conference on Computer Aided Verification. Proceedings 14th International Conference on Computer Aided Verification, CAV’02, Copenhagen, Denmark, LNCS, vol. 2404 (2002), Springer-Verlag), 324-337 · Zbl 1010.68508 |
| [22] | Cirstea, H., Specifying authentication protocols using rewriting and strategies, (Ramakrishnan, I. V., Proceedings of Conference on Practical Aspects of Declarative Languages. Proceedings of Conference on Practical Aspects of Declarative Languages, PADL’01, Las Vegas, Nevada. Proceedings of Conference on Practical Aspects of Declarative Languages. Proceedings of Conference on Practical Aspects of Declarative Languages, PADL’01, Las Vegas, Nevada, LNCS, vol. 1990 (2001), Springer-Verlag), 138-152 |
| [23] | Clark, J.; Jacob, J., 1997. A Survey of Authentication Protocol Literature, Web Draft Version 1.0 Available from |
| [24] | Cohen, E., TAPS: A first-order verifier for cryptographic protocols, (Proceedings 13th Computer Security Foundations Workshop. Proceedings 13th Computer Security Foundations Workshop, CSFW’00, Cambridge, England (2000), IEEE Computer Society Press), 144-158 · Zbl 0974.68562 |
| [25] | Delzanno, G., Specifying and debugging security protocols via hereditary Harrop formulas and \(λ\) Prolog—A case-study, (Kuchen, H.; Ueda, K., Proceedings 5th International Symposium on Functional and Logic Programming. Proceedings 5th International Symposium on Functional and Logic Programming, FLOPS’01, Tokyo, Japan. Proceedings 5th International Symposium on Functional and Logic Programming. Proceedings 5th International Symposium on Functional and Logic Programming, FLOPS’01, Tokyo, Japan, LNCS, vol. 2024 (2001), Springer-Verlag), 123-137 · Zbl 0977.68526 |
| [26] | Denker, G.; Meseguer, J.; Talcott, C., Protocol specification and analysis in Maude, (Heintze, N.; Wing, J., Proceedings Workshop on Formal Methods and Security Protocols. Proceedings Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana (1998)) · Zbl 0962.68081 |
| [27] | Dolev, D.; Yao, A., On the security of public-key protocols, IEEE Transactions on Information Theory, 2, 29 (1983) · Zbl 0502.94005 |
| [28] | Fages, F.; Ruet, P.; Soliman, S., Linear concurrent constraint programming: operational and phase semantics, Information and Computation, 165, 1, 14-41 (2001) · Zbl 1003.68065 |
| [29] | Genet, T.; Klay, F., Rewriting for cryptographic protocol verification, (McAllester, D. A., Proceedings 17th International Conference on Automated Deduction. Proceedings 17th International Conference on Automated Deduction, CADE-17. Proceedings 17th International Conference on Automated Deduction. Proceedings 17th International Conference on Automated Deduction, CADE-17, LNCS, vol. 1831 (2000), Springer-Verlag), 271-290 · Zbl 0963.94016 |
| [30] | Girard, J.-Y., Linear logic, Theoretical Computer Science, 50, 1, 1-102 (1987) · Zbl 0625.03037 |
| [31] | Jacquemard, F.; Rusinowitch, M.; Vigneron, L., Compiling and verifying security protocols, (Parigot, M.; Voronkov, A., Proceedings 7th International Conference on Logic for Programming and Automated Reasoning. Proceedings 7th International Conference on Logic for Programming and Automated Reasoning, LPAR’00, Reunion Island, France. Proceedings 7th International Conference on Logic for Programming and Automated Reasoning. Proceedings 7th International Conference on Logic for Programming and Automated Reasoning, LPAR’00, Reunion Island, France, LNCS, vol. 1955 (2000), Springer-Verlag), 131-160 · Zbl 0988.68562 |
| [32] | Kobayashi, N.; Yonezawa, A., Asynchronous communication model based on linear logic, Formal Aspects of Computing, 7, 2, 113-149 (1995) · Zbl 0835.68016 |
| [33] | Lowe, G., An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, 56, 131-133 (1995) · Zbl 0875.94114 |
| [34] | Lowe, G., Breaking and fixing the Needham-Schroeder public-key protocol using FDR, (Margaria, T.; Steffen, B., Proceedings 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems. Proceedings 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems, TACAS’96, Passau, Germany. Proceedings 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems. Proceedings 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems, TACAS’96, Passau, Germany, LNCS, vol. 1055 (1996), Springer-Verlag), 147-166 |
| [35] | Lowe, G., Casper: a compiler for the analysis of security protocols, Journal of Computer Security, 6, 1, 53-84 (1998) |
| [36] | Lowe, G., Towards a completeness result for model checking of security protocols, Journal of Computer Security, 7, 2-3, 89-146 (1999) |
| [37] | Marrero, W., Clarke, E., Jha, S., 1997. Model checking for security protocols. Technical Report CMU-CS-97-139, School of Computer Science, Carnegie Mellon University; Marrero, W., Clarke, E., Jha, S., 1997. Model checking for security protocols. Technical Report CMU-CS-97-139, School of Computer Science, Carnegie Mellon University |
| [38] | McDowell, R.; Miller, D.; Palamidessi, C., Encoding transition systems in sequent calculus, (Girard, J.-Y.; Okada, M.; Scedrov, A., Proceedings Linear Logic 96 Tokyo Meeting. Proceedings Linear Logic 96 Tokyo Meeting, Keio University, Tokyo, Japan. Proceedings Linear Logic 96 Tokyo Meeting. Proceedings Linear Logic 96 Tokyo Meeting, Keio University, Tokyo, Japan, ENTCS, vol. 3 (1996)) · Zbl 1028.68095 |
| [39] | Meadows, C., The NRL protocol analyzer: an overview, Journal of Logic Programming, 26, 2, 113-131 (1996) · Zbl 0871.68052 |
| [40] | Millen, J. K., A necessarily parallel attack, (Proceedings Workshop on Formal Methods and Security Protocols. Proceedings Workshop on Formal Methods and Security Protocols, Trento, Italy (1999)) |
| [41] | Millen, J.K., 1997. CAPSL: Common Authentication Protocol Specification Language. Technical Report MP 97B48, The MITRE Corporation; Millen, J.K., 1997. CAPSL: Common Authentication Protocol Specification Language. Technical Report MP 97B48, The MITRE Corporation |
| [42] | Millen, J. K.; Shmatikov, V., Constraint solving for bounded-process cryptographic protocol analysis, (Proceedings Conference on Computer and Communication Security. Proceedings Conference on Computer and Communication Security, CCS’01, Philadelphia, Pennsylvania (2001), ACM Press), 166-175 |
| [43] | Miller, D., The \(π\)-calculus as a theory in linear logic: preliminary results, (Lamma, E.; Mello, P., Proceedings Workshop on Extensions of Logic Programming. Proceedings Workshop on Extensions of Logic Programming, Bologna, Italy. Proceedings Workshop on Extensions of Logic Programming. Proceedings Workshop on Extensions of Logic Programming, Bologna, Italy, LNCS, vol. 660 (1992), Springer-Verlag), 242-265 |
| [44] | Miller, D., Forum: a multiple-conclusion specification logic, Theoretical Computer Science, 165, 1, 201-232 (1996) · Zbl 0872.68019 |
| [45] | Miller, D.; Nadathur, G.; Pfenning, F.; Scedrov, A., Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, 51, 125-157 (1991) · Zbl 0721.03037 |
| [46] | Needham, R.; Schroeder, M., Using encryption for authentication in large networks of computers, Communications of the ACM, 21, 12, 993-999 (1978) · Zbl 0387.68003 |
| [47] | Otway, D.; Rees, O., Efficient and timely mutual authentication, Operating Systems Review, 21, 1, 8-10 (1987) |
| [48] | Paulson, L. C., The inductive approach to verifying cryptographic protocols, Journal of Computer Security, 6, 1-2, 85-128 (1998) |
| [49] | Roscoe, A. W.; Broadfoot, P. J., Proving security protocols with model checkers by data independence techniques, Journal of Computer Security, 7, 2-3, 147-190 (1999) |
| [50] | Rusinowitch, M.; Turuani, M., Protocol insecurity with finite number of sessions is NP-complete, (Proceedings 14th Computer Security Foundations Workshop. Proceedings 14th Computer Security Foundations Workshop, CSFW’01, Cape Breton, Nova Scotia, Canada (2001), IEEE Computer Society Press) · Zbl 1042.68009 |
| [51] | Song, D. X., A new efficient automatic checker for security protocol analysis, (Proceedings 12th Computer Security Foundations Workshop. Proceedings 12th Computer Security Foundations Workshop, CSFW’99, Mordano, Italy (1999), IEEE Computer Society Press), 192-202 |
| [52] | Syverson, P.; Meadows, C.; Cervesato, I., Dolev-Yao is no better than Machiavelli, (Degano, P., Proceedings Workshop on Issues in the Theory of Security. Proceedings Workshop on Issues in the Theory of Security, WITS’00, Geneva, Switzerland (2000)), 87-92 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
