@string{save01 = "Proc.\ Workshop on Specification, Analysis and Validation for Emerging Technologies (SAVE01)"} @string{edsave01 = "G. Delzanno and S. Etalle and M. Gabbrielli"} @string{csfw2001 = "Proc.\ 14th IEEE Computer Security Foundations Workshop"} @string{edcsfw2001 = "S. Schneider"} @inproceedings{LC03, author = {P. Laud and R. Corin}, title = {Sound Computational Interpretation of Formal Encryption with Composed Keys}, year = {2003}, booktitle={Information Security and Cryptology - ICISC 2003, 6th International Conference}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}} @Comment =================================================================== @Comment To be corrected @Comment =================================================================== @Article{Sch98csp, title = "Verifying Authentication Protocols in {CSP}", author = "S. Schneider", pages = "741--758", journal = "IEEE Transactions on Software Engineering", ISSN = "0098-5589", year = "1998", volume = "24", number = "9", abstract = "This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder Public-Key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs.", keywords = "Authentication, security protocols, formal methods, CSP, verification, Needham-Schroeder protocol", references = "M. Abadi and A.D. Gordon, {"}A Calculus for Cryptographic Protocols: The spi Calculus,{"} technical report, Univ. of Cambridge, 1996. M. Burrows, M. Abadi, and R. Needham, {"}A Logic of Authentication,{"} Technical Report 39, SRC, Dec. 1989. J. Davies and S. Schneider, {"}Recursion Induction for Real-Time Processes,{"} Formal Aspects of Computing, vol. 5, no. 6, 1993. W. Diffie, P.C. van Oorschot, and M.J. Wiener, {"}Authentication and Key Exchanges,{"} Designs, Codes, and Cryptography, vol. 2, 1992. D. Dolev and A.C. Yao, {"}On the Security of Public Key Protocols,{"} IEEE Trans. Information Theory, vol. 29, no. 2, 1983. D. Gollmann, {"}What Do We Mean by Entity Authentication,{"} IEEE Computer Society Symp. Research in Security and Privacy, 1996. C.A.R. Hoare, Comm. Sequential Processes. Prentice Hall, 1985. International Organisation for Standardisation, Information Processing Systems---Open Systems Interconnection---Basic Reference Model---Part 2: Security Architecture, ISO 7498-2. 1989. R. Kemmerer, C. Meadows, and J. Millen, {"}Three Systems for Cryptographic Protocol Analysis,{"} J. Cryptology, vol. 7, no. 2, 1994. G. Lowe, {"}An Attack on the Needham-Schroeder Public-Key Authentication Protocol,{"} Information Processing Letters, no. 56, 1995. G. Lowe, {"}Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR,{"} Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1055. Springer-Verlag, 1996. G. Lowe, {"}A Hierarchy of Authentication Specifications,{"} Proc. Computer Security Foundations Workshop, no. 10, 1997. C. Meadows, {"}Applying Formal Methods to the Analysis of a Key Management Protocol,{"} J. Computer Security, vol. 1, no. 1, 1992. J. Millen, {"}The Interrogator Model,{"} IEEE Computer Society Symp. Research in Security and Privacy, 1995. R. Milner, J. Parrow, and D. Walker, {"}A Calculus of Mobile Processes,{"} Information and Computation, no. 100, 1992. R. Needham and M.L. Schroeder, {"}Using Encryption for Authenticiation in Large Networks of Computers,{"} Comm. ACM, vol. 21, no. 12, 1978. S. Owre, N. Shankar, and J. Rushby, {"}The PVS Specification Language,{"} technical report, Computer Science Laboratory, SRI Int'l, 1993. L.C. Paulson, {"}Proving Properties of Security Protocols by Induction,{"} technical report, Univ. of Cambridge, UK, 1996. A.W. Roscoe, {"}Modelling and Verifying Key-Excfhange Protocols Using CSP and FDR,{"} Proc. Computer Security Foundations Workshop, no. 8, 1995. A.W. Roscoe, {"}Intensional Specifications of Security Protocols,{"} Computer Security Foundations Workshop, no. 9, 1996. A.W. Roscoe, The Theory and Practice of Concurrency. Prentice Hall, 1997. S.A. Schneider, {"}Security Properties and CSP,{"} IEEE Computer Society Symp. Research in Security and Privacy, 1996. P. Syverson and C. Meadows, {"}A Formal Language for Cryptographic Protocol Requirements,{"} Designs, Code,s and Cryptography, no. 7, 1996. T. Woo and S. Lam, {"}A Semantic Model for Authentication Protocols,{"} Proc. IEEE Computer Society Symp. Research in Security and Privacy, 1993.", annote = "incomplete", } @InProceedings{KR02, author = {S.\ Kremer and J-F. Raskin}, title = {Game Analysis of Abuse-free Contract Signing}, booktitle = {Proc.\ Computer Securuty Foundations Workshop 2002 (CSFW 2002)}, OPTpages = {}, year = {2002}, OPTeditor = {}, OPTnumber = {}, OPTseries = {}, OPTpublisher = {}, note = {available at: http://www.ulb.ac.be/di/scsi/skremer/} } @inProceedings{Ros95, author = {A.~W.~Roscoe}, title = {Modelling and verifying key-exchange protocols using CSP and FDR}, booktitle = {IEEE Symposium on Foundations of Secure Systems}, year = 1995, } @Misc{CV01-workshop, author = {Y.~Chevalier and L.~Vigneron}, title = {Towards Efficient Automated Verification of Security Protocols}, howpublished = {Proc. VERIF01, Verification Workshop in conjunction with IJCAR}, year = {2001}, OPTnote = {}, OPTannote = {} } @InProceedings{CV01, author = {Y.~Chevalier and L.~Vigneron}, title = {A Tool for Lazy Verification of Security Protocols}, booktitle = {Proc. 16th IEEE International Conference Automated Software Engineering}, OPTpages = {}, year = {2001}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{MK00, author = "O.\ Markowitch and S.\ Kremer", title = "A Multi-party Optimistic Non-repudiation Protocol", booktitle = "ICISC: International Conference on Information Security and Cryptology", publisher = "Springer-Verlag", year = "2000", } @InProceedings{KM00, author = "S.\ Kremer and O.\ Markowitch", title = "A multi-party non-repudiation protocol", booktitle = "SEC 2000: 15th International Conference on Information Security", series = "IFIP World Computer Congress", publisher = "Kluwer Academic", pages = "271--280", year = "2000" } @Comment =================================================================== @Comment To be downloaded or fetched !!! @Comment =================================================================== @InProceedings{BD94, author = {M. Burmester and Y. Desmedt}, title = {A Secure and Efficient Conference Key Distribution System}, booktitle = {EUROCRYPT}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, OPTyear = {1994}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{BD96, author = {M. Burmester and Y. Desmedt}, title = {Efficient and Secure Conference Key Distribution System}, booktitle = {Security Protocol Workshop}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, OPTyear = {1996}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{STW98, author = {M. Steiner and G. Tsudik and M. Waidner}, title = {CLIQUES: A New Approach to group key agreement}, booktitle = {18th IEEE International Conference on Distributed Computing Systems}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {1998}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @Article{BOGMR90, author = "M, {Ben-Or} and O. Goldreich and S. Micali and R. L. Rivest", title = "A Fair Protocol for Signing Contracts", number = "1", journal = "IEEE Transactions on Information Theory", volume = "36", pages = "40--46", year = "1990", annote = "The authors present a neat fair exchange protocol which works as follows: two parties $A$ and $B$ exchange in rounds signed statements of the form ``with probability $p$ the agreed-upon contract is valid for me'' ($p$ is different for messages signed by $A$ or by $B$). Both parties start with $p=0$ and independently decide how to increase their $p$. In the effective case, eventually both will receive a statement of the form ``with probability 1 the contract is valid for me''. In the non-effective case, one party (say $A$) can turn to a judge and present to it the last message it received from $B$. The judge throws a dice and decides with probability $p_B$ whether the contract holds for both or not. If it holds, $B$ must obey the contract too. If it does not hold, the contract is refuted. The judge must be able to recollect every verdict (and thus usually store the value together with the contract [a method is given how this can be circumvented]). Overall, this is a very interesting and well-written paper keeping mathematics small. The protocol can be seen as a very general and clever gradual exchange protocol which can also be applied if the to be exchanged item is not infinitely splittable. It is optimistic since the judge is only needed in failed cases. The paper is also interesting since it reviews some fairness definitions regarding gradual exchange (computational vs. probabilistic) and thus comes close to the formalization of strong fairness of \cite{Gaertner:1999:AFD}. Also, an impossibility result concerning two-party exchange is cited \cite{Even:1980:RAP} which is difficult to get, but relevant for \cite{Pagnia:1999:IFE}."} @InProceedings{BCDvdG88, author = "E. F. Brickell and D. Chaum and I. B. Damg{\aa}rd and J. van de Graaf", title = "Gradual and verifiable release of a secret", pages = "156--166", booktitle = "Proc.\ CRYPTO 87", editor = "Carl Pomerance", note = "Lecture Notes in Computer Science No. 293", publisher = "Springer-Verlag", year = "1988" } @Comment =================================================================== @Comment End to to be downloaded !!! @Comment =================================================================== @InProceedings{BFGLLP01, author = "S.\ Blom and W.\ Fokkink and J.\ F.\ Groote and I.\ van Langevelde and B.\ Lisser and J.\ van de Pol", title = "{$\mu$CRL:} {A} Toolset for Analysing Algebraic Specifications", booktitle = "Proceedings of the 13th Conference on Computer-Aided Verification (CAV'01)", pages = "250--254", year = "2001", editor = "G.\ Berry and H.\ Comon and A.\ Finkel", volume = "2102", series = "LNCS", publisher = "Springer-Verlag", } @book{Ros99, author = {A.~W.~Roscoe}, title = {The Theory and Practice of Concurrency}, publisher = {Prentice-Hall}, year = 1999, } @inproceedings{AHMQRT98, author = "R. Alur and T. Henzinger and F. Mang and S. Qadeer and S. Rajamani and Serdar Tasiran", title = "{MOCHA}: Modularity in Model Checking", booktitle = "Computer Aided Verification", pages = "521-525", year = "1998", url = "citeseer.nj.nec.com/alur98mocha.html" } @inproceedings{AHK97, author = "R. Alur and T. Henzinger and O. Kupferman", title = "Alternating-time Temporal Logic", booktitle = "38th {IEEE} Symposium on Foundations of Computer Science", pages = "100-109", year = "1997", url = "citeseer.nj.nec.com/article/alur97alternatingtime.html" } @InProceedings{Bor01, author = "Michele Boreale", title = "Symbolic Trace Analysis of Cryptographic Protocols", booktitle = "28th Colloquium on Automata, Languages and Programming ({ICALP})", year = "2001", series = "LNCS", publisher = "Springer-Verlag", url = "http://www.dsi.unifi.it/~boreale/symbspi.ps", abstract = "A cryptographic protocol can be described as a system of concurrent processes, and analysis of the traces generated by this system can be used to verify authentication and secrecy properties of the protocol. However, this approach suffers from a state-explosion problem that causes the set of states and traces to be typically infinite or very large. In this paper, starting from a process language inspired by the spi-calculus, we propose a symbolic operational semantics that relies on unification and leads to compact models of protocols. We prove that the symbolic and the conventional semantics are in full agreement, and then give a method by which trace analysis can be carried out directly on the symbolic model. The method is proven to be complete for the considered class of properties and is amenable to to automatic checking.", } @InProceedings{KMMS98, author = "K. P. Kihlstrom and L. E. Moser and P. M. Melliar-Smith", title = "The {SecureRing} Protocols for Securing Group Communication", booktitle = "31st Annual Hawaii International Conference on System Sciences (HICSS)", year = "1998", volume = "3", publisher = "IEEE Computer Society Press", pages = "317--326", ISBN = "0-8186-8239-6", ISSN = "1060-3425", keywords = "asynchronous distributed systems, Byzantine fault, group communication protocol, total order, group membership, fault (failure) detector", url = {http://beta.ece.ucsb.edu/pub/publications.html} } @InProceedings{KMMS97, author = "K. P. Kihlstrom and L. E. Moser and P. M. Melliar-Smith", title = "Solving Consensus in a {Byzantine} Environment Using an Unreliable Fault Detector", booktitle = "International Conference on Principles of Distributed Systems (OPODIS)", year = "1997", pages = "61--75", keywords = "consensus, asynchronous distributed systems, Byzantine fault, fault (failure) detector, distributed algorithms", url = {http://beta.ece.ucsb.edu/pub/publications.html} } @Article{SNW01, author = {R. Safavi-Naini and H. Wang}, title = {Broadcast Autentication for Group Communication}, journal = {Theoretical Computer Science}, volume = "269", number = "1--2", pages = "1--21", year = "2001", ISSN = "0304-3975", url = "http://www.elsevier.nl/gej-ng/10/41/16/219/27/27/abstract.html; http://www.elsevier.nl/gej-ng/10/41/16/219/27/27/article.pdf"} @Article{SM02, author = {V. Shmatikov and J. C. Mitchell}, title = {Finite-State Analysis of Two Contract Signing Protocols}, journal = {Theoretical Computer Science}, year = {2002}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, note = {Also available at citeseer.nj.nec.com/article/shmatikov01finitestate.html and at http://www.csl.sri.com/users/shmat/}} @inproceedings{SM00, author = "V. Shmatikov and J. C. Mitchell", title = "Analysis of Abuse-Free Contract Signing", booktitle = "Financial Cryptography", pages = "174-191", year = "2000", url = "citeseer.nj.nec.com/shmatikov00analysis.html" } @InProceedings{CKS01, author = {R. Chadha and M Kanovich and A Scedrov}, title = {Inductive Methods and Contract-Signing Protocols}, booktitle = {Eigth ACM Conference on Computer and Communications Security}, pages = {176--185}, year = {2001}, publisher = {ACM Press}, note = {available at http://www.cis.upenn.edu/~scedrov/recent_papers.html} } @Comment questo deve essere molto nuovo. @misc{yasi??, author = "Alec Yasinsac Yasinsac", title = "An Environment for Security Protocol Intrusion Detection", url = "citeseer.nj.nec.com/445485.html" } @article{FG97, author = "R.~Focardi and R.~Gorrieri", title = "The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties", journal = "Software Engineering", volume = "23", number = "9", pages = "550-571", year = "1997", url = "citeseer.nj.nec.com/67597.html" } @article{SBP01, author = "D. X. Song and S.~Berezin and A. Perrig", title = "Athena: A Novel Approach to Efficient Automatic Security Protocol Analysis", journal = "Journal of Computer Security", volume = "9", number = "1/2", pages = "47-74", year = "2001", url = "citeseer.nj.nec.com/401195.html" } @inproceedings{Song99, author = "D.~X.~Song", title = "Athena: {A} New Efficient Automatic Checker for Security Protocol Analysis", booktitle = "{PCSFW}: Proceedings of The 12th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "1999", url = "citeseer.nj.nec.com/211930.html" } @inproceedings{SC00, author = "Paul F. Syverson and Iliano Cervesato", title = "The Logic of Authentication Protocols", booktitle = "{FOSAD}", pages = "63-136", year = "2000", url = "citeseer.nj.nec.com/455968.html" } @InProceedings{RG97, author = {A.~W.~Roscoe and M.~H.~Goldsmith}, title = {The perfect ``Spy'' for Model-Checking Cryptoprotocols}, booktitle = {DIMACS workshop on Design and Formal Verification of Security Protocols}, OPTpages = {}, year = {1997}, editor = {C. Meadows and H. Orman}, url = {dimacs.rutgers.edu/Workshops/Security/program2/goldsmith.ps} } @article{HvB99, author = "A. Hafid and G. von Bochmann", title = "An Approach to Quality of Service Management in Distributed Multimedia Application: Design and an Implementation", journal = "Multimedia Tools and Applications", volume = "9", number = "2", pages = "167-191", year = "1999", url = "citeseer.nj.nec.com/hafid95approach.html" } @inproceedings{CM96, author = "J. Callahan and T. Montgomery", title = "An Approach to Verification and Validation of a Reliable Multicasting Protocol", booktitle = "International Symposium on Software Testing and Analysis", pages = "187-194", year = "1996", url = "citeseer.nj.nec.com/callahan96approach.html" } @misc{Sto00, author = "S. Stoller", title = "A bound on attacks on authentication protocols", text = "S. D. Stoller. A bound on attacks on authentication protocols. Indiana University, Computer Science Dept, Technical Report 526, February 2000.", year = "2000", url = "citeseer.nj.nec.com/stoller00bound.html", annote = "uses strand spaces and disallows nested encryptions (\cite{HS00})"} @inproceedings{HS00, author = "J. Heather and S. Schneider", title = "Towards Automatic Verification of Authentication Protocols on an Unbounded Network", booktitle = "Proc. 13th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "2000", url = "citeseer.nj.nec.com/279495.html" } @inproceedings{OO94, author = {T. Okamoto and K. Ohta}, title = {How to simultaneously exchange secrets by general assumptions}, booktitle = {Proc. 2nd ACM Conference on Computer and communications security}, year = {1994}, pages = {184--192}, url = {www.acm.org/pubs/toc/}} @Article{EGL85, author = "S. Even and O. Goldreich and A. Lempel", title = "A randomized protocol for signing contracts", journal = "Communications of the ACM", volume = "28", number = "6", pages = "637--647", year = "1985", ISSN = "0001-0782", url = "http://www.acm.org/pubs/toc/", keywords = "security; theory; verification", review = "ACM CR 8512-1137", subject = "{\bf E.3}: Data, DATA ENCRYPTION, Data encryption standard (DES). {\bf E.3}: Data, DATA ENCRYPTION, Public key cryptosystems. {\bf C.2.2}: Computer Systems Organization, COMPUTER-COMMUNICATION NETWORKS, Network Protocols. {\bf H.4.3}: Information Systems, INFORMATION SYSTEMS APPLICATIONS, Communications Applications, Electronic mail. {\bf J.1}: Computer Applications, ADMINISTRATIVE DATA PROCESSING, Financial." } @Article{Dam94, author = "I. B. Damgard", title = "Practical and provably secure release of a secret and exchange of signatures", journal = "Lecture Notes in Computer Science", volume = "765", pages = "200--217", year = "1994", annote = {http://link.springer.de/link/service/series/0558/bibs/0765/07650200.htm, full version appeared in Journal of Cryptology, Volume 8 Volume 8, Number 4, 1995} } @InProceedings{Cle89, title = "Controlled Gradual Disclosure Schemes for Random Bits and Their Applications", author = "Richard Cleve", pages = "573--588", booktitle = "Advances in Cryptology---{CRYPTO}~'89", editor = "G. Brassard", series = "Lecture Notes in Computer Science", volume = "435", year = "1989", publisher = "Springer-Verlag", annote = {http://link.springer.de/link/service/series/0558/bibs/0435/04350573.htm}, abstract = "We construct a protocol that enables a secret bit to be revealed gradually in a very controlled manner. In particular, if Alice possesses a bit S that was generated randomly according to the uniform distribution and 1/2 $<$ p(subscript 1) $<$ ... $<$ p(subscript m) = 1 then, using our protocol with Bob, Alice can achieve the following. The protocol consists of m stages and after the i-th stage, Bob's best prediction of S, based on all his interactions with Alice, is correct with probability exactly p(subscript i) (and a reasonable condition is satisfied in the case where S is not initially uniform). Furthermore, under an intractabilility assumption, our protocol can be made {"}oblivious{"} to Alice and {"}secure{"} against an Alice or Bob that might try to cheat in various ways. Previous proposed gradual disclosure schemes for single bits release information in a less controlled manner: the probabilities that represent Bob's confidence of his knowledge of S follow a random walk that eventually drifts towards 1, rather that a predetermined sequence of values. $<$P$>$Using controlled gradual disclosure schemes, we show how to construct an improved version of the protocol proposed by Luby, Micali and Rackoff for two-party secret bit exchanging ({"}How to Simultaneously Exchange a Secret Bit by Flipping a Symmetrically-Biased Coin,{"} Proc. 22nd Ann. IEEE Symp. on Foundations of Computer Science, 1983, pp. 11-21) that is secure against additional kinds of attacks that the previous protocol is not secure against. Also, our protocol is more efficient in the number of rounds that it requires to attain a given level of security, and is proven to be asymptotically optimal in this respect. $<$P$>$We also show how to use controlled gradual disclosure schemes to improve existing protocols for other cryptographic problems, such as multi-party function evaluation." } @InProceedings{SM00, author = "V. Shmatikov and J. Mitchell", title = "Analysis of a Fair Exchange Protocol", annote = "Analysis of \cite{ASW98} as a case study of formalizing fairness. Finds some (minor) flaws in protocols (e.g., regarding replay); mostly a question of an appearant lack of precise enough definitions of what constitutes contract is in \cite{ASW98}.", pages = "119--128", booktitle = "Proc. Symposium on Network and Distributed Systems Security ({NDSS} '00)", year = "2000", organization = "Internet Society"} @InProceedings{ASW98, author = "N. Asokan and V. Shoup and M. Waidner", title = "Asynchronous Protocols for Optimistic Fair Exchange", booktitle = "Proceedings of the {IEEE} Symposium on Research in Security and Privacy", year = "1998", organization = "{IEEE} Computer Society, Technical Committee on Security and Privacy", publisher = "{IEEE} Computer Society Press", address = "Oakland, CA", pages = "86--99", note = "A minor bug in the proceedings version was fixed. An errata sheet, distributed at the conference, is available at \url{http://www.zurich.ibm.com/Technology/Security/publications/1998/ASW98-errata.ps.gz}; A related paper~\cite{AS98} is available as well", url = {http://citeseer.nj.nec.com/10944.html} } @InProceedings{AB02, author = {Mart{\'\i}n Abadi and Bruno Blanchet}, title = {Analyzing {S}ecurity {P}rotocols with {S}ecrecy {T}ypes and {L}ogic {P}rograms}, booktitle = {29th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002)}, pages = {33--44}, year = {2002}, address = {Portland, Oregon}, publisher = {ACM Press}, url = {http://www.di.ens.fr/~blanchet/publications.html} } @InProceedings{MS01, author = {J. Millen and V. Shmatikov}, title = {Constraint Solving for Bounded-Process Cryptographic Protocol Analysis}, booktitle = {Proc. 2001 ACM Conference on Computer and Communication Security}, pages = {166 - 175}, year = 2001, publisher = {ACM press}, url = {http://www.csl.sri.com/users/shmat/ and citeseer.nj.nec.com/449378.html}} @InProceedings{Hui99, author = {A. Huima}, title = {Efficient Infinite-State Analysis of Security Protocols}, booktitle = {Proc.\ Workshop Formal Methods and Security Protocols (FLOC 1999)}, OPTpages = {}, year = {1999}, OPTeditor = {}, url = "citeseer.nj.nec.com/huima99efficient.html" } @Unpublished{casrul, author = {Y. Chevalier and F.\ Jacquemard and M.\ Rusinowitch and M.\ Turuani and L. Vigneron}, title = {{CASRUL} Web Site}, note = {{\tt http://www.loria.fr/equipes/protheo/SOFTWARES/CASRUL/}} } @inproceedings{Ros98, author = "A.\ W.\ Roscoe", title = "Proving Security Protocols with Model Checkers by Data Independence Techniques", booktitle = "Proc. 11th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "1998", url = "citeseer.nj.nec.com/roscoe98proving.html" } @InProceedings{MMS97, author = "J. C. Mitchell and M. Mitchell and U. Stern", title = "Automated Analysis of Cryptographic Protocols Using Mur$\phi$", pages = "141--153", booktitle = "Proceedings of the 1997 Conference on Security and Privacy", publisher = "IEEE Press", year = "1997" } @InProceedings{RT01, author = {M. Rusinowitch and M. Turuani}, title = {Protocol Insecurity with Finite Number of Sessions is NP-complete}, booktitle = {Proc.\ 14th IEEE Computer Security Foundations Workshop}, year = {2001}, editor = {S. Schneider}} @InProceedings{JRV00, author = "F. Jacquemard and M. Rusinowitch and L. Vigneron", title = "Compiling and Verifying Security Protocols", booktitle = "Proc.\ LPAR: International Conference on Logic for Programming and Automated Reasoning", editor = {M.~Parigot and A.~Vonkorov}, series = {LNCS}, number = {1995}, publisher = {Springer-Verlag}, year = "2000", } @InProceedings{Bla01, author = {B. Blanchet}, title = {An Efficient Cryptographic Protocol Verifier Based on Prolog Rules}, booktitle = {Proc.\ 14th IEEE Computer Security Foundations Workshop}, year = {2001}, editor = {S. Schneider}} @InProceedings{DLMS99, author = {N. Durgin and P. Lincoln and J. Mitchell and A. Scedrov}, title = {Undecidability of bounded security protocols}, booktitle = {Proc. Workshop on Formal Methods and Security Protocols (FMSP'99) (part of FLOC99)}, year = {1999}, note = {http://www.cs.bell-labs.com/who/nch/fmsp99/program.html} } @Unpublished{CJ96, author = "John Clark and Jeremy Jacob", title = "{A Survey of Authentication Protocol Literature}", year = "1996"} @InProceedings{KR01, author = {S.\ Kremer and J-F. Raskin}, title = {A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols}, booktitle = {Proc.\ Concur'01, 12th International Conference of Concurrency Theory}, pages = {551--565}, year = {2001}, editor = {K. G. Larsen and M. Nielsen}, number = {2154}, series = {LNCS}, publisher = {Springer-Verlag}, OPTnote = {full version available at: http://www.ulb.ac.be/di/scsi/skremer/} } @inproceedings{Sch98, author = "S. Schneider", title = "Formal Analysis of a Non-Repudiation Protocol", booktitle = "{PCSFW}: Proc.\ 11th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", pages = "54--65", year = "1998", url = "citeseer.nj.nec.com/schneider98formal.html", OPTnote = downloaded } @inproceedings{Sch97-csf, author = "S. Schneider", title = "Verifying Authentication Protocols with {CSP}", booktitle = "{PCSFW}: Proceedings of The 10th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "1997", url = "citeseer.nj.nec.com/196196.html" } @incollection{And96, author = "R. Anderson", title = "Why Cryptosystems Fail, from Communications of the {ACM}, November, 1994", booktitle = "William Stallings, Practical Cryptography for Data Internetworks, {IEEE} Computer Society Press, 1996", year = "1996", url = "citeseer.nj.nec.com/anderson94why.html"} @InProceedings{AB01fossacs, author = {M. Abadi and B. Blanchet}, title = {Secrecy Types for Asymmetric Communication}, booktitle = {Proc.\ Foundation of Software Science and Coputation Structures (FoSSacS 2001)}, pages = {25--41}, year = {2001}, editor = {F. Honsel and M. Miculan}, volume = {2030}, series = {LNCS}, publisher = {Springer-Verlag}} @Article{AM01, author = {L. C. Aiello and F. Massacci}, title = {Verifying Security Protocols as Planning in Logic Programming}, journal = {Transactions on Computational Logic}, year = {2001}, annote = {to appear} } @Inproceedings{Bas99, author = {D.\ Basin}, title = {Lazy Infinite-State Analysis of Security Protocols}, booktitle = {Secure Networking - CQRE (Secure) '99, International Exhibition and Congress}, pages = {30--42}, year = {1999}, editor = {R.~Baumgart}, volume = {1740}, series = {LNCS}, publisher = {Springer-Verlag}} @Article{BAN90, author = "M. Burrows and M. Abadi and R. Needham", journal = "ACM Transactions on Computer Systems", number = "1", pages = "18--36", title = "A Logic of Authentication", volume = "8", year = "1990", keywords = "Security and Authentication", abstract = "Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been extremely error prone. Most the protocols found in the literature contain redundancies or security flaws. A simple logic has allowed us to describe the beliefs of trustworthy parties involved in authentication protocols and the evolution of these beliefs as a consequence of communication. We have been able to explain a variety of authentication protocols formally, to discover subtleties and errors in them, and to suggest improvements. In this paper, we present the logic and then give the results of our analysis of four published protocols, chosen either because of their practical importance or because they serve to illustrate our method.", url = "http://julmara.ce.chalmers.se/Security/SRC-039.ps.gz", appendix = "SRC-039-appendix.ps.gz", } @InProceedings{BDM01, author = "M. Bozzano and G. Delzanno and M. Martelli", title = "A bottom-up semantics for linear logic programs.", pages = "92--102", booktitle = "Proc.\ Second International {ACM} {SIGPLAN} Conference on Principles and Practice of Declarative Programming ({PPDP}-00)", publisher = "ACM Press", year = "2000", editor = {M. Gabbrielli and F. Pfenning} } @TechReport{BDM01techrep, author = {M. Bozzano and G. Delzanno and M. Martelli}, title = {An Effective Bottom-Up Semantics for First Order Linear Logic Programs and its Relationship with Decidability Results for Timed Petri Nets}, institution = {University of Genova}, year = {2001}, number = {DISI-TR-01-01}} @InProceedings{Boz01, author = {M. Bozzano}, title = {Ensuring Security Through Model Checking in a Logical Environment (Preliminary Results)}, booktitle = save01, year = {2001}, editor = edsave01} @InProceedings{Del01, author = {G. Delzanno}, title = {Specifying and Debugging Security Protocols via Hereditary Harrop Formulas and lambda Prolog - A Case Study}, booktitle = {Proc.\ 5th International Symposium on Functional and Logic Programming}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2001}, pages = "123--137", editor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } } @InProceedings{BMM99, author = {S Brackin and C. Meadows and J.~K.~Millen}, title = {{CAPSL} interface for the {NRL} protocol analyzer}, booktitle = {Proc.\ IEEE Symposium on Application-Specific Systems and Software Engineering Technology (ASSET '99)}, year = 1999 } @InProceedings{BP98, author = "G. Bella and L. C. Paulson", title = "Kerberos Version {IV}: Inductive Analysis of the Secrecy Goals", editor = "J.-J. Quisquater", pages = "361--375", booktitle = "Proc.\ 5th European Symposium on Research in Computer Security", year = 1998, publisher = "Springer-Verlag LNCS 1485", address = "Louvain-la-Neuve, Belgium", urlps = "http://www.cl.cam.ac.uk/users/lcp/papers/Bella/esorics98.ps.gz" } @Unpublished{CAPSL00, author = {J.~K.~Millen}, title = {{CAPSL} Web Site}, year = 2000, note = {{\tt http://www.csl.sri.com/\~{}millen/capsl}} } @InProceedings{CDLMS99, author = "I. Cervesato and N. Durgin and P. Lincoln and J. Mitchell and A. Scedrov", title = "A Meta-Notation for Protocol Analysis", booktitle = "PCSFW: Proc.\ 12th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "1999", pages= "55-69" } @InProceedings{CDLMS00, author = "I. Cervesato and N. Durgin and J. Mitchell and Lincoln and A. Scedrov", title = "Relating Strands and Multiset Rewriting for Security Protocol Analysis", booktitle = "PCSFW: Proc.\ 13th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "2000" } @Article{DY83, author = "D. Dolev and A. C. Yao", title = "On the Security of Public Key Protocols", pages = "198--208", year = "1983", added-at = "Mon Sep 4 10:48:30 2000", annote = "Founding paper on formalizing cryptographic protocols with an algebraic approach (e.g., $D(E(m))=m$, perfect encryption, protocol modeled as string of concatenated messages, reduceable by above term-rewriting rules). Considers secure message transmission protocols. Cascade (only messages and E/D) and Name-stamp (also containing names) protocols. Journal-version of \cite{DolYao81}", volume = "29", number = "2", journal = "{IEEE} Transactions on Information Theory", } @TechReport{DE01-techrep, author = {G. Delzanno and S. Etalle}, title = {A Proof Theoretic Analysis of Security Protocols}, institution = {Dipartimento di Informatica e Scienze dell'Informazione, Universit\`a di Genova}, year = {2001}, number = {DISI-TR-01-08}, note = {{http://www.cs.utwente.nl/\~{}etalle}}} @InProceedings{DE02, author = {G. Delzanno and S. Etalle}, title = {Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols}, booktitle = {Proc.\ Eleventh International Workshop on Logic Program Synthesis and Transformation -- LOPSTR 2001}, year = 2002, editor = {A.\ Pettorossi}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{DE01, author = {G. Delzanno and S. Etalle}, title = {Combining Proof Theoretical Analysis, Transformations and Logic Programming for Debugging Security Protocols}, booktitle = {Proc.\ Eleventh International Workshop on Logic Program Synthesis and Transformation -- LOPSTR 2001}, OPTpages = {}, year = {2002}, editor = {A.\ Pettorossi}, OPTvolume = {}, OPTnumber = {}, series = {LNCS}, publisher = {Springer-Verlag} } @Article{Lowe95, author = "G. Lowe", title = "An attack on the {Needham-Schroeder} public-key authentication protocol", journal = "Information Processing Letters", volume = "56", number = "3", pages = "131--133", day = "10", month = nov, year = "1995", coden = "IFPLAT", ISSN = "0020-0190", bibdate = "Wed Nov 11 12:16:26 MST 1998", acknowledgement = ack-nhfb, classification = "C5640 (Protocols); C6130S (Data security); C6150N (Distributed systems software); C6155 (Computer communications software)", corpsource = "Comput. Lab., Oxford Univ., UK", keywords = "access protocols; agent impersonation; attack; authorisation; computer hacking; impersonate; intruder; Needham-Schroeder public-key authentication protocol; public key cryptography", treatment = "P Practical", } @Article{Lowe96, author = "G. Lowe", title ="Breaking and Fixing the {N}eedham-{S}chroeder Public-Key Protocol using {FDR}", journal = "Software Concepts and Tools", number = 17, pages = "93--102", year = 1996} @Article{Lowe98, title="Towards a Completeness Result for Model Checking of Security Protocols", author = {G. Lowe}, journal = {Journal of Computer Security}, volume= {7}, number={2-3}, pages={89--146}, year ={1998}} @InProceedings{Lowe96b, author = "G. Lowe", title = "Breaking and Fixing the {N}eedham-{S}chroeder Public-Key Protocol Using {FDR}", editor = "T. Margaria and B. Steffen", booktitle = "Proc.\ TACAS: Tools and Algorithms for the Construction and Analysis of Systems", series = "LNCS", publisher = "Springer-Verlag", volume = "1055", year = "1996", ISBN = "3-540-61042-1", pages = "147--166"} @InProceedings{Lowe97, author = "G. Lowe", title = "Casper: {A} Compiler for the Analysis of Security Protocols", pages = "18--30", booktitle = "Proc.\ 10th {IEEE} Computer Security Foundations Workshop ({CSFW} '97)", ISBN = "0-8186-7990-5", publisher = "IEEE", year = "1997"} @Article{MCF97, title = "The {I}nterrogator: Protocol Security Analysis", author = "J. K. Millen and S. C. Clark and S. B. Freedman", pages = "274--288", journal = "IEEE Transactions on Software Engineering", ISSN = "0098-5589", year = 1987, volume = 13, month = "February", number = 2, referencedby = "\cite{1997:tse:lowe}", note = "Special Issue on Computer Security and Privacy", annote = "incomplete", } @InProceedings{Mea94, author = "C. Meadows", title = "Formal Verification of Cryptographic Protocols: {A} Survey", pages = "133--150", url = "http://www.itd.nrl.navy.mil/ITD/5540/publications/CHACS/1995meadows-asiacrypt94.ps", booktitle = "Advances in Cryptology -- {ASIA\-CRYPT} ' 94", year = "1995", editor = "J. Pieprzyk and R. Safavi-Naini", series = "LNCS", publisher = "Springer-Verlag" } @Article{Mea96, author = "C. Meadows", title = "The {NRL} Protocol Analyzer: An Overview", pages = "113--131", year = "1996", url = "http://www.itd.nrl.navy.mil/ITD/5540/publications/CHACS/1995meadows-toappearJLP.ps", volume = "26", number = "2", journal = "Journal of Logic Programming" } @InProceedings{Mea96a, author = "C Meadows", year = "1996", title = "Analyzing the {N}eedham-{S}chroeder Public Key Protocol: {A} Comparison of Two Approaches", booktitle = "Proc.\ ESORICS 96", editor = {E.\ Bertino and H.\ Kurth and G.\ Martella and E.\ Montolivo}, pages = "351--364", series = {LNCS}, number = {1146}, publisher = "Springer Verlag", abstract = "In this paper we contrast the use of the NRL Protocol Analyzer and Gavin Lowe's use of the model checker FDR [8] to analyze the Needham-Schroeder public-key protocol. This is used as a basis for comparing and contrasting the two systems and to point out possible future directions for research.", } @InProceedings{Mea00, author = "Catherine Meadows", title = "Open Issues in Formal Methods for Cryptographic Protocol Analysis", pages = "237--250", year = "2000", abstract = "The history of the application of formal methods to cryptographic protocol analysis spans nearly twenty years, and recently has been showing signs of new maturity and consolidation. A number of specialized tools have been developed, and others have effectively demonstrated that existing general-purpose tools can also be applied to these problems with good results. However, with this better understanding of the field comes new problems that strain against the limits of the existing tools. In this paper we will outline some of these new problem areas, and describe what new research needs to be done to to meet the challenges posed.", url = "http://chacs.nrl.navy.mil/publications/CHACS/2000/2000meadows-discex.ps", booktitle = "{DISCEX 2000}", publisher = "{IEEE} Computer Society Press", } @InProceedings{Mil97, author = "J. K. Millen", title = "{CAPSL}: Common Authentication Protocol Specification Language", pages = "132--133", ISBN = "0-89791-944-0", booktitle = "Proc.\ Workshop on New Security Paradigms", publisher = "ACM Press", address = "New York", year = "1997"} @InProceedings{Mil99, title = "A Necessarily Parallel Attack", author = "J.~K.~Millen", booktitle = "Proc.\ Workshop on Formal Methods and Security Protocols, Part of the Federated Logic Conference", editor = "N.~Heintze and E.~Clarke", year = {1999}, note = {available at: http://www.cs.bell-labs.com/who/nch/fmsp99/program.html}} @Article{Mil96, author = "D. Miller", title = "Forum: A Multiple-Conclusion Specification Logic", journal = "TCS", volume = "165", number = "1", pages = "201--232", year = "1996" } @Article{NS78, author = "R. M. Needham and M. D. Schroeder", title = "Using Encryption for Authentication in Large Networks of Computers", journal = "Communications of the ACM", volume = "21", number = "12", pages = "993--999", year = "1978", coden = "CACMA2", ISSN = "0001-0782", bibdate = "Tue Mar 25 13:26:09 MST 1997", abstract = "Use of encryption to achieve authenticated communication in computer networks is discussed. Example protocols are presented for the establishment of authenticated connections, for the management of authenticated mail, and for signature verification and document integrity guarantee. Both conventional and public-key encryption algorithms are considered as the basis for protocols.", acknowledgement = ack-nhfb, classcodes = "C5620 (Computer networks and techniques); C6130 (Data handling techniques)", classification = "723", corpsource = "Xerox Palo Alto Res. Center, Palo Alto, CA, USA", journalabr = "Commun ACM", keywords = "authenticated communication; computer networks; data processing --- Security of Data; document integrity; encryption; guarantee; protocols; public key encryption algorithms; security of data; signature verification", treatment = "P Practical", } @Article{Pau98, author = "L. C. Paulson", title = "The Inductive Approach to Verifying Cryptographic Protocols", journal = "Journal of Computer Security", year = "1998", volume = "6", pages = "85--128", keywords = "Isabelle", urlps = "http://www.cl.cam.ac.uk/ftp/papers/reports/TR443-lcp-Inductive-Approach-to-Verifying-Cryptographic-Protocols.ps.gz", } @TechReport{Pau97, author = "L. C. Paulson", title = "Mechanized Proofs of Security Protocols: {Needham-Schroeder} with Public Keys", institution = "University of Cambridge, Computer Laboratory", year = "1997", number = "413", month = {January} } @InProceedings{SM93, author = "P. Syverson and C. Meadows", title = "A Logical Language for Specifying Cryptographic Protocol Requirements", pages = "165--177", booktitle = "Proc.\ 1993 {IEEE} Computer Society Symposium on Security and Privacy ({SSP} '93)", ISBN = "0-8186-3370-0", publisher = "IEEE", year = "1993" } @inproceedings{ZG98, author = "J. Zhou and D. Gollmann", title = "Towards verification of non-repudiation protocols", booktitle={Proc.\ 1998 International Refinement Workshop and Formal Methods Pacific}, pages={370--380}, year = "1998", url = "citeseer.nj.nec.com/article/zhou98towards.html" } @inproceedings{ZG96, author = "J. Zhou and D. Gollmann", title = "A Fair Non-repudiation Protocol", booktitle = "Proc.\ {IEEE} Symposium on Research in Security and Privacy", publisher = "IEEE Computer Society Press", address = "Oakland, CA", pages = "55--61", year = "1996", url = "citeseer.nj.nec.com/62704.html" } @article{ZG97, author = "J. Zhou and D. Gollmann", title = "Evidence and non-repudiation", journal = "Journal of Network and Computer Applications", year = "1997", url = "citeseer.nj.nec.com/zhou97evidence.html" }