% file sandro.bib % coi dettami di Apt % intanto le abbreviazioni coniate dai pisani %NOTE @string{cwinote = "Available via anonymous ftp at ftp.cwi.nl, or at http://www.cwi.nl/cwi/publications/index.html"} % %CONFERENCES @string{alp94 = "Proc. Fourth Int'l Conf. on Algebraic and Logic Programming" } @string{edalp94 = "G. Levi and M. Rodr\'iguez-Artalejo" } @string{iclp84 = "Proc. Second Int'l Conf. on Logic Programming" } @string{iclp86 = "Proc. Third Int'l Conf. on Logic Programming"} @string{iclp87 = "Proc. Fourth Int'l Conf. on Logic Programming"} @string{iclp88 = "Proc. Fifth Int'l Conf. on Logic Programming"} @string{iclp89 = "Proc. Sixth Int'l Conf. on Logic Programming"} @string{iclp90 = "Proc. Seventh Int'l Conf. on Logic Programming"} @string{iclp91 = "Proc. Eighth Int'l Conf. on Logic Programming"} @string{iclp93 = "Proc. Tenth Int'l Conf. on Logic Programming"} @string{iclp94 = "Proc. Eleventh Int'l Conf. on Logic Programming"} @string{iclp95 = "Proc. Twelfth Int'l Conf. on Logic Programming"} @string{ediclp84 = {Sten-\AA~ke T\"{a}rnlund}} @string{ediclp86 = "E. Y. Shapiro"} @string{ediclp87 = "J.-L. Lassez"} @string{ediclp88 = "R. A. Kowalski and K. A. Bowen"} @string{ediclp89 = "G. Levi and M. Martelli"} @string{ediclp90 = "D. H. D. Warren and P. Szeredi"} @string{ediclp91 = "K. Furukawa"} @string{ediclp93 = "D.S. Warren"} @string{ediclp94 = "P. van Hentenryck"} @string{ediclp95 = "L. Sterling"} @string{jicslp92 = "Proc. Joint International Conference and Symposium on Logic Programming"} @string{edjicslp92 = "K.~R.~Apt"} @string{cl2000 ="First International Conf. on Computational Logic (CL2000)"} @string{edcl2000 = "J. Lloyd et.\ al."} @string{ijcai97 = "Fifteenth International Joint Conference on Artificial Intelligence"} @string{edijcai97 = "Martha Pollack"} @string{fgcs88 = "Proc. Int'l Conf. on Fifth Generation Computer Systems"} @string{gulp89="Proc. Fourth Italian Conference on Logic Programming"} @string{edgulp89="P. Mello"} @string{gulp90="Proc. Fifth Italian Conference on Logic Programming"} @string{edgulp90="A. Bossi"} @string{gulp91="Proc. Sixth Italian Conference on Logic Programming"} @string{edgulp91="P. Asirelli"} @string{gulpro94="Proc. 1994 Joint Conference on Declarative Progrmming GULP-PRODE'94"} @string{edgulpro94="M. Alpuente"} @string{lics87 = "Proc. Second IEEE Symp. on Logic In Computer Science"} @string{lics88 = "Proc. Third IEEE Symp. on Logic In Computer Science"} @string{lics89 = "Proc. Fourth IEEE Symp. on Logic In Computer Science"} @string{lics91 = "Proc. Sixth IEEE Symp. on Logic In Computer Science"} @string{lopstr91 = "Proc. First Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr91 ="T. Clement and K.-K. Lau"} @string{lopstr93 = "Proc. Thirs Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr93 ="Y. Deville"} @string{lopstr94 = "Proc. Fourth Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr94 ="F. Turini"} @string{lopstr96 = "Proc. Sixth Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr96 ="J. Gallagher"} @string{vollopstr96 = 1207} @string{lopstr97 = "Proc. Seventh Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr97 ="R. Fuchs"} @string{vollopstr97 = 1463} @string{lopstr98 = "Proc. Eighth Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr98 ="P. Flener"} @string{vollopstr98 = 1559} @string{lopstr99 = "Proc. Ninth Workshop on Logic Program Synthesis and Transformation"} @string{edlopstr99 ="A. Bossi"} @string{meta94 = "Proc. Fourth International Workshop on Meta Programming in Logic"} @string{edmeta94 ="F. Turini"} @string{naclp89 = "Proc. North American Conf. on Logic Programming'89"} @string{ednaclp89 = "E. Lusk and R. Overbeck"} @string{naclp90 = "Proc. North American Conf. on Logic Programming'90"} @string{ednaclp90 = "S. Debray and M. Hermenegildo"} @string{plilp91 = "Proc. Third Int'l Symp. on Programming Language Implementation and Logic Programming"} @string{plilp96 = "Proc. 8th Int'l Symp. on Programming Languages: Implementations, Logics and Programs"} @string{popl87 = "Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages"} @string{popl88 = "Proc. Fiftheenth Annual ACM Symp. on Principles of Programming Languages"} @string{popl89 = "Proc. Sixteenth Annual ACM Symp. on Principles of Programming Languages"} @string{popl90 = "Proc. Seventeenth Annual ACM Symp. on Principles of Programming Languages"} @string{popl91 = "Proc. Eighteenth Annual ACM Symp. on Principles of Programming Languages"} @string{popl92 = "Proc. Nineteenth Annual ACM Symp. on Principles of Programming Languages"} @string{popl93 = "Proc. 20th Annual ACM Symposium on Principles of Programming Languages"} @string{popl94 = "Proc. 21st Annual ACM Symp. on Principles of Programming Languages"} @string{slp84 = "Proc. First IEEE Int'l Symp. on Logic Programming"} @string{slp85 = "Proc. Second IEEE Int'l Symp. on Logic Programming"} @string{slp86 = "Proc. Third IEEE Int'l Symp. on Logic Programming"} @string{slp87 = "Proc. Fourth IEEE Int'l Symp. on Logic Programming"} @string{edtapsoft87 = "H. Ehrig, R. Kowalski, G. Levi and U. Montanari"} @string{tapsoft91 = "Proc. TAPSOFT'91"} @string{edtapsoft91=" S. Abramsky and T. Maibaum"} @string{edplilp96="H. Kuchen and S.Doaitse Swierstra"} @string{ilps93 = "Proc. Tenth International Logic Programming Symposium"} @string{edilps93 = "D.~Miller"} @string{ilps94 = "Proc. Eleventh International Logic Programming Symposium"} @string{edilps94 = "M. Bruynooghe"} @string{ilps95 = "Proc. Twelfth International Logic Programming Symposium"} @string{edilps95 = "J. Lloyd"} @string{tppp94 = "Proc. 1994 Int. Workshop on Theory and Practice of Parallel Programming"} @string{edtppp94 = "T. Ito and A. Yonezawa"} @string{voltppp94 = "907"} @string{cp97 = "Third International Conference on Principles and Practice of Constraint Programming (CP97)"} @string{edcp97 = "G. Smolka"} @string{volcp97 = "1330"} %INSTITUTIONS @string{cwi = "CWI, Centre for {M}athematics and {C}omputer {S}cience, Amsterdam, The Netherlands"} @string{dip = "Dipartimento di Informatica, Universit\`{a} di Pisa"} @string{icot = "Institute for New Generation Computer Technology, Tokyo"} %JOURNALS @string{i&c = "Information and Computation"} @string{jacm = "Journal of the ACM"} @string{jlc = "Journal of Logic and Computation"} @string{jlp = "Journal of Logic Programming"} @string{JSC = "Journal of Symbolic Computation"} @string{JLP = "Journal of Logic Programming" } @string{tcs = "Theoretical Computer Science"} @string{toplas = "ACM Transactions on Programming Languages and Systems"} @string{tplp = "Theory and Practice of Logic Programming"} %PUBLISHERS @string{csp = "Computer Science Press, New York"} @string{lnai = "Lecture Notes in Artificial Intelligence"} @string{lncs = "Lecture Notes in Computer Science"} @string{mit = "The MIT Press, Cambridge, Mass."} @string{springer = " Springer-Verlag, Berlin"} @string{addison = " Addison-Wesley"} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % poi la abbreviazioni di nostra.bib % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Journals, books, and series @STRING{AI = "Artificial Intelligence"} @STRING{Acta = "Acta Informatica"} @STRING{CACM = "Communications of the {ACM}"} @STRING{CJ = "Computer Journal"} @STRING{ESOP = "European Symposium on Programming"} @STRING{FPCA = "International Conference on Functional Programming Languages and Computer Architecture"} @STRING{IFIP = "IFIP World Congress Proceedings"} @STRING{IPL = "Information Processing Letters"} @STRING{JACM = "Journal of the {ACM}"} @STRING{JCSS = "Journal of Computer and System Sciences"} @STRING{JFP = "Journal of Functional Programming"} @STRING{LASC = "Lisp and Symbolic Computation"} @STRING{LFP = "{ACM} Conference on Lisp and Functional Programming"} @STRING{LICS = "{IEEE} Symposium on Logic in Computer Science"} @STRING{LNCS = "Lecture Notes in Computer Science"} @STRING{MFCS = "Mathematical Foundations of Computer Science"} @STRING{MFPLS = "Mathematical Foundations of Programming Language Semantics"} @STRING{NGC = "New Generation Computing"} @STRING{PEMC = "Partial Evaluation and Mixed Computation"} @STRING{PEPM = "Partial Evaluation and Semantics-Based Program Manipulation, New Haven, Connecticut. (Sigplan Notices, vol. 26, no. 9, September 1991)"} @STRING{PDO = "Programs as Data Objects, Copenhagen, Denmark. (Lecture Notes in Computer Science, vol. 217)"} @STRING{POPL = "ACM Symposium on Principles of Programming Languages"} @STRING{SCP = "Science of Computer Programming"} @STRING{SIGPLAN = "Sigplan Notices"} @STRING{SMD = "Soviet Mathematics Doklady"} @STRING{SPE = "Software -- Practice and Experience"} @STRING{TCS = "Theoretical Computer Science"} @STRING{TOPLAS = "ACM Transactions on Programming Languages and Systems"} @STRING{TSE = "IEEE Transactions on Software Engineering"} Publishers @STRING{A-W = "Addison-Wesley"} @STRING{AP = "Academic Press"} @STRING{CSP = "Computer Science Press"} @STRING{CUP = "Cambridge University Press"} @STRING{JWS = "John Wiley \& Sons"} @STRING{MIT = "MIT Press"} @STRING{N-H = "North-Holland"} @STRING{OUP = "Oxford University Press"} @STRING{P-H = "Prentice-Hall"} @STRING{S-V = "Springer-Verlag"} @STRING{SL = "Studentlitteratur, Lund, Sweden"} @STRING{WHF = "W.H. Freeman"} Institutions and people @STRING{BEJ = "D. Bj{\o}rner and A.P. Ershov and N.D. Jones"} @STRING{CCN = "Computing Center, No\-vo\-si\-birsk, USSR"} @STRING{CTH = "Chalmers University of Technology"} @STRING{DIKU = "DIKU, University of Copenhagen, Denmark"} @STRING{ISI = "Informatics Systems Institute, Novosibirsk, USSR"} @STRING{PMG = "Programming Methodology Group, Chalmers University of Technology"} @STRING{UPMAIL = "UPMAIL, Uppsala University, Sweden"} @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"} @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"} @Article{Lam04, author = {B. Lampson}, title = {Computer Security in the Real World}, journal = {IEEE Computer}, year = {2004}, volume = {37}, number = {6}, pages = {37--46}, month = {June} } %$# TO BE PROCESSED @article{LST87, author = {J. W. Lloyd and L. Sonenberg and R. W. Topor}, title = {Integrity Constraint Checking in Stratified Databases}, journal = {Journal of Logic Programing}, volume = {4}, number = {4}, year = {1987}, pages = {331-343}, PUBLISHER = {Elsevier Science}, bibsource = {DBLP, http://dblp.uni-trier.de} } % WE HAVE THIS ALREADY @article{LT86, author = {John W. Lloyd and Rodney W. Topor}, title = {A Basis for Deductive Database Systems II}, @article{DBLP:journals/jlp/LloydT85, author = {J. W. Lloyd and R. W. Topor}, title = {A Basis for Deductive Database Systems}, journal = {Journal of Logic Programing}, volume = {2}, number = {2}, year = {1985}, pages = {93-109}, PUBLISHER = {Elsevier Science}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{KSS87, author = {R. Kowalski and F. Sadri and P. Soper}, title = {Integrity Checking in Deductive Databases}, booktitle = {VLDB'87, Proceedings of 13th International Conference on Very Large Data Bases}, editor = {P. M. Stocker and W. Kent and P. Hammersley}, publisher = {Morgan Kaufmann}, year = {1987}, pages = {61-69} } @inproceedings{Oli91, author = {A. Oliv\'{e}}, title = {Integrity Constraints Checking In Deductive Databases}, booktitle = {VLDB '91: Proceedings of the 17th International Conference on Very Large Data Bases}, year = {1991}, pages = {513--523}, publisher = {Morgan Kaufmann} } @inproceedings{EPS04, author = {I. Elkabani and E. Pontelli and T. C. Son}, title = {Smodels with CLP and Its Applications: A Simple and Effective Approach to Aggregates in ASP.}, booktitle = {ICLP}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3132}, year = {2004}, pages = {73-89}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3132{\&}spage=73}, crossref = {DBLP:conf/iclp/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{PSE04, author = {E. Pontelli and T. C. Son and I. Elkabani}, title = {Smodels with CLP - A Treatment of Aggregates in ASP.}, booktitle = {LPNMR}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2923}, year = {2004}, pages = {356-360}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2923{\&}spage=356}, crossref = {DBLP:conf/lpnmr/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inbook{Gam88, author = "D. Gambetta", title = "Can We Trust Trust?", editor = "D. Gambetta", booktitle = {Trust: Making and Breaking Cooperative Relations}, publisher= "Basil Blackwell", year = "1988", note = {Reprinted in electronic edition from Department of Sociology, University of Oxford, chapter 13, pp. 213-237}, } %$# NEWINPUT @inproceedings{DFI+03, author = {T. Dell'Armi and W. Faber and G. Ielpa and N. Leone and G. Pfeifer}, title = {Aggregate Functions in DLV.}, booktitle = {Answer Set Programming}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, volume = {78}, year = {2003}, pages = {274-288}, ee = {http://SunSITE.Informatik.RWTH-Aachen.de/Publications/CEUR-WS//Vol-78/asp03-final-dellarmi.pdf}, crossref = {DBLP:conf/asp/2003}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DPR03, author = {A. Dovier and E. Pontelli and G. Rossi}, title = {Intensional Sets in CLP.}, booktitle = {ICLP}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2916}, year = {2003}, pages = {284-299}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2916{\&}spage=284}, crossref = {DBLP:conf/iclp/2003}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{KS91, author = {D.~B.~Kemp and P.~J.~Stuckey}, title = {Semantics of Logic Programs with Aggregates.}, booktitle = {ISLP}, publisher = {MIT Press}, year = {1991}, pages = {387-401}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{GL91, author = {M. Gelfond and V. Lifschitz}, title = {{Classical Negation in Logic Programs and Disjunctive Databases.}}, journal = {New Generation Computing}, publisher = {{Verlag Omsha}}, volume = {9}, number = {3/4}, year = {1991}, pages = {365-386}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{NS97, author = {I. Niemel and P. Simons}, title = {Smodels - An Implementation of the Stable Model and Well-Founded Semantics for Normal LP}, booktitle = {LPNMR '97: Proc.\ of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning}, year = {1997}, isbn = {3-540-63255-7}, pages = {421--430}, publisher = {Springer-Verlag}, } @inproceedings{CW93, author = {W. Chen and D. S. Warren}, title = {Query evaluation under the well-founded semantics}, booktitle = {{PODS '93: Proc.\ of the twelfth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems}}, year = {1993}, isbn = {0-89791-593-3}, pages = {168--179}, location = {Washington, D.C., United States}, doi = {http://doi.acm.org/10.1145/153850.153865}, publisher = {ACM Press} } @inproceedings{SSW94, author = {K. Sagonas and T. Swift and D. S. Warren}, title = {{XSB as an efficient deductive database engine}}, booktitle = {{SIGMOD '94: Proc.\ of the 1994 ACM SIGMOD international conference on Management of data}}, year = {1994}, isbn = {0-89791-639-5}, pages = {442--453}, location = {Minneapolis, Minnesota, United States}, doi = {http://doi.acm.org/10.1145/191839.191927}, publisher = {ACM Press} } @article{LT86, author = {J. W. Lloyd and R. W. Topor}, title = {A Basis for Deductive Database Systems II.}, journal = {Journal of Logic Programming}, publisher = {Elsevier Science}, volume = {3}, number = {1}, year = {1986}, pages = {55-67}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{GNY90, author = "L. Gong and R. Needham and R. Yahalom", title = "{Reasoning About Belief in Cryptographic Protocols}", booktitle = "Proceedings 1990 {IEEE} Symposium on Research in Security and Privacy", publisher = "IEEE Computer Society Press", pages = "234--248", year = "1990", url = "citeseer.ist.psu.edu/gong90reasoning.html" } %$# @article{BDGS04, author = {D. Balfanz and G. Durfee and R. E. Grinter and D. K. Smetters}, title = {In Search of Usable Security: Five Lessons from the Field}, journal = {IEEE Journal on Security and Privacy}, volume = {2}, number = {5}, pages = {19-24}, month = {Sep}, year = {2004}, url = {http://doi.ieeecomputersociety.org/10.1109/MSP.2004.71 }} @article{SM03, author = {A. Sabelfled and A. C. Meyers}, title = {{Language-Based} {Information-Flow} security}, journal = {IEEE Journal on Selected Areas in Communications}, volume = {21}, number = {1}, pages = {5-19}, month = {Jan}, year = {2003}, url = {http://doi.ieeecomputersociety.org/10.1109/JSAC.2002.806121}} @InProceedings{YWS05, author = {C. Yao and W. H. Winsborough and S. Jajodia}, title = {A hierarchical release control policy framework}, booktitle = {Proc. IFIP TC-11 WG 11.1 & WG 11.5 Joint Working Conference on Security Management, Integrity, and Internal Control in Information Systems}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTorganization = {}, OPTpublisher = {} } @MISC{SHTZ06, TITLE = {Managing Policy Updates in Security-Typed Languages}, AUTHOR = {N. Swamy and M. Hicks and S. Tse and S. Zdancewic}, NOTE = {Submitted for publication}, MONTH = {February}, url ={http://www.cs.umd.edu/~mwh/papers/swamy06rx.html}, YEAR = 2006 } @article{Sam06, author = {P. Samuelson}, title = {Regulating technical design}, journal = {Commun. ACM}, volume = {49}, number = {2}, year = {2006}, pages = {25--30}, doi = {http://doi.acm.org/10.1145/1113034.1113057}, publisher = {ACM Press} } @InProceedings{HV04, author = {J. I. den Hartog and E. P. de Vink}, title = {Virtual Analysis and Reduction of Side-Channel Vulnerabilities of Smartcards}, pages = {85--98}, booktitle = {2ndt Int. Workshop on Formal Aspect of Security and Trust ({FAST})}, publisher = {Springer Verlag}, series = {IFIP International Federation for Information Processing}, number = {173}, editor = {T.\ Dimitrakos and F.\ Martinelli}, year = {2004} } @Misc{drmblog, OPTauthor = {}, OPTtitle = {}, howpublished = {www.drmblog.com}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @inproceedings{CB04, author = {B. Chun and A. Bavier}, title = {Decentralized Trust Management and Accountability in Federated Systems.}, booktitle = {37th Hawaii International Conference on System Sciences (HICSS-37 2004)}, year = {2004}, editor = {G. Agha}, ee = {http://csdl.computer.org/comp/proceedings/hicss/2004/2056/09/205690279aabs.htm}, publisher = {IEEE} } @article{Lin92a, author = {P. Lincoln}, title = {Linear logic}, journal = {SIGACT News}, volume = {23}, number = {2}, pages = {29-37}, year = {1992}, url = {http://doi.acm.org/10.1145/130956.130958}, annote = {ISSN 0163-5700}} @techreport{Bra96a, author = {T. Bra{\"u}ner}, title = {Introduction to Linear Logic}, institution = {Dept. of Comp. Sci, Aarhus Univ, Denmark}, type = {BRICS Lecture Series}, number = {LS-96-6}, month = {Dec}, year = {1996}, url = {http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf}} @InProceedings{GWW01, author = {C. Gunter and S. Weeks and A. Wright}, title = {Models and Languages for Digital Rights}, booktitle = {Proceedings of the 34th Annual Hawaii International Conference on System Sciences (HICSS-34)}, year = {2001}, publisher = {IEEE Computer Society Press}, pages = {4034--4038} } @InProceedings{Guo01, author = {H. Guo}, title = {Digital Rights Management ({DRM}) Using {XrML}}, booktitle = {T-110.501 Seminar on Network Security 2001}, year = {2001}, annote = {ISBN 951-22-5807-2}, pages = {Poster paper 4}, url = {http://www.tml.hut.fi/Studies/T-110.501/2001/papers/} } \InProceedings{WL02policy, author = {W. H. Winsborough and N. Li}, title = {Towards Practical Automated Trust Negotiation.}, booktitle = {POLICY}, publisher = {IEEE Computer Society Press}, year = {2002}, pages = {92-103} } @inproceedings{PGE+05, author = {J.A. Pouwelse and P. Garbacki and D.H.J. Epema and H.J. Sips}, title = {The {B}ittorrent {P2P} {F}ile-sharing {S}ystem: {M}easurements and {A}nalysis}, booktitle = {Proc.\ of the 4th International Workshop on Peer-to-Peer Systems (IPTPS05)}, editor = {M. Castro and R. van Renesse}, year = {2005}, pages = {205-216}, ee = {http://dx.doi.org/10.1007/11558989_19}, publisher = {Springer}, series = {LNCS}, volume = {3640} } @PhdThesis{Li00, author = {N. Li}, title = {Delegation Logic: A Logic-Based Approach to Distributed Authorization}, school = {New York University}, year = {2000} } @PhdThesis{Dam02, author = {N.C. Damianou}, title = {A Policy Framework for Management of Distributed Systems}, school = {Imperial College of Science, Technology and Medicine, University of London}, year = {2002}, url = {http://www-dse.doc.ic.ac.uk/Research/policies/ponder/thesis-ncd.pdf} } @InProceedings{GMM+04, author = {P. Giorgini and F. Massacci and J. Mylopoulos and N. Zannone}, title = {{Filling the gap between Requirements Engineering and Public Key/Trust Management Infrastructures}}, booktitle = {Proc.\ 1st European PKI Workshop: Research and Applications (1st EuroPKI)}, series = {LNCS}, volume = {3093}, pages = {98--111}, publisher = {Springer-Verlag}, month = {June}, year = {2004} } %$# THE FOLLOWING ONES ARE PROCESSED ALREADY @article{EFL+00, author = {T. Eiter and W. Faber and N. Leone and G. Pfeifer}, title = {Declarative problem-solving using the {DLV} system}, book = {Logic-based artificial intelligence}, year = {2000}, isbn = {0-7923-7224-7}, pages = {79--103}, publisher = {Kluwer Academic Publishers} } @InProceedings{VRD+01, author = {P. Vora and D. Reynolds and I. Dickinson and J. Erickson and D. Banks}, title = {Privacy and Digital Rights Management}, booktitle = {Proc. W3C workshop on Digital Rights Management}, year = {2001} } @inproceedings{MHB03, author = {D. K. Mulligan and J. Han and A. J. Burstein}, title = {How DRM-based content delivery systems disrupt expectations of "personal use"}, booktitle = {DRM '03: Proceedings of the 3rd ACM workshop on Digital rights management}, year = {2003}, isbn = {1-58113-786-9}, pages = {77--89}, location = {Washington, DC, USA}, doi = {http://doi.acm.org/10.1145/947380.947391}, publisher = {ACM Press} } @article{Eri03, author = {J. S. Erickson}, title = {Fair use, DRM, and trusted computing}, journal = {Commun. ACM}, volume = {46}, number = {4}, year = {2003}, issn = {0001-0782}, pages = {34--39}, doi = {http://doi.acm.org/10.1145/641205.641228}, publisher = {ACM Press} } @article{Coh03, author = {Julie E. Cohen}, title = {DRM and privacy}, journal = {Commun. ACM}, volume = {46}, number = {4}, year = {2003}, issn = {0001-0782}, pages = {46--49}, doi = {http://doi.acm.org/10.1145/641205.641230}, publisher = {ACM Press}} @article{Dus03, author = {S. Dusollier}, title = {Fair use by design in the European copyright directive of 2001}, journal = {Commun. ACM}, volume = {46}, number = {4}, year = {2003}, issn = {0001-0782}, pages = {51--55}, doi = {http://doi.acm.org/10.1145/641205.641231}, publisher = {ACM Press} } @article{Fel03, author = {E. Felten}, title = {A skeptical view of DRM and fair use}, journal = {Commun. ACM}, volume = {46}, number = {4}, year = {2003}, issn = {0001-0782}, pages = {56--59}, doi = {http://doi.acm.org/10.1145/641205.641232}, publisher = {ACM Press}} @inproceedings{CNS04, author = {M. Carbone and M. Nielsen and V. Sassone}, title = {A Calculus for Trust Management.}, editor = {K. Lodaya and M. Mahajan}, booktitle = {Proc. 24th Int. Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS)}, year = {2004}, pages = {161-173} } @article{Lam77, author = {L. Lamport}, title = {Proving the Correctness of Multiprocess Programs.}, journal = {IEEE Trans. Software Eng.}, volume = {3}, number = {2}, year = {1977}, pages = {125-143}} @InProceedings{GM82, author = "J. Goguen and J. Meseguer", title = "Security policies and security models", booktitle = "Proc. IEEE Symposium on Security and Privacy", publisher = "IEEE Computer Society Press", pages = "11--20", year = "1982"} @inproceedings{ZPPS04, author = {X. Zhang and J. Park and F. Parisi-Presicce and R. Sandhu}, title = {A logical specification for usage control}, booktitle = {SACMAT '04: Proceedings of the ninth ACM symposium on Access control models and technologies}, year = {2004}, isbn = {1-58113-872-5}, pages = {1--10}, editor = {E. Ferrari}, publisher = {ACM Press} } @inproceedings{MAG04, author = {M. McDougall and R. Alur and C. Gunter}, title = {A model-based approach to integrating security policies for embedded devices}, editor = {G. Buttazzo}, booktitle = {Proc. ACM International Conference On Embedded Software (EMSOFT)}, year = {2004}, pages = {211-219}, publisher = {ACM Press} } @article{AG02, author = {V. Atluri and A. Gal}, title = {An authorization model for temporal and derived data: securing information portals.}, journal = {ACM Trans. Inf. Syst. Secur.}, volume = {5}, number = {1}, year = {2002}, pages = {62-94} } @inproceedings{GA00, author = {A. Gal and V. Atluri}, title = {An authorization model for temporal data.}, booktitle = {ACM Conference on Computer and Communications Security}, year = {2000}, pages = {144-153}, publisher = {ACM Press} } @inproceedings{SCZ03, author = {F. Siewe and A. Cau and H. Zedan}, title = {A compositional framework for access control policies enforcement}, booktitle = {FMSE '03: Proceedings of the 2003 ACM workshop on Formal methods in security engineering}, year = {2003}, isbn = {1-58113-781-8}, pages = {32--42}, location = {Washington, D.C.}, doi = {http://doi.acm.org/10.1145/1035429.1035433}, publisher = {ACM Press}, address = {New York, NY, USA}, } @article{BBFS98, author = {E. Bertino and C. Bettini and E. Ferrari and P. Samarati}, title = {An access control model supporting periodicity constraints and temporal reasoning}, journal = {ACM Trans. Database Syst.}, volume = {23}, number = {3}, year = {1998}, issn = {0362-5915}, pages = {231--285}, doi = {http://doi.acm.org/10.1145/293910.293151}, publisher = {ACM Press} } @InProceedings{HBP05, author = {M. Hilty and D. Basin and A. Pretschner}, title = {On Obligations}, booktitle = {Proc.\ 10th European Symposium On Research In Computer Security (ESORICS)}, editor = {S. De Capitani di Vimercati and P. Syverson and D. Gollmann}, publisher = {Springer}, series = {LNCS}, pages = {98-117}, year = {2005} } @article{Sch00, author = {F. B. Schneider}, title = {Enforceable security policies}, journal = {ACM Trans. Inf. Syst. Secur.}, volume = {3}, number = {1}, year = {2000}, issn = {1094-9224}, pages = {30--50}, doi = {http://doi.acm.org/10.1145/353323.353382}, publisher = {ACM Press} } @inproceedings{YMW00, author = {T. Yu and X. Ma and M. Winslett}, title = {PRUNES: an efficient and complete strategy for automated trust negotiation over the Internet.}, booktitle = {ACM Conference on Computer and Communications Security (CCS)}, year = {2000}, pages = {210-219}, publisher = {ACM Press} } @article{JPLI99, author = {T. Jaeger and A. Prakash and J. Liedtke and N. Islam}, title = {Flexible Control of Downloaded Executable Content.}, journal = {ACM Trans. Inf. Syst. Secur.}, volume = {2}, number = {2}, year = {1999}, pages = {177-228} } @inproceedings{HJM02, author = {A. Hess and J. Jacobson and H. Mills and R. Wamsley and K. E. Seamons and B. Smith}, title = {Advanced Client/Server Authentication in TLS.}, booktitle = {Proc. of the Network and Distributed System Security Symposium, (NDSS 2002)}, year = {2002}, ee = {http://www.isoc.org/isoc/conferences/ndss/02/proceedings/papers/hess.pdf}, publisher = {The Internet Society} } @inproceedings{WL02, author = {W. H. Winsborough and N. Li}, title = {Protecting sensitive attributes in automated trust negotiation.}, booktitle = {Proc ACM Workshop on Privacy in the Electronic Society, WPES 2002}, year = {2002}, pages = {41-51}, ee = {http://doi.acm.org/10.1145/644532}, publisher = {ACM press} } @inproceedings{JMT98, author = {W.\ Johnston and S.\ Mudumbai and M.\ Thompson}, title = {Authorization and Attribute Certificates for Widely Distributed Access Control.}, booktitle = {Proc: 7th Workshop on Enabling Technologies (WETICE '98), Infrastructure for Collaborative Enterprises}, year = {1998}, pages = {340-345}, ee = {http://dlib2.computer.org/conferen/wetice/8751/pdf/87510340.pdf?}, publisher = {IEEE Computer Society}} @Book{Zim94, author = {P. Zimmerman}, title = {PGP User's guide}, publisher = {MIT Press}, year = {1994} } @Misc{spki, author = {IETF}, title = {Simple Public-Key Infrastructure (SPKI)}, howpublished = {IETF}, year = {2001} } @Misc{x509, author = {IETF}, title = {Public-Key Infrastructure (X.509)}, howpublished = {IETF}, year = {2002} } @inproceedings{PCT05, author = {B. Popescu and B. Crispo and A. Tanenbaum}, title = {Support for Multi-Level Security Policies in DRM Architectures}, booktitle = {Proc. 13th New Security Paradigms Workshop}, year = {2005}, isbn = {1-59593-076-0}, pages = {3--9}, doi = {http://doi.acm.org/10.1145/1065907.1065909}, publisher = {ACM Press}, abstract = {We propose a paradigm shift - moving from the original DRM system model where all devices are equally trustworthy and have discretionary control over all protected content, to a new model where in- formation ow is controlled through a multi-level security policy that differentiates between devices based on their tamper-resistance properties. We show that besides im- proved intrusion-tolerance, supporting such policies has other advantages, such as the ability to define more exible busi- ness models for supplying content. The paradigm currently pondered when designing DRM architectures is that compliant devices can be indiscriminately assumed as part of the trusted computing base (TCB) of the system and given discretionary access to all protected content. In this paper we show that when a DRM system comprises devices with different tamper-resistance proper- ties, following the above paradigm is bad security practice, because it goes against the basic principle of least privilege, making the overall intrusion-resistance of the system to be}} @inproceedings{PKCT04, author = {B. Popescu and F. Kamperman and B. Crispo and A. Tanenbaum}, title = {A DRM security architecture for home networks}, booktitle = {DRM '04: Proceedings of the 4th ACM workshop on Digital rights management}, year = {2004}, isbn = {1-58113-969-1}, pages = {1--10}, location = {Washington DC, USA}, doi = {http://doi.acm.org/10.1145/1029146.1029150}, publisher = {ACM Press}, abstract = {This paper describes a security architecture al- lowing digital rights management in home net- works consisting of consumer electronic devices. The idea is to allow devices to establish dynamic groups, so called "Authorized Domains", where legally acquired copyrighted content can seamlessly move from device to device. This greatly improves the end-user experience, preserves "fair use" ex- pectations, and enables the development of new business models by content providers. Key to our design is a hybrid compliance checking and group establishment protocol, based on pre-distributed symmetric keys, with minimal reliance on pub- lic key cryptographic operations. Our architecture does not require continuous network connectivity between devices, and allows for efficient and ex- ible key updating and revocation}} @Article{RZFK00, author = {P. Resnick and R. Zeckhauser and E. Friedman and K. Kuwabara}, title = {Reputation Systems}, journal = {Communication of the ACM}, year = {2000}, volume = {43}, number = {12}, pages = {45-48} } @Article{LABW92, author = {B. Lampson and M. Abadi and M. Burrows and E. Wobber}, title = {Authentication in Distributed Systems: Theory and Practice}, journal = {ACM Transactions on Computer Systems}, year = {1992}, volume = {10}, number = {2}, pages = {265-310}, publisher = {ACM Press} } @article{BFS04, author = {E. Bertino and E. Ferrari and A. C. Squicciarini}, title = {Trust-X: A Peer-to-Peer Framework for Trust Establishment.}, journal = {IEEE Trans. Knowl. Data Eng.}, volume = {16}, number = {7}, year = {2004}, pages = {827-842}, publisher = {IEEE Computer Society Press}, ee = {http://csdl.computer.org/comp/trans/tk/2004/07/k0827abs.htm}} @article{Avi04, author = {A. Avizienis and J.-C. Laprie and B. Randell and C. Landwehr}, title = {Basic Concepts and Taxonomy of Dependable and Secure Computing}, journal = {IEEE Transactions on Dependable and Secure Computing}, volume = {1}, number = {1}, pages = {11-33}, month = {Jan}, year = {2004}, url = {http://doi.ieeecomputersociety.org/10.1109/TDSC.2004.2 }} @article{SBL+04, author = {S. Staab and B. Bhargava and L. Lilien and A. Rosenthal and M. Winslett and M. Sloman and T. Dillon and E. Chang and F. Hussain and W. Nejdl and D. Olmedilla and V. Kashyap}, title = {The Pudding of Trust}, journal = {IEEE Intelligent Systems}, volume = {19}, number = {5}, year = {2004}, issn = {1094-7167}, pages = {74--88}, doi = {http://dx.doi.org/10.1109/MIS.2004.52}, publisher = {IEEE Educational Activities Department}, address = {Piscataway, NJ, USA}, } @inproceedings{KSG03, author = {S. Kamvar and M. Schlosser and H. Garcia-Molina}, title = {The Eigentrust algorithm for reputation management in P2P networks}, booktitle = {WWW '03: Proceedings of the 12th international conference on World Wide Web}, year = {2003}, editor = {Y Robin Chen and L. Kov\'acs and S. Lawrence}, isbn = {1-58113-680-3}, pages = {640--651}, location = {Budapest, Hungary}, doi = {http://doi.acm.org/10.1145/775152.775242}, publisher = {ACM Press} } @inproceedings{CNSS04, author = {P-A. Chirita and W. Nejdl and M. Schlosser and O. Scurtu}, title = {Personalized Reputation Management in P2P Networks.}, booktitle = {ISWC Workshop on Trust, Security, and Reputation on the Semantic Web}, editor = {J. Golbeck and P. Bonatti and W. Nejdl and D. Olmedilla and M. Winslett}, year = {2004}, ee = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-127/paper4.pdf}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, volume = {127} } @inproceedings{GS02, author = {T. Grandison and M. Sloman}, title = {Specifying and Analysing Trust for Internet Applications.}, booktitle = {I3E '02: Proceedings of the IFIP Conference on Towards The Knowledge Society}, editor = {J. Monteiro and P. Swatman and L. Valadares Tavares}, year = {2002}, pages = {145-157} } @Article{GS00, author = {T. Grandison and M. Sloman}, title = {A Survey of Trust in Internet Applications}, journal = {IEEE Communications and Surveys}, year = {2000}, volume = {3}, number = {4}, OPTpages = {}, publisher = {IEEE Computer Society} } @inproceedings{AD01, author = {K. Aberer and Z. Despotovic}, title = {Managing trust in a peer-2-peer information system}, booktitle = {Proc. tenth international conference on Information and knowledge management (CIKM '01)}, editor = {D. Grossman and L. Liu}, year = {2001}, isbn = {1-58113-436-3}, pages = {310--317}, doi = {http://doi.acm.org/10.1145/502585.502638}, publisher = {ACM Press} } @inproceedings{AH05, author = {A. Abdul-Rahman and S. Hailes}, title = {Supporting Trust in Virtual Communities}, booktitle = {HICSS '00: Proc. 33rd Hawaii International Conference on System Sciences-Volume 6}, year = {2000}, isbn = {0-7695-0493-0}, pages = {6007}, publisher = {IEEE Computer Society}, } @Article{CKS05, author = {R.\ Chadha and S.\teve Kremer and A.\ Scedrov}, title = {Formal Analysis of Multi-Party Contract Signing}, journal = {Journal of Automated Reasoning}, year = {2005}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, note = {To appear} } @InProceedings{BDOS05, author = {P. Bonatti and C. Duma and D. Olmedilla and N. Shahmehri}, title = {An Integration of Reputation-based and Policy-based Trust Management}, booktitle = {Proc. 2005 Semantic Web and Policy Workshop}, OPTpages = {}, year = {2005}, editor = {L. Kagal and T. Finin and J. Hendler}, note = {available at http://cs.na.infn.it/rewerse/} } @article{YWS03, author = {T. Yu and M. Winslett and K. E. Seamons}, title = {Supporting structured credentials and sensitive policies through interoperable strategies for automated trust negotiation}, journal = {ACM Trans. Inf. Syst. Secur.}, volume = {6}, number = {1}, year = {2003}, issn = {1094-9224}, pages = {1--42}, doi = {http://doi.acm.org/10.1145/605434.605435}, publisher = {ACM Press} } @InProceedings{RSS+97, author = {P. Rao and K. F. Sagonas and T. Swift and D. S. Warren and J. Freire}, title = {XSB: A System for Efficiently Computing Well-Founded Semantics}, booktitle = {Proc. 4th International Conference on Logic Programming and Non-Monotonic Reasoning (LPNMR'97)}, series = {LNAI}, volume = {1265}, pages = {2--17}, year = {1997}, editor = {J. Dix and U. Furbach and A. Nerode}, publisher = {Springer-Verlag}} @InProceedings{Tho97, author = {R.\ K.\ Thomas}, title = {{Team-based access control (TMAC): a primitive for applying role-based access controls in collaborative environments}}, booktitle = {Proc.\ 2nd ACM workshop on Role-based access control}, pages = {13-19}, year = {1997}, publisher = {ACM Press}, } @InProceedings{GMP+01, author = {C.K. Georgiadis and I. Mavridis and G. Pangalos and R.K. Thomas}, title = {{Flexible team-based access control using contexts}}, booktitle = {Proc.\ 6th ACM symposium on Access control models and technologies}, pages = {21-27}, year = {2001}, publisher = {ACM Press} } @InProceedings{CTW+02, author = {E. Cohen and R.K. Thomas and W. Winsborough and D. Shands}, title = {{Models for coalition-based access control (CBAC)}}, booktitle = {Proc.\ 7th ACM symposium on Access control models and technologies}, pages = {97-106}, year = {2002}, publisher = {ACM Press} } @article{LLR05, author = {S. Lahlou and M. Langheinrich and C. R{\"o}cker}, title = {Privacy and trust issues with invisible computers}, journal = {Commun. ACM}, volume = {48}, number = {3}, pages = {59-60}, year = {2005}, url = {http://doi.acm.org/10.1145/1047671.1047705}} @inproceedings{Lan03, author = {M. Langheinrich}, title = {When Trust Does Not Compute - The Role of Trust in Ubiquitous Computing}, booktitle = {Workshop on Privacy at Ubicomp}, publisher = {Unpublished}, address = {Seattle, Washington}, month = {Oct}, year = {2003}, url = {http://www.vs.inf.ethz.ch/publ/papers/ubicomp03-trust.pdf}} @inproceedings{BGR05, author = {L.\ Bauer and S.\ Garriss and M.\ K.\ Reiter}, title = {Distributed Proving in Access-Control Systems}, booktitle = {SP '05: Proc.\ 2005 IEEE Symposium on Security and Privacy}, year = {2005}, isbn = {0-7695-2339-0}, pages = {81--95}, doi = {http://dx.doi.org/10.1109/SP.2005.9}, publisher = {IEEE Computer Society} } @inproceedings{BNO+04, author = {J.\ Basney and W.\ Nejdl and D.\ Olmedilla and V.\ Welch and M.\ Winslett}, title = {Negotiating Trust on the Grid}, booktitle = {2nd Workshop on Semantics in P2P and Grid Computing}, year = 2004, url = {citeseer.ist.psu.edu/article/basney04negotiating.html} } @inproceedings{BIK03, author = {M. Blaze and J. Ioannidis and A. Keromytis}, title = {Experience with the KeyNote Trust Management System: Applications and Future Directions.}, booktitle = {iTrust}, year = {2003}, pages = {284-300}, ee = {http://link.springer.de/link/service/series/0558/bibs/2692/26920284.htm}} @InProceedings{NOW04, author = {W.\ Nejdl and D.\ Olmedilla and M.\ Winslett}, title = {PeerTrust: Automated Trust Negotiation for Peers on the Semantic Web}, editor = {W.\ Jonker and M.\ Petkovic}, booktitle = {VLDB Workshop on Secure Data Management (SDM)}, year = {2004}, pages = {118--132}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3178{\&}spage=118}, publisher = {Springer}, series = {LNCS}, volume = {3178}, isbn = {3-540-22983-3}} @inproceedings{Yao03, author = {W. Yao}, title = {Fidelis: A Policy-Driven Trust Management Framework.}, booktitle = {iTrust}, year = {2003}, pages = {301-317}, ee = {http://link.springer.de/link/service/series/0558/bibs/2692/26920301.htm} } @Misc{BO05:report, author = {P. Bonatti and D. Olmedilla}, title = {Policy Language Specification}, howpublished = {Project Deliverable D2, Working Group I2, EU NoE REWERSE}, year = 2005, note = {http://www.l3s.de/~olmedilla/pub/publications.html}, annote = {trust negotiation} } @InProceedings{BO05, author = {P.\ Bonatti and D.\ Olmedilla}, title = {Driving and Monitoring Provisional Trust Negotiation with Metapolicies}, booktitle = {Proc.\ 6th {IEEE} International Workshop on Policies for Distributed Systems and Networks ({POLICY} 2005)}, address = {Stockholm, Sweden}, pages = {14-23}, year = 2005, annote = {metapolicies, trust negotiation} } @inproceedings{She02a, author = {O. Sheyner and J. W. Haines and S. Jha and R. Lippmann and J. M. Wing}, title = {Automated Generation and Analysis of Attack Graphs}, booktitle = {23rd Symp. on Security and Privacy ({S}\&{P})}, publisher = {IEEE Computer Society}, address = {Berkeley, California}, month = {May}, year = {2002}, pages = {273-284}} @Article{JSS+01, author = {S. Jajodia and P. Samarati and M.L. Sapino and V.S. Subrahmanian}, title = {{Flexible support for Multiple Access Control Policies}}, journal = {ACM Transactions on Database Systems (TODS)}, year = {2001}, volume = {26}, number = {2}, pages = {214-260}, month = {June}, publisher = {ACM Press} } @InProceedings{HMM+00, author = {A. Herzberg and Y. Mass and J. Michaeli and Y. Ravid and D. Naor}, title = {{Access Control Meets Public Key Infrastructure, Or: Assigning Roles to Strangers}}, booktitle = {Proc.\ 2000 IEEE Symposium on Security and Privacy}, pages = {2-14}, year = {2000}, address = {Oakland, CA}, month = {May}, publisher = {IEEE Computer Society Press} } @InProceedings{BCF01, author = {E. Bertino and S. Castano and E. Ferrari}, title = {{On Specifying Security Policies for Web Documents with an XML-based Language}}, booktitle = {Proc.\ 6th ACM symposium on Access control models and technologies}, pages = {57-65}, year = {2001}, address = {Chantilly, Virginia}, month = {May}, publisher = {ACM Press} } @PhdThesis{Li00, author = {N. Li}, title = {Delegation Logic: A Logic-Based Approach to Distributed Authorization}, school = {New York University}, year = {2000} } @PhdThesis{Dam02, author = {N. C. Damianou}, title = {A Policy Framework for Management of Distributed Systems}, school = {Imperial College of Science, Technology and Medicine, University of London}, year = {2002}, url = {http://www-dse.doc.ic.ac.uk/Research/policies/ponder/thesis-ncd.pdf} } @inproceedings{DT04, author = {P.M. Dung and P.M. Thang}, title = {{Trust Negotiation with Nonmonotonic Access Policies}}, booktitle = {Proc.\ IFIP International Conference on Intelligence in Communication Systems (INTELLCOMM 04)}, series = {LNCS}, volume = {3283}, pages = {70-84}, publisher = {Springer}, year = {2004} } @InProceedings{BS00, author = "P.\ Bonatti and P.\ Samarati", title = "Regulating Service Access and Information Release on the Web", booktitle = "Proc.\ 7th ACM Conference on Computer and Communications Security (CCS-7)", publisher = "ACM Press", year = "2000", pages = "134--143" } @INPROCEEDINGS{YWS01, AUTHOR = {T.\ Yu and M.\ Winslett and K.\ Seamons}, TITLE = {Interoperable Strategies in Automated Trust Negotiation}, BOOKTITLE = {Proc.\ 8th ACM Conference on Computer and Communications Security (CCS-8)}, publisher = "ACM Press", pages = "146--155", YEAR = {2001}} @INPROCEEDINGS{SWY01, AUTHOR = {K.\ Seamons and M.\ Winslett and T.\ Yu}, TITLE = "Limiting the Disclosure of Access Control Policies During Automated Trust Negotiation", BOOKTITLE = {Proc.\ Symposium on Network and Distributed System Security (NDSS'01)}, publisher = {The Internet Society}, YEAR = {2001}} @inproceedings{GMMZ04, author = {P. Giorgini and F. Massacci and J. Mylopoulos and N. Zannone}, title = {{Filling the gap between Requirements Engineering and Public Key/Trust Management Infrastructures}}, booktitle = {Proceedings of the 1st European PKI Workshop: Research and Applications (1st EuroPKI)}, series = {LNCS}, volume = {3093}, pages = {98-111}, publisher = {Springer-Verlag Heidelberg}, month = {June}, year = {2004}, } @article{BS03, author = {S. Barker and P. J. Stuckey}, title = {Flexible access control policy specification with constraint logic programming}, journal = {ACM Trans. Information and System Security}, volume = {6}, number = {4}, year = {2003}, issn = {1094-9224}, pages = {501--546}, doi = {http://doi.acm.org/10.1145/950191.950194}, publisher = {ACM Press}, topic = {ac} } @article{Kle00a, author = {J. M. Kleinberg}, title = {Navigation in a small world}, journal = {Nature}, volume = {406}, pages = {845}, month = {Aug}, year = {2000}, url = {http://www.cs.cornell.edu/home/kleinber/nat00.pdf}} @article{Wat98, author = {D. J. Watts and S. H. Strogatz}, title = {Collective dynamics of small-world networks}, journal = {Nature}, volume = {393}, month = {Jun}, year = {1998}, url = {http://tam.cornell.edu/SS_nature_smallworld.pdf}} @InProceedings{CL96, author = {B. Crispo and M. Lomas}, title = {A Certification Scheme for Electronic Commerce}, booktitle = {Proc.\ 1st Security Protocols Workshop}, pages = {19--32}, year = {1996}, editor = {}, number = {1189}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{CR01, author = {B. Crispo and G. Ruffo}, title = {Reasoning about Accountability within Delegation}, booktitle = { Proc.\ 3rd Conference on Information and Communications Security (ICICS'01)}, pages = {251--260}, year = {2001}, editor = {}, number = {2229}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{DB01, author = {G. Delzanno and T. Bultan}, title = {Constraint-Based Verification of Client-Server Protocols}, booktitle = {Proc.\ 7th Conference on Principles and Practice of Constraint Programming (CP'01)}, pages = {286--301}, year = {2002}, OPTeditor = {}, number = {2239}, series = {LNCS}, publisher = {Springer-Verlag}} @Article{BMP03, author = {G. Bella and F. Massacci and L.C. Paulson}, title = {Verifying the SET Registration Protocols}, journal = {IEEE Journal on Selected Areas in Communications}, year = {2003}, volume = {21}, number = {1}, pages = {77-87} } @InProceedings{AdMG01, author = {G. Ateniese and B. de Medeiros and M. T. Goodrich.}, title = {TRICERT: Distributed Certified E-Mail Schemes}, booktitle = {Proc.\ ISOC 2001 Network and Distributed System Security Symposium (NDSS'01)}, pages = {47--56}, year = {2001}, editor = {P. van Oorschot and V. Gligor}, OPTpublisher = {} } @PhdThesis{Aso98, author = {N. Asokan}, title = {Fairness in Electronic Commerce}, school = {University of Waterloo}, year = {1998} } @InProceedings{LF01, author = "N. Li and J. Feigenbaum", title = "Nonmonotonicity, User Interfaces, and Risk Assessment in Certificate Revocation (Position Paper)", booktitle = "Proceedings of the 5th Internation Conference on Financial Cryptography (FC'01)", pages = "166--177", series = "LNCS", number = "2339", publisher = "Springer", year = "2002", annote ={http://crypto.stanford.edu/~ninghui/papers/revocation_fc01.pdf} } @article{ZAC03, author = {L. Zhang and G-J. Ahn and B-T. Chu}, title = {A rule-based framework for role-based delegation and revocation}, journal = {ACM Trans. Information System Security}, volume = {6}, number = {3}, year = {2003}, issn = {1094-9224}, pages = {404--441}, doi = {http://doi.acm.org/10.1145/937527.937530}, publisher = {ACM Press} } @inproceedings{Aba97, author = "M. Abadi", title = "On {SDSI}'s Linked Local Name Spaces", booktitle = "{PCSFW}: Proceedings of The 10th Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", year = "1997", pages = "98-108", url = "citeseer.ist.psu.edu/article/abadi97sdsis.html" } @article{Aba98, author = {M. Abadi}, title = {On SDSI's Linked Local Name Spaces}, journal = {J. Computer Security}, volume = {6}, number = {1-2}, year = {1998}, issn = {0926-227X}, pages = {3--21}, publisher = {IOS Press} } @InProceedings{Li00, author = "N. Li", title = "Local Names in {SPKI/SDSI}", booktitle = "Proc.\ 13th IEEE Computer Security Foundations Workshop", year = "2000", publisher = "IEEE Computer Society Press", pages = "2--15"} @inProceedings{LM03understading, AUTHOR = {N. Li and J. Mitchell}, TITLE = {Understanding SPKI/SDSI Using First-Order Logic}, Booktitle = {Proc. 16th IEEE Computer Security Foundations Workshop}, publisher = "IEEE Computer Society Press", year = "2003", URL = {http://www.cs.purdue.edu/homes/ninghui/papers/sem_spki_j.pdf} } @article{LGF03, author = {N. Li and B. Grosof and J. Feigenbaum}, title = {Delegation logic: A logic-based approach to distributed authorization}, journal = {ACM Trans. Information System Security}, volume = {6}, number = {1}, year = {2003}, issn = {1094-9224}, pages = {128--171}, doi = {http://doi.acm.org/10.1145/605434.605438}, publisher = {ACM Press}, address = {New York, NY, USA} } @InProceedings{LGF00, author = {N. Li and B. Grosof and J. Feigenbaum}, title = "A Practically Implementable and Tractable {Delegation Logic}", booktitle = "Proceedings of the 2000 IEEE Symposium on Security and Privacy", year = "2000", publisher = "IEEE Computer Society Press", pages = "27--42", doi = {http://crypto.stanford.edu/~ninghui/abstracts/dl_oakland00.html} } @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", 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 = {}, OPTpublisher = {} } @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}, year = {1994}} @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 = "Proc. 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} } @InProceedings{AB02, author = {M. Abadi and B. Blanchet}, title = {Analyzing {S}ecurity {P}rotocols with {S}ecrecy {T}ypes and {L}ogic {P}rograms}, booktitle = {Proc.\ 29th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002)}, pages = {33--44}, year = {2002}, 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}} @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{BP01, author = {G. Bella and L. Paulson}, title = {Mechanical Proofs about a Non-Repudiation Protocol}, booktitle = {Proc.\ 14th Conference on Theorem Proving in Higher Order Logics (TPHOLs'01)}, pages = {91--104}, year = {2001}, OPTeditor = {}, number = {2152}, series = {LNCS}, publisher = {Springer-Verlag}} @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" } @article{CW96, author = {W. Chen and D. S. Warren}, title = {Tabled evaluation with delaying for general logic programs}, journal = {Journal of ACM}, volume = {43}, number = {1}, year = {1996}, issn = {0004-5411}, pages = {20--74}, doi = {http://doi.acm.org/10.1145/227595.227597}, publisher = {ACM Press} } @Article{CSW95, author = {W. Chen and T. Swift and D. S. Warren}, title = {Efficient Top-Down Computation of Queries under the Well-Founded Semantics}, journal = {Journal of Logic Programming}, volume = "24", number = "3", pages = "161-199", year = "1995", publisher = {Elsevier}, url = "citeseer.ist.psu.edu/article/chen94efficient.html" } @InProceedings{Wee01, author = "S. Weeks", title = "Understanding Trust Management Systems", booktitle = "Proceedings of 2001 IEEE Symposium on Security and Privacy", year = "2001", publisher = "IEEE Computer Society Press", pages = "94--105"} @Article{SCFY96, author = "R. Sandhu and E. Coyne and H. Feinstein and C. Youman", title = "Role-Based Access Control Models", journal = {IEEE Computer}, year = {1996}, volume = {29}, number = {2}, pages = {38--47}, month = {February}, publisher = "IEEE Computer Society Press" } @Misc{RL96, author = "R. Rivest and B. Lampson", title = "{SDSI} --- A Simple Distributed Security Infrastructure", month = {October}, year = "1996", note = "Available at http://theory.lcs.mit.edu/\ensuremath{\sim}rivest/sdsi11.html.", } @InProceedings{LFG99, author = "Ni. Li and J. Feigenbaum and B. Grosof", title = "A Logic-based Knowledge Representation for Authorization with Delegation (Extended Abstract)", booktitle = "Proceedings of the 1999 IEEE Computer Security Foundations Workshop", publisher = "IEEE Computer Society Press", pages = "162--174", year = "1999"} @InProceedings{Jim01, author = "T. Jim", title = "{SD3}: A Trust Management System with Certified Evaluation", booktitle = "Proceedings of the 2001 IEEE Symposium on Security and Privacy", paddress = "Los Alamitos, CA", month = {May}, year = "2001", publisher = "IEEE Computer Society Press", pages = "106--115"} @article{GJ00, author = "C. Gunter and T. Jim", title = "Policy-directed Certificate Retrieval", journal = "Software: Practice \& Experience", year = "2000", volume = "30", number = "15", pages = "1609--1640", month = {September}, publisher = {Wiley}} @misc{RFC2693, author = "C. Ellison and B. Frantz and B. Lampson and R. Rivest and B. Thomas and T. Ylonen", title = "{SPKI} Certificate Theory", year = "1999", month = {September}, howpublished = "IETF RFC 2693", } @article{CEE+01, author = {D. Clarke and J.E. Elien and C. Ellison and M. Fredette and A. Morcos and R. L. Rivest}, title = {Certificate chain discovery in {SPKI/SDSI}}, journal = {Journal of Computer Security}, pages = {285-322}, volume = {9}, number = {4}, year = {2001}} @article{CEEFMR01, author = "D. Clarke and J-E. Elien and C. Ellison and M. Fredette and A. Morcos and R. Rivest", title = "Certificate Chain Discovery in {SPKI/SDSI}", journal = "Journal of Computer Security", year = "2001", volume = "9", number = "4", publisher = {{IOS Press}}, pages = "285--322", } @InCollection{GGGM98, author = "P. Godfrey and J. Grant and J. Gryz and J. Minker", title = "Integrity Constraints: Semantics and Applications", booktitle = "Logics for Databases and Information Systems", pages = "265-306", editor = {J. Chomicki and G. Saake}, publisher = {Kluwer Academic}, year = {1998}} @Book{Das92, author = {S.~K.~Das}, title = {Deductive Databases and Logic Programming}, publisher = {Addison-Wesley}, year = {1992} } @article{LMW05, author = {N. Li and J. C. Mitchell and W. H. Winsborough}, title = {Beyond proof-of-compliance: security analysis in trust management.}, journal = {J. ACM}, volume = {52}, number = {3}, year = {2005}, pages = {474-514}, ee = {http://doi.acm.org/10.1145/1066103} } @article{LMW04, author = {N. Li and J. C. Mitchell and W. H. Winsborough}, title = {Beyond proof-of-compliance: security analysis in trust management.}, journal = {J. ACM}, volume = {52}, number = {3}, year = {2005}, pages = {474-514}, ee = {http://doi.acm.org/10.1145/1066103} } @InProceedings{WL04, author = {W. Winsborough and N. Li}, title = {Safety in Automated Trust Negotiation.}, booktitle = {Proc. 2004 IEEE Symposium on Security and Privacy}, pages = {147-160}, year = {2004}, publisher = {IEEE Press} } @PhdThesis{Cho05, author = {C. N. Chong}, title = {Experiments in rights control expression and enforcement}, school = {University of Twente - CTIT - 05-68}, year = {2005}, ISSN = {1381-3617} } @inproceedings{Cho03a, author = {C. N. Chong and R. Corin and S. Etalle and P. H. Hartel and W. Jonker and Y. W. Law}, title = {{LicenseScript}: {A} Novel Digital Rights Language and its Semantics}, booktitle = {3rd Int. Conf. on Web Delivering of Music ({WEDELMUSIC})}, editor = {K. Ng and C. Busch and P. Nesi}, publisher = {IEEE Computer Society Press, Los Alamitos, California}, address = {Leeds, UK}, month = {Sep}, year = {2003}, pages = {122-129}, url = {http://www.ub.utwente.nl/webdocs/ctit/1/000000bf.pdf}, annote = {GROUP DIES}, annote = {GROUP DB}, annote = {TOPIC Security}, annote = {PROGRAM ISTRICE}, annote = {PROJECT LicenseScript}, annote = {ISBN 0-7695-1935-0}, annote = {ABSTRACT We propose LicenseScript as a new multiset rewriting/ logic based language for expressing dynamic conditions of use of digital assets such as music, video or private data. LicenseScript differs from other DRM languages in that it caters for the intentional but legal manipulation of data. We believe this feature is the answer to providing the flexibility needed to support emerging usage paradigms of digital data. We provide the language with a simple semantics based on traces.}, annote = {refs}, annote = {inproceedings}} @Misc{p3p, author = {W3C}, title = {A P3P Preference Exchange Language 1.0 (APPEL1.0)}, howpublished = {www.w3.org/TR/P3P-preferences}, year = {2002} } W3C.A P3P Preference Exchange Language 1.0 (APPEL1.0),2002.Available at @InProceedings{Wang02, author = "X. Wang and G. Lao and T. {De Martini} and H. Reddy and M. Nguyen and E. Valenzuela", title = "{XrML}: {eXtensible} rights Markup Language", editor = "M. Kudo", pages = "71--79", booktitle = "Proc. 2002 {ACM} workshop on {XML} security ({XMLSEC}-02)", publisher = "ACM Press", year = "2002" } @Misc{Ian01, author = {R. Iannella}, title = {Open Digital Rights Management}, howpublished = {DRM Workshop, Position Paper 23}, year = {2001}, note = {http://www.w3.org/2000/12/drm-ws/pp/} } @Misc{Ian01, author = {R. Iannella}, title = {Open Digital Rights Management}, howpublished = {DRM Workshop, Position Paper 23}, year = {2001}, note = {http://www.w3.org/2000/12/drm-ws/pp/} } @inproceedings{JSSE97, author = {S. Jajodia and P. Samarati and V. S. Subrahmanian and E. Bertino}, editor = {J. Peckham}, title = {A Unified Framework for Enforcing Multiple Access Control Policies}, booktitle = {SIGMOD 1997, Proc. International Conference on Management of Data}, publisher = {ACM Press}, year = {1997}, pages = {474-485} } @article{CJM00:acm, author = "E.~M.~Clarke and S.~Jha and W.~Marrero", title = "Verifying security protocols with {Brutus}", journal = "ACM Transactions on Software Engineering and Methodology", volume = "9", number = "4", pages = "443--487", year = 2000, } @InProceedings{CJM00:tacas, author = {E.~M.~Clarke and S.~Jha and W.~Marrero}, title = {Partial {O}rder {R}eductions for {S}ecurity {P}rotocol {V}erification}, booktitle = {Proc.~of the International Conference for the Construction and Analysis of Systems -- TACAS 2000}, series = lncs, volume = "1785", pages = "503--518", year = 2000 } @InProceedings{CJM98:fmsp, author = {E.~M.~Clarke and S.~Jha and W.~Marrero}, title = {A {M}achine {C}heckable {L}ogic of {K}nowledge for {P}rotocols}, booktitle = {Proc.~of Workshop on Formal Methods and Security Protocols}, year = 1998 } @InProceedings{CJM98:procomet, author = {E.~M.~Clarke and S.~Jha and W.~Marrero}, title = {Using state space exploration and a natural deduction style message derivation engine to verify security protocols}, booktitle = {Proc.~of IFIP Working Conference on Programming Concepts and Methods (PROCOMET)}, year = 1998 } @ARTICLE{JSSS01, AUTHOR = {S. Jajodia and P. Samarati and {M.L.} Sapino and {V.S.} Subrahmanian}, TITLE = {Flexible Support for Multiple Access Control Policies}, JOURNAL = {ACM Transactions on Database Systems}, YEAR = {2001}, MONTH = {June}, VOLUME = {26}, NUMBER = {2}, PAGES = {214-260} } @Article{VPS03, author = {S. De Capitani di Vimercati and S. Paraboschi and P. Samarati}, title = {Access control: Principles and Solutions}, journal = {Software -- Practice and Experience}, year = {2003}, month = {April}, volume = {33}, number = {5}, pages = {397-421} } @Article{CDM04, author = {A. Chander and D. Dean and J. Mitchell}, title = {Reconstructing Trust Management}, journal = {Journal of Computer Security}, year = {2004}, volume = {12}, number = {1}, pages = {131--164}, month = {January}, note = {http://www.csl.sri.com/users/ddean/papers/jcs04.pdf} } @InProceedings{CDM01, author = "A. Chander and D. Dean and J. Mitchell", title = "A state-transition model of trust management and access control", pages = "27--43", booktitle = "14th {IEEE} Computer Security Foundations Workshop ({CSFW} '01)", ISBN = "0-7695-1146-5", publisher = "IEEE Press", year = "2001", note = "http://citeseer.ist.psu.edu/chander01statetransition.html"} @InProceedings{HRU75, author = "M. Harrison and W. Ruzzo and J. Ullman", title = "On Protection in Operating Systems", boottitle = "ACM symposium on Operating systems principles", year = "1975", pages = "14--24", publisher = "ACM Press"} @Article{HRU76, author = "M. Harrison and W. Ruzzo and J. Ullman", title = "Protection in Operating Systems", journal = "Communications of the ACM", volume = "19", number = "8", year = "1976", pages = "461--471", publisher = "ACM Press"} @InProceedings{GMS04:pet, author = {C.~A.~Gunter and M.~J.~May and S.~G.~Stubblebine}, title = {A Formal Privacy System and its Application to Location Based Services}, booktitle = {4th Workshop on Privacy Enhancing Technologies (PET 2004)}, OPTpages = {}, year = {2004}, editor = {D.\ Martin and A.\ Serjantov}, OPTvolume = {}, OPTnumber = {}, series = {LNCS}, OPTaddress = {Toronto, Canada}, month = {26-28 May}, publisher = {Springer--Verlag}, } @InProceedings{LM03, author = {N. Li and J. C. Mitchell}, title = {DATALOG with Constraints: A Foundation for Trust Management Languages}, booktitle = {5th International Symposium on Practical Aspects of Declarative Languages (PADL'03)}, pages = {58-73}, year = {2003}, editor = {V. Dahl and P. Wadler}, publisher = {Springer-Verlag}, series = {LNCS}, volume = {2562}} @InProceedings{GTCHRS04, author = {J. Guttman, F. Thayer, J. Carlson, J. Herzog, J. Ramsdell, B. Sniffen}, title = {Trust Management in Strand Spaces: A Rely-Guarantee Method}, booktitle = {Proc. 13th European Symposium on Programming, ESOP 2004}, pages = {325--339}, year = {2004}, editor = {D. Schmidt}, volume = {2986}, series = {LNCS}, publisher = {Springer-Verlag}, note = {http://springerlink.metapress.com/link.asp?id=nlf06qug0j79 and http://www.ccs.neu.edu/home/guttman/trust_mgt_in_strands.pdf} } @InProceedings{BFL96, author={M. Blaze and J. Feigenbaum and J. Lacy}, title={Decentralized Trust Management}, booktitle = {Proc.\ 1996 IEEE Symposium on Security and Privacy}, pages = {164-173}, year = {1996}, editor = {IEEE Computer Society Press}} } @misc{RFC2704, author = "M. Blaze and J. Feigenbaum and J. Ioannidis and A. Keromytis", title = "The {KeyNote} Trust-Management System, Version 2", year = "1999", month = sep, howpublished = "IETF RFC 2704", url = "http://www.ietf.org/rfc/rfc2704.txt"} @misc{BFIK99rfc, author = "M. Blaze and J. Feigenbaum and J. Ioannidis and A. Keromytis", title = "The {KeyNote} Trust-Management System, Version 2", year = "1999", howpublished = "IETF RFC 2704", url = "http://www.ietf.org/rfc/rfc2704.txt"} @misc{BFIK99-rfc, author = "M. Blaze and J. Feigenbaum and J. Ioannidis and A. Keromytis", title = "The {KeyNote} Trust-Management System, Version 2", year = "1999", howpublished = "IETF RFC 2704", url = "http://www.ietf.org/rfc/rfc2704.txt"} @InCollection{BFIK99, author = "M. Blaze and J. Feigenbaum and J. Ioannidis and A. Keromytis", title={The Role of Trust Management in Distributed Systems Security}, booktitle={Secure Internet Programming: Security Issues for Mobile and Distributed Objects}, editor = {J.~Vitek and C.~Jensen}, series={LNCS}, volume={1603}, year={1999}, pages={185-210}, publisher={Springer-Verlag} } @incollection{SS97, author={R. Sandhu and P. Samarati}, title={Authentication, Access Control, and Intrusion Detection}, booktitle={The Computer Science and Engineering Handbook}, year={1997}, editor={A. B. Tucker}, publisher={CRC Press}, pages={1929-1948} } @article{BF02, author={E. Bertino and E. Ferrari}, title={Secure and selective dissemination of XML documents}, journal={ACM Transactions on Information and System Security (TISSEC)}, year={2002}, publisher={ACM press}, pages={290-331} } @article{BCFP03, author={E. Bertino and B. Catania and E. Ferrari and P. Perlasca}, title={A logical framework for reasoning about access control models}, journal={ACM Transactions on Information and System Security (TISSEC)}, year={2003}, publisher={ACM press}, pages={71-127} } @techreport{AHPS03, author={P. Ashley and S. Hada and C. Powers and M. Schunter}, title={Enterprise Privacy Authorization Language (EPAL)}, institution={IBM Research}, year={2003}, number={3485} } @inproceedings{AHKS02, author = {P.~Ashley and S.~Hada and G.~Karjoth and M.~Schunter}, title = {E-P3P privacy policies and privacy authorization}, booktitle = {Proc.~of the ACM workshop on Privacy in the Electronic Society (WPES 2002)}, year = {2002}, pages = {103--109}, publisher = {ACM Press}} @InProceedings{PW04, author = {R. Pucella and V. Weissman}, title = {A Formal Foundation for ODRL}, booktitle = {Proc. Workshop on Issues in the Theory of Security (WITS)}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2004}, editor = {P. Ryan}} @InProceedings{PW02, title = "A Logic for Reasoning about Digital Rights", author = "R. Pucella and V. Weissman", year = "2002", booktitle = {Proc. 15th IEEE Computer Security Foundations Workshop}, OPTcrossref = {}, OPTkey = {}, pages = {282--294}, OPTeditor = {}, OPTorganization = {}, OPTpublisher = {}, URL = "http://arXiv.org/abs/cs/0405066", } @article{SS94, author = "R. Sandhu and P. Samarati", title = "Access Control: Principles and Practice", journal = "IEEE Communications Magazine", volume = "32", number = "9", pages = "40--48", year = "1994", url = "citeseer.ist.psu.edu/article/sandhu94access.html" } @inproceedings{SP03, author = "R. Sandhu and J. Park", title = "Usage Control: {A} Vision for Next Generation Access Control", editor = {V. Gorodetsky and L. J. Popyack and V. A. Skormin}, booktitle = {Proc.\ Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security MMM-ACNS}, publisher = {Springer-Verlag}, series = {LNCS}, volume = {2776}, year = {2003} } @InProceedings{PS02, author = "J. Park and R. Sandhu", title = "Towards Usage Control Models: Beyond Traditional Access Control", pages = "57--64", booktitle = "Proc.\ of the Seventh {ACM} Symposium on Access Control Models and Technologies ({SACMAT}-02)", publisher = "ACM Press", year = "2002" } @Article{PS04, author = {J. Park and R. Sandhu}, title = {The {UCON}$_{\mathrm{ABC}}$ Usage Control Model}, journal = {ACM Trans. on Information and System Security}, year = {2004}, volume = {7}, number = {1}, pages = {128-174} } @InProceedings{SS99-anonymity, author = {P. Syverson and S. Stubblebine}, title = {Group Principals and the Formalization of Anonymity}, booktitle = {World Congress on Formal Methods}, pages = {814-833}, year = {1999}, url = "citeseer.ist.psu.edu/syverson99group.html" }} @article{Kai96, author = "R. Kailar", title = "Accountability in Electronic Commerce Protocols", journal = "{IEEE} Transactions on Software Engineering", volume = "22", number = "5", year = "1996", url = "citeseer.nj.nec.com/kailar96accountability.html" } @InProceedings{AF99, author = "A.~W.~Appel and E.~W.~Felten", title = "Proof-Carrying Authentication", editor = "G. Tsudik", booktitle = "Proc of the 6th Conference on Computer and Communications Security", year = "1999", publisher = "ACM Press"} @InProceedings{Aba03, author = {M.~Abadi}, title = {Logic in Access Control}, booktitle = {Proc. 8th Annual IEEE Symposium on Logic in Computer Science (LICS)}, pages = {228-233}, year = {2003}, month = {June}, publisher = {IEEE Computer Society Press} } @Book{Apt03, author = {K.\ R.\ Apt}, title = {Principles of Constraint Programming}, publisher = {cambridge University Press}, year = {2003}} @Book{AF03, author = {S.\ Abdennadher and T.\ Fruehwirth}, title = {Essentials of Constraint Programming}, publisher = {Springer-Verlag}, year = {2003}} @article{ABLP93, author = {M.~Abadi and M.~Burrows and B.~Lampson and G.~Plotkin}, title = {A calculus for access control in distributed systems}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {15}, number = {4}, year = {1993}, issn = {0164-0925}, pages = {706--734}, publisher = {ACM Press} } @InProceedings{DAF02, author = {J. Dai and J. Alves-Foss}, title = {Logic Based Authorization Policy Engineering}, booktitle = {Proc. 6th World Multiconference on Systemics, Cybernetics, and Informatics}, pages = {230--238}, year = {2002}} @Misc{McCul03, author = {D.\ McCullagh}, OPTtitle = {RFID tags: Big Brother in small packages}, howpublished = {CNET NEWS.COM -- http://news.com.com/2010-1069-980325.html}, OPTmonth = {January}, year = {2003} } InProceedings{BJWW02, author = {C. Bettini and S. Jajodia and X. S. Wang and D. Wijesekera}, title = "Provisions and Obligations in Policy Management and Security Applications", editor = "P.\ Bernstein et al.", booktitle = "{VLDP 2002}: proceedings of the Twenty-Eighth International Conference on Very Large Data Bases, Hong Kong {SAR}, China, 20--23 August 2002", publisher = "Morgan Kaufmann", ISBN = "1-55860-869-9", pages = "502--513", year = "2002", URL = "http://www.vldb.org/conf/2002/S14P03.pdf"} @article{BJWW03, author = {C. Bettini and S. Jajodia and X. S. Wang and D. Wijesekera}, title = {Provisions and Obligations in Policy Rule Management}, journal = {J. Network and Systems Management }, volume = {11}, number = {3}, year = {2003}, issn = {1064-7570}, pages = {351--372}, doi = {http://dx.doi.org/10.1023/A:1025711105609}, publisher = {Plenum Press}, address = {New York, NY, USA}, } @InProceedings{BJWW02policy, author = "C.\ Bettini and S.\ Jajodia and X.\ Sean Wang and D.\ Wijesekera", title = {Obligation Monitoring in Policy Management}, booktitle = {3rd IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY'02)}, OPTcrossref = {}, OPTkey = {}, pages = {1-12}, year = {2002}, url = {http://tizero.usr.dico.unimi.it/~bettini/papers/policy02.pdf} } @article{Fol92, author = "S.\ Foley", title = "Aggregation and separation as noninterference properties", journal = {Journal of Computer Security }, year = {1992}, volume = {1}, number = {2}, url = "citeseer.nj.nec.com/foley92aggregation.html" } @Article{LWM03, author = {N.\ Li and W.\ Winsborough and J.\ Mitchell}, title = {Distributed Credential Chain Discovery in Trust Management}, journal = {Journal of Computer Security}, year = {2003}, volume = {11}, number = {1}, publisher = {IOS Press}, pages = {35--86}, comment = "Extended abstract appeared in \emph{Proceedings of the Eighth ACM Conference on Computer and Communications Security}, November 2001."} @InProceedings{LMW02, author = "N.\ Li and J.\ Mitchell and W.\ Winsborough", title = "Design of a Role-based Trust-management Framework", booktitle = "Proc. of the {IEEE} Symposium on Research in Security and Privacy", year = "2002", organization = "{IEEE} Computer Society, Technical Committee on Security and Privacy", publisher = "{IEEE} Computer Society Press", pages = "114--130" } InProceedings{BJWW02, author = "C.\ Bettini and S.\ Jajodia and X.\ Sean Wang and D.\ Wijesekera", title = "Provisions and Obligations in Policy Management and Security Applications", editor = "P.\ Bernstein et al.", booktitle = "{VLDP 2002}: proceedings of the Twenty-Eighth International Conference on Very Large Data Bases, Hong Kong {SAR}, China, 20--23 August 2002", publisher = "Morgan Kaufmann", ISBN = "1-55860-869-9", pages = "502--513", year = "2002", URL = "http://www.vldb.org/conf/2002/S14P03.pdf"} @inproceedings{KSW02, author={G. Karjoth and M. Schunter and M. Waidner}, title={Platform for Enterprise Privacy Practices: Privacy-Enabled Management of Customer Data}, booktitle={Second International Workshop on Privacy Enhancing Technologies}, year={2002}, publisher={Springer-Verlag}, series={LNCS}, volume={2482}, pages={69-84} } @inproceedings{KS02:csfw, author = "G.~Karjoth and M.~Schunter", title = "A Privacy Policy Model for Enterprises", booktitle = {Proc.~of the 15th IEEE Computer Security Foundations Workshop (CSFW 2002), Cape Breton, Nova Scotia, Canada, June 24-26, 2002}, pages = {271-281}, publisher = {IEEE Computer Society Press}, year = "2002", isbn = {0-7695-1689-0}} @inproceedings{BPS03:esorics, author = {M.~Backes and B.~Pfitzmann and M.~Schunter}, title = {A Toolkit for Managing Enterprise Privacy Policies}, booktitle = {Proc.~of the 8th European Symposium on Research in Computer Security (ESORICS)}, series = {LNCS}, volume = {2808}, year = {2003}, pages = {162--180}, publisher = {Springer-Verlag}, isbn = {3-540-20300-1}} @inproceedings{AHLS02:wpes, author = {P.~Ashley and S.~Hada and G.~Karjoth and M.~Schunter}, title = {E-P3P privacy policies and privacy authorization}, booktitle = {Proc.~of the ACM workshop on Privacy in the Electronic Society (WPES 2002)}, year = {2002}, pages = {103--109}, publisher = {ACM Press}} @InProceedings{DeT02, author = "John {DeT}reville", title = "Binder, a Logic-based Security Language", booktitle = "Proceedings of the {IEEE} Symposium on Research in Security and Privacy", year = "2002", organization = "{IEEE} Computer Society, Technical Committee on Security and Privacy", publisher = "{IEEE} Computer Society Press", pages = "105--113" } @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{BP02, author = {S. Blom and J. van de Pol}, title = {State Space Reduction by Proving Confluence}, booktitle = {Proc.\ 14th Conference on Computer Aided Verification (CAV'02)}, pages = {596--609}, year = {2002}, OPTeditor = {}, number = {2404}, series = {LNCS}, publisher = {Springer-Verlag} } @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 = {M. Abadi and B. 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{DG04, AUTHOR = {G. Delzanno and P. Ganty}, TITLE = {{Automatic Verification of Time Sensitive Cryptographic Protocols}}, BOOKTITLE = {Proc. of Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems ({TACAS}'04)}, YEAR = 2004, SERIES = {LNCS}, PUBLISHER = {Springer-Verlag}, NUMBER = {2988}, PAGES = {342--356} } @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/} } @book{Sch99a, author = {F. B. Schneider}, title = {Trust in Cyberspace}, publisher = {National Academy Press, Washington}, month = {Jan}, year = {1999}, url = {http://www.nap.edu/readingroom/books/trust/}, annote = {ISBN 0309065585}, annote = {refs}, annote = {book}} @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", } Automated Verification of Secrecy Properties for Linear Logic Specifications of Cryptographic Protocols Marco Bozzano, Giorgio Delzanno Journal of Symbolic Computation 38(5): 1375-1415, 2004. @Article{BD04, author = {M Bozzano and G. Delzanno}, title = {Automated Verification of Secrecy Properties for Linear Logic Specifications of Cryptographic Protocols}, journal = {Journal of Symbolic Computation}, year = {2004}, volume = {38}, number = {5}, pages = {1375-1415}, } @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{Bol97, author = {D. Bolignano}, title = {Towards the Formal Verification of Electronic Commerce Protocols}, booktitle = {Proc.\ 10th Computer Security Foundations Workshop (CSFW'97)}, pages = {113--147}, year = {1997}, OPTeditor = {}, publisher = {IEEE Computer Society Press} } @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" } @article{HK99, author = "S. Halevi and H. Krawczyk", title = "Public-Key Cryptography and Password Protocols", journal = "ACM Transactions on Information and System Security", volume = "2", number = "3", pages = "25--60", year = "1999", url = "citeseer.nj.nec.com/halevi98publickey.html" } @Article{CFMW97, author = "M. Codish and M. Falaschi and K. Marriott and W. Winsborough", title = "A Confluent Semantic Basis for the Analysis of Concurrent Constraint Logic Programs", journal = "Journal of Logic Programming", year = "1997", volume = "30", number = "1", pages = "53--81", URL = "http://www.cs.bgu.ac.il/~mcodish/Papers/ppapers.html", acknowledgement = ack-mmc, } @InProceedings{MEK01, author = {O. Mansour and S. Etalle and T. Krol}, title = {Scheduling and Allocation of Non-Manifest Loops on Herdware Graph-Models}, booktitle = {Proc. PROGRESS workshop}, OPTpages = {}, year = {2001}, editor = {F. Karelse}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, ISBN = {90-73461-26-X} } @InProceedings{ACP93, author = {J.-M.~Andreoli and T.\ Castagnetti and R.\ Pareschi}, title = {Abstract Interpretation of Linear Logic Programming}, booktitle = {Proc. ILPS 93}, year = {1993}, editor = {D. Miller}, pages= {295-314} } @inproceedings{ACJT96, author = {P.~A.~Abdulla, K.~{C}er{\=a}ns, B.~Jonsson and Y.-K.~Tsay}, title = {General Decidability Theorems for Infinite-State Systems}, booktitle = {Proc. 10th IEEE Int. Symp. on Logic in Computer Science}, pages = {313--321}, year = {1996}} @article{AB90a, author = "K. R. Apt and H. A. Blair ", title = "Arithmetic classification of perfect models of stratified programs", journal = "Fundamenta Informaticae", volume = "13", pages = "1-18", year = 1990, Note = "Addendum in vol. 14, pages 339-344, 1991." } @InCollection{ABW88, author = "K. R. Apt and H. A. Blair and A. Walker", title = "Towards a theory of declarative knowledge", booktitle = "Foundation of Deductive Databases and Logic Programming", publisher = "Morgan Kaufmann", year = "1988", editor = "J. Minker, editor", pages = "89-148"} @ARTICLE {Apt82, AUTHOR = "K.R. Apt and M.H. van Emden", TITLE = "Contributions to the theory of logic programming", JOURNAL = JACM, YEAR = "1982", MONTH = "July", VOLUME = "29", NUMBER = "3", PAGES = "841-862", ANNOTE = ""} @incollection{Apt90, author = {K. R. Apt}, title = {Introduction to {L}ogic {P}rogramming}, booktitle = "Handbook of Theoretical Computer Science", volume = "B: Formal Models and Semantics", editor="J. van Leeuwen", publisher = "Elsevier, Amsterdam and The MIT Press, Cambridge", pages="495--574", year= "1990"} @InCollection{Apt94, author = "K. R. Apt", title = "Program Verification and Prolog", booktitle = "Specification and validation methods for programming languages and systems", publisher = OUP, year = "1994", editor = "E. B{\o}rgher", note = "to appear"} @Book{Apt97, author = "K.~R.~Apt", title = "From Logic Programming to Prolog", publisher = "Prentice Hall", year = "1997" } @Article{Apt98, author = {K.~R.~Apt}, title = {A Proof Theoretic View of Constraint Programming}, journal = {Fundamenta Informaticae}, year = {1998}, volume = {34}, number = {3}, pages = {295-321}} @Article{Apt99, author = {K.~R. Apt}, title = {The essence of constraint propagation}, journal = {Theoretical Computer Science}, year = {1999}, volume = {221}, number = {1--2}, pages = {179--210}, note = {Available via \verb+http://xxx.lanl.gov/archive/cs/+} } @inproceedings{AAP78, author = "L. Aiello and G. Attardi and G. Prini", title = "Towards a more declarative programming style", booktitle = "Proc. of the IFIP Conference on Formal Description of Programming Concepts", publisher = N-H, pages = "121-137", editor = "E. J. Neuhold", year = 1978 } @article{AB91, author = "K. R. Apt and M. Bezem", title = "Acyclic Programs", journal = NGC, volume = 9, number = "3\&4", pages = "335-363", year = 1991 } @inproceedings{AB90, author = "K. R. Apt and M. Bezem", title = "Acyclic Programs", booktitle = "Proceedings of the Seventh International Conference on Logic Programming", publisher = "The MIT Press", pages = "617-633", editor = "D. H. D. Warren and P. Szeredi", year = 1990 } @article{AB94, author = "K. R. Apt and M. Bezem", title = "Acyclic Programs", journal = NGC, volume = 9, number = "3\&4", pages = "335-363", year = 1991 } @article {AB94-negation, author = "K. R. Apt and R. Bol", title = "Logic Programming and Negation: a Survey", journal = jlp, volume = "19-20", pages = "9-71", year = "1994"} @inproceedings{AD92, author = "C. Aravidan and P. M. Dung", title = "Partial deduction of logic programs w.r.t. well-founded semantics", booktitle = "Proceedings of the Third International Conference on Algebraic and Logic Programming", publisher = "Springer-Verlag", pages = "384-402", editor = "H. Kirchner G. Levi", year = 1992 } @TechReport{AD93, AUTHOR = "C. Aravidan and P. M. Dung", TITLE = "On the correctness of {U}nfold/{F}old transformation of normal and extended logic programs", INSTITUTION = "Division of {C}omputer {S}cience, Asian {I}nstitute of {T}echnology, {B}angkok, {T}hailand", month = "April", year = "1993"} @inproceedings{AE93, author = "K. R. Apt and S. Etalle", title = "On the unification free {P}rolog programs", booktitle = "Proceedings of the Conference on Mathematical Foundations of Computer Science (MFCS 93)", editor = "A. Borzyszkowski and S. Sokolowski", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", address = "Berlin", pages = "1--19", year = 1993 } @inproceedings{AF88, author = "I. Attali and P. Franchi-Zannettacci", title = "Unification-free Execution of {TYPOL} programs by semantic attribute evaluation", booktitle = "Proceedings of the Fifth International Conference on Logic Programming", publisher = "The MIT Press", pages = "160-177", editor = "R.A. Kowalski and K.A. Bowen", year = 1988 } @techreport{AL93b, author = "A. Aiken and T.K. Lakshman", title = "Type Checking Directionally Typed Logic Programs", institution = {Department of Computer Science, University of Illinois at Urbana Champaign}, month = "november", year = 1993 } @inproceedings{AK94, author = "A. Aiken and T.K. Lakshman", title = "Directional Type Checking of Logic Programs", booktitle = "Static Analysis, First International Static Analysis Symposium, (SAS'94)", editor = "B. Le Charlier", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", number = "864", address = "Berlin", pages = "43-60", year = 1994, } @inproceedings{AL95, author = "K. R. Apt and I. Luitjes", title = "Verification of Logic Programs with Delay Declarations", booktitle = "Proceedings of the Fourth International Conference on Algebraic Methodology and Software Technology, (AMAST'95)", editor = "V. Alagar and M.Nivat", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", address = "Berlin", pages = "66-90", year = 1995, } @Article{AguMod93, author = "Aguzzi and Modigliani", title = "Proving Termination of Logic Programs by Transforming them Equivalent Term Rewriting Systems", journal = "FSTTCS: Foundations of Software Technology and Theoretical Computer Science", volume = "13", year = "1993" } @techreport{AM93, author ="K. R. Apt and E. Marchiori", title = "Reasoning about {P}rolog programs: from Modes through Types to Assertions", institution = "CWI, Amsterdam, The Netherlands", year = 1993, number = "CS-R9358", note = cwinote } @article{AM94, author = "K. R. Apt and E. Marchiori", title = "Reasoning about {P}rolog programs: from {M}odes through {T}ypes to {A}ssertions.", journal = "Formal Aspects of Computing", volume = "6", number = "6A", pages = "743-765", year = 1994 } @InProceedings{Ant91, author = "S.~Antoy", title = {Lazy Evaluation in Logic}, booktitle = "PLILP 91, Passau, Germany (Lecture Notes in Computer Science, Vol.528)", year = "1991", editor = "Maluszynski and M. Wirsing", pages = "371-382", publisher = "Springer-Verlag"} @inproceedings{AP90, author = "K. R. Apt and D. Pedreschi", title = "Studies in Pure {P}rolog: termination", booktitle = "Symposium on Computional Logic", editor = "J.W. Lloyd", publisher = "Springer-Verlag", address = "Berlin", pages = "150-176", year = 1990 } @inproceedings{AP91, author = "K. R. Apt and D. Pedreschi", title = " Proving Termination of General {P}rolog Programs", booktitle = "Proceedings of the International Conference on Theoretical Aspects of Computer Software", editor = "T. Ito and A. Meyer", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science 526", address = "Berlin", pages = "265-289", year = 1991 } @article{AP93, author = "K. R. Apt and D. Pedreschi", title = " Reasoning about Termination of Pure {P}rolog Programs", journal = i&c, volume = "106", number = "1", pages = "109--157", year = 1993, } @incollection{AP94, author = "K. R. Apt and D. Pedreschi", title = "Modular Termination Proofs for Logic and Pure {P}rolog Programs", booktitle = "Advances in Logic Programming Theory", editor = "G. Levi", publisher = {Oxford University Press}, year = "1994", pages = "183-229" } @article{AP94a, author = "K. R. Apt and A. Pellegrini", title = "On the occur-check free {P}rolog programs", journal = "ACM Toplas", year = 1994, volume = 16, number = 3, pages = "687-726" } @InProceedings{Aug97, author = "L. Augustsson", title = "Partial Evaluation in Aircraft Crew Planning", pages = "127--136", ISSN = "0362-1340", booktitle = "Proceedings of the {ACM} {SIGPLAN} Symposium on Partial Evaluation and Semantics-Based Program Manipulation ({PEPM}-97)", series = "ACM SIGPLAN Notices", volume = "32, 12", publisher = "ACM Press", address = "New York", year = "1997"} %%%B @phdthesis{Bau89, AUTHOR = "M. Baudinet", TITLE = "Logic Programming Semantics: Techniques and Applications", school = "Stanford University, Stanford, California", YEAR = "1989"} @InProceedings{Bar98, author = {R. Bart\`{a}k}, title = {Constraint Hierarchy Networks}, booktitle = {Third ERCIM/Compulog Workshop on Constraints}, OPTpages = {}, year = {1998}, OPTeditor = {}} @inproceedings{BBGLM93, author = {A. Bossi and M. Bugliesi and M. Gabbrielli and G. Levi and M. C. Meo}, title = {Differential Logic Programming}, Booktitle = popl93, publisher = "ACM Press", year = {1993}, pages ={359-370}} @InProceedings {BC89, author = "A. Bossi and N. Cocco", title = "Verifying correctness of logic programs", booktitle = "TAPSOFT '89, Barcelona, Spain, March 1989, (Lecture Notes in Computer Science, vol. 352)", year = "1989", pages = " 96-110", publisher = S-V, editor = "J. Diaz and F. Orejas", OPTnote = ""} @TechReport{BC90, AUTHOR = "A. Bossi and N. Cocco", TITLE = "Basic Transformation Operations for logic programs which preserve Computed Answer Substitutions", INSTITUTION = "Dip. Matematica Pura e Applicata, Universit\`{a} di Padova, Italy", number = "16", month = "April", year = "1990", NOTE = "to appear in Special Issue on Partial Deduction of the Journal of Logic Programming"} @article{BC93, author = {A. Bossi and N. Cocco}, title = {Basic {T}ransformation {O}perations which preserve {C}omputed {A}nswer {S}ubstitutions of {L}ogic {P}rograms}, journal = jlp, volume = 16, number = "1\&2", year = 1993, pages = {47-87}} @inproceedings{BC94, author = {A. Bossi and N. Cocco}, title = {Preserving Universal Termination trough Unfold/Fold}, booktitle = alp94, series = lncs, volume = 850, publisher = springer, editor = edalp94, pages = "269-286", year = "1994"} @InProceedings{BC97, author = {A. Bossi and N. Cocco}, title = {Replacement Can Preserve Termination}, booktitle = lopstr96, pages = {104-129}, year = {1997}, editor = edlopstr96, volume = vollopstr96, series = lncs, publisher = springer } @InProceedings{BC98, author = {A. Bossi and N. Cocco}, title = {Programs Without Failures}, booktitle = lopstr97, pages = {28-48}, year = {1998}, editor = edlopstr97, volume = vollopstr97, series = lncs, publisher = springer } @InProceedings{BC99, author = {A. Bossi and N. Cocco}, title = {Successes in Logic Programs}, booktitle = lopstr98, pages = {219-139}, year = {1999}, editor = edlopstr98, volume = vollopstr98, series = lncs, publisher = springer } @ARTICLE {BCD90, AUTHOR = "A. Bossi and N. Cocco and S. Dulli", TITLE = "A method for specializing logic programs", JOURNAL = "ACM Transactions on Programming Languages and Systems", YEAR = "1990", MONTH = "April", VOLUME = "12", NUMBER = "2", PAGES = "253-302", ANNOTE = ""} %---------------------------------------------------------------- @inproceedings{BCE92, author = {A. Bossi and N. Cocco and S. Etalle}, title = {Transforming {N}ormal {P}rograms by {R}eplacement}, booktitle = "{M}eta {P}rogramming in {L}ogic - {P}roceedings {META}'92", series = lncs, volume = 649, publisher = springer, editor = "A. Pettorossi", pages = "265-279", year = "1992", isbn = "3-540-56282-6"} %---------------------------------------------------------------- @inproceedings{BCE92b, author = {A. Bossi and N. Cocco and S. Etalle}, title = {On {S}afe {F}olding}, booktitle = "Programming {L}anguage {I}mplementation and {L}ogic {P}rogramming - {P}roceedings {PLILP}'92", series = lncs, volume =631 , publisher = S-V, editor = "M. Bruynooghe and M. Wirsing", pages = "172-186", year = "1992", isbn ="3-540-55844-6" } @TechReport{BCE93, AUTHOR = "A. Bossi and N. Cocco and S. Etalle", TITLE = "Simultaneous Replacement in Normal Programs", INSTITUTION = cwi, number = "CS-R9357", month = "August", year = "1993", note = "To appear in Journal of Logic and Computation, 1996. Available at ftp.cwi.nl, in /pub/etalle"} @article{BCE96, AUTHOR = "A. Bossi and N. Cocco and S. Etalle", TITLE = "Simultaneous Replacement in Normal Programs", journal = "Journal of Logic and Computation", YEAR = "1996", number = "1", volume = "6", month = "February", pages = "79-120", issn = "0955-792X"} @InProceedings{BCE95, author = "A. Bossi and N. Cocco and S. Etalle", title = "Transformation of {L}eft {T}erminating {P}rograms: the {R}eordering {P}roblem", editor = "M. Proietti", number = "1048", series = "LNCS", pages = "33-45", booktitle = "LOPSTR95 -- Fifth International Workshop on Logic Program Synthesis and Transformation", year = "1996", publisher = "Springer-Verlag" } @InProceedings{BCE99, author = {A. Bossi and N. Cocco and S. Etalle}, title = {Transformation of Left Terminating Programs}, booktitle = {Ninth International Workshop on Logic Program Synthesis and Transformation}, pages = {156-175}, year = {2000}, editor = {A. Bossi}, number = {1817}, series = {LNCS}, publisher = s-v, OPTnote = {ISSN 0302-9743. ISBN 3-540-67628-7.}} @ARTICLE {BE94, AUTHOR = {A. Bossi and S. Etalle}, TITLE = "Transforming {A}cyclic {P}rograms", JOURNAL = TOPLAS, YEAR = "1994", number = "4", volume = "16", month = "July", pages = "1081-1096"} @inproceedings{BE94b, author = {A. Bossi and S. Etalle}, title = {More on {U}nfold/{F}old {T}ransformations of {N}ormal {P}rograms: {P}reservation of {F}itting's {S}emantics}, booktitle = "Proc. Fourth International Workshop on Meta Programming in Logic", year = "1994", editor = "F. Turini", publisher = "Springer-Verlag", series = "LNCS", number = "883", pages = "265-279", ISBN="3-540-58792-6"} @InProceedings{BEP99, author = {M. Bertolino and S. Etalle and C. Palamidessi}, title = {The Replacement Operation for CCP Programs}, booktitle = {Ninth International Workshop on Logic Program Synthesis and Transformation}, OPTpages = {}, year = {2000}, pages = {216-233}, editor = {A. Bossi}, number = {1817}, series = {LNCS}, publisher = s-v, OPTnote = {ISSN 0302-9743. ISBN 3-540-67628-7.}} @TechReport{BER99techrep, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Properties of Input-Consuming Derivations}, institution = {Universiteit Maastricht}, number = {CS 99-06}, year = {1999} } @Article{BER99, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Properties of Input-Consuming Derivations}, journal = {Electronic Notes in Theoretical Computer Science}, year = 1999, volume = 30, number = 1, note = {http://www.elsevier.nl/locate/entcs}} @TechReport{BER00-techrep, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Semantics of input-consuming programs}, institution = {Universiteit Maastricht}, year = {2000}, number = {CS 00-01} } @InProceedings{BER00-cl2000, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Semantics of input-consuming programs}, editor = edcl2000, number = "1861", series = "LNAI", pages = "194-208", booktitle = cl2000, year = "2000", publisher = "Springer-Verlag", note = "ISBN 3-540-67797-6" } @InProceedings{BERS01, author = {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus}, title = {Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling}, booktitle = {Proc. European Symposium on Programming}, pages = {402-416}, year = {2001}, editor = {D. Sands}, number = {2028}, series = {LNCS}, publisher = {Springer-Verlag}, note = {available at http://link.springer.de/link/service/series/0558/tocs/t2028.htm}, ISBN = {3-540-41862-8} } @Article{BER02, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Properties of input-consuming derivations}, journal = {Theory and Practice of Logic Programming}, volume = {2}, number = {2}, year = {2002}, pages = {125-154}, note = {Available also at CoRR at http://xxx.lanl.gov/abs/cs.PL/0101023} } @Article{BER01, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Semantics of well-moded input-consuming logic programs}, journal = {Computer Languages}, year = {2001}, volume = {26}, number = {1}, pages = {1-25}, publisher = {Elsevier}, ISSN ={0096-0551} } @Article{BER02, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Properties of Input Consuming Derivations}, journal = tplp, note = {To appear. Available also at CoRR at http://xxx.lanl.gov/abs/cs.PL/0101023} } @Article{BER00, author = {A. Bossi and S. Etalle and S. Rossi}, title = {Properties of Input-Consuming Derivations}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2000}, OPTkey = {}, volume = {30}, number = {1}, OPTpages = {}, OPTmonth = {}, note = {Proceedings of the ICLP99 post-conference workshop in verification and analysis of logic programs}, OPTannote = {} } @MISC {Ber97, AUTHOR = "M. Bertolino", TITLE = "Transformazione dei programmi concorrenti {T}esi di {L}aurea, {D}ip. {I}nformatica e {S}cienze dell' {I}nformazione, {U}niversit\`{a} di {G}enova, {G}enova, {I}taly", HOWUBLISHED = "Tesi di Laurea, Universit\`{a} di Genova", YEAR = "1997"} @ARTICLE {Bez93, AUTHOR = "M. Bezem", TITLE = "Strong termination of logic programs", JOURNAL = "Journal of Logic Programming", YEAR = "1993", VOLUME = "15", number = "1\&2", pages = "79-97", ANNOTE = ""} @InProceedings {BCF91, author = "A. Bossi and N. Cocco and M. Fabris", title = "Proving termination of logic programs by exploiting term properties", booktitle = "TAPSOFT '91, Brighton, United Kingdom, April 1991, (Lecture Notes in Computer Science 494)", year = "1991", pages = "153-180", editor = "S. Abramsky and T.S.E. Maibaum", publisher = S-V, OPTnote = ""} @article{BCF94, author = {A. Bossi and N. Cocco and M. Fabris}, title = {Norms on {T}erms and their use in {P}roving {U}niversal {T}ermination of a {L}ogic {P}rogram}, journal = tcs, volume = 124, year = 1994, pages = {297-328}} @ARTICLE {BD77, AUTHOR = "R.M. Burstall and J. Darlington", TITLE = "A transformation system for developing recursive programs", JOURNAL = JACM, YEAR = "1977", MONTH = "January", VOLUME = "24", NUMBER = "1", PAGES = "44-67", ANNOTE = ""} @Article{BFB92, author = "A. Borning and B. N. Freeman-Benson and M. Wilson", title = {Constraint Hierarchies}, journal = "Lisp and Symbolic Computation", volume = "5", number = "3", year = "1992", pages = "223--270", mynote = "Borning_ec_92LSC_constraint_hierarchies.ps.gz" } @inproceedings{BG94, author = {N. Bensaou and I. Guessarian}, title = {{T}ransforming {C}onstraint {L}ogic {P}rograms}, booktitle = lopstr94, year = "1994", editor = edlopstr94} series = lncs, publisher = springer} @Article{BG98, title = {Transforming Constraint Logic Programs}, author = "N. Bensaou and I. Guessarian", pages = "81--125", journal = "Theoretical Computer Science", year = "1998", volume = "206", number = "1--2", references = "\cite{JLOGP::BossiC1993} \cite{TOPLAS::BossiCD1990} \cite{TOPLAS::BossiE1994} \cite{JACM::BurstallD1977} \cite{STACS::DenisD1991} \cite{TCS::EtalleG1996} \cite{JFP::EtalleG1996} \cite{TCS::FalaschiLMP1989} \cite{POPL::JaffarL1987} \cite{JLOGP::JaffarM1994} \cite{TCS::Maher1993} \cite{JLOGP::PettorossiP1994}" } @Article{BGLM94:s-semantics, author = "Annalisa Bossi and Maurizio Gabrielli and Giorgio Levi and Maurizio Martelli", title = "The {S}-Semantics Approach: Theory and Applications", journal = "The Journal of Logic Programming", year = "1994", month = "May", volume = "19 \& 20", pages = "149--198" } @article{BGLM94, author="A.~Bossi and M.~Gabbrielli and G.~Levi and M.~C. Meo", title= "A {C}ompositional {S}emantics for {L}ogic {P}rograms", journal=tcs, volume=122, number ="1-2", year= 1994, pages = "3--47"} @InProceedings{BGMP94, author = "F.~de Boer and M.~Gabbrielli and E.~Marchiori and C. Palamidessi", title = "Proving Concurrent Constraint Programs Correct", pages = "98-108", booktitle = popl94, year = "1994", publisher = "ACM press" } @Article{BGMP97, author = "F. de Boer and M. Gabbrielli and E. Marchiori and C. Palamidessi", title = "Proving Concurrent Constraint Programs Correct", journal = "ACM Transactions on Programming Languages and Systems", volume = "19", number = "5", pages = "685--725", year = "1997", url = "http://www.acm.org:80/pubs/citations/journals/toplas/1997-19-5/p685-de_boer/", abstract = "We introduce a simple compositional proof system for proving (partial) correctness of concurrent constraint programs (CCP). The proof system is based on a denotational approximation of the strongest postcondition semantics of CCP programs. The proof system is proved to be correct for full CCP and complete for the class of programs in which the denotational semantics characterizes exactly the strongest postcondition. This class includes the so-called confluent CCP, a special case of which is constraint logic programming with dynamic scheduling.", keywords = "languages; theory; verification", subject = "{\bf D.1.3} Software, PROGRAMMING TECHNIQUES, Concurrent Programming. {\bf D.3.1} Software, PROGRAMMING LANGUAGES, Formal Definitions and Theory, Semantics. {\bf F.3.1} Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS, Specifying and Verifying and Reasoning about Programs, Logics of programs. {\bf F.3.2} Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS, Semantics of Programming Languages, Denotational semantics." } @InProceedings{BGP96, author = "F. de Boer and M.~Gabbrielli and C. Palamidessi", title = "Proving Correctness of Constraint Logic Programs with Dynamic Scheduling", OPTeditor = "R.~Cousot and D.~Schmidt", OPTvolume = "", OPTnumber = "", series = "LNCS", OPTpages = "", booktitle = "Static Analysis, Third International Static Analysis Symposium, (SAS'96)", year = "1996", OPTorganization = "", publisher = springer } @InProceedings{BL90, author = "K. Benkerimi and J. W. Lloyd", title = "A partial evaluation procedure for logic programs", booktitle = "Logic Programming: Proceedings of the 1990 North American Conference, Austin, Texas, October 1990", year = "1990", editor = "S. Debray and M. Hermenegildo", pages = "343-358", publisher = "MIT Press"} @InProceedings{BK00, author = {C. Boyd and P. Kearney}, title = {Exploring Fair Exchange Protocols Using Specification Animation}, booktitle = {Proc.\ Information Security Workshop (ISW00)}, pages = {209-223}, year = {2000}, OPTeditor = {}, number = {1975}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{BKK98, author = {P. Borovansk\'i and C. Kirchner and H. Kirchner}, title = {A Functional View of Rewriting and Strategies for a semantics of {E}{L}{A}{N}}, booktitle = {Third Fuji International Symposium on Functional and Logic Programming}, OPTpages = {}, year = {1998}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, address = {Kyoto, Japan}, month = {April}, OPTorganization = {}, OPTpublisher = {}} @Article{BLM92, author = "A. Brogi and E. Lamma and P. Mello", title = "Compositional {M}odel-theoretic {S}emantics for {L}ogic {P}rograms.", journal = NGC, year = "1992", volume = "11", number = "1", pages = "1-21" } @InProceedings{BGR00, author = {S. Bistarelli and R. Gennari and F. Rossi}, title = {Constraint Propagation for Soft Constraint Satisfaction Problems: Generalization and Termination Condition}, booktitle = {Int. Conference on Principle and Practice of Constraint Programming}, OPTpages = {}, year = {2000}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, series = {LNCS}, publisher = S-V} @ARTICLE {Bird84-toplas, AUTHOR = "R.S. Bird", TITLE = "The {P}romotion and {A}ccumulation {S}trategies in {T}ransformational {P}rogramming", JOURNAL = "TOPLAS ACM", YEAR = "1984", VOLUME = "6", NUMBER = "4", pages = "487-504"} @Article{Bird84, author = "R. S. Bird", title = "{Using Circular Programs to Eliminate Multiple Traversals of Data}", journal = "Acta Informatica", year = "1984", volume = "21", pages = "239--250", abstract = "This paper describes a technique for transforming functional programs that repeatedly traverse a data structure into more efficient alternatives that do not. The transformation makes essential use of lazy evaluation and local recursion (such as provided by letrec, or its equivalent) to build a circular program that, on one pass over the structure, determines the effects of the individual traversals and the combines them.", keywords = "Circular Programs" } @ARTICLE{BLM93, author = "A. Brogi and E. Lamma and P. Mello", title = "Composing Open Logic Programs", JOURNAL = "Journal of Logic and Computation", YEAR = "1993", VOLUME = "3", Number = "4", PAGES = "417-439" } @ARTICLE{BLM94, AUTHOR = "M. Bugliesi and E. Lamma and P. Mello", TITLE = "Modularity in Logic Programming", JOURNAL = JLP, VOLUME = "19-20", PAGES = "443-502", YEAR = "1994" } @InProceedings{BLR92, author = "F. Bronsard and T.K. Lakshman and U.S. Reddy", title = "A Framework of Directionality for Proving Termination of Logic Programs", booktitle = jicslp92, year = 1992, editor = "K. R. Apt", publisher = "MIT Press", pages = "321-335" } @InProceedings{BM93, author = "B. Bertolino and M. Mowbray", title = "A Completeness Result for SLDNF-resolution", booktitle = "GULP'93: Atti dell'Ottavo Convegno sulla Programmazione Logica, Gizzera, Italy, June 1993", year = "1993", editor = "Domnico Sacc\`a", pages = "301-307", publisher = "Mediterranean Press"} @InProceedings{BM95, author = "J. Boye and J. {Ma\l uszy{\'n}ski}", title = "Two Aspects of Directional Types", booktitle = iclp95, year = 1995, editor = ediclp95, publisher = mit, pages = "747-764"} @Article{BM97, author = "J. Boye and J. {Ma\l uszy{\'n}ski}", title = "Directional Types and the Annotation Method", OPTcrossref = "", OPTkey = "", journal = jlp, year = "1997", volume = "33", OPTnumber = "3", pages = "179-220", OPTmonth = "", OPTnote = "", OPTannote = "" } @inproceedings{BMPT90, author = "A. Brogi and P. Mancarella and D. Pedreschi and F. Turini", title = "Composition {O}perators for {L}ogic {T}heories", booktitle = "Proc. Symposium on Computational Logic", editor = "J. W. Lloyd", organization = "Springer-Verlag, Basic Research Series", year = "1990", pages = "117-134" } @InProceedings{BMMW89, author = "A. Borning and M. Maher and A. Martindale and M. Wilson", title = "Constraint Hierarchies and Logic Programming", pages = "149--164", OPTISBN = "0-262-62065-0", editor = "G. Levi and M. Martelli", booktitle = "Proceedings of the 6th International Conference on Logic Programming ({ICLP} '89)", OPTaddress = "Lisbon, Portugal", OPTmonth = jun, year = "1989", publisher = "MIT Press" } @InProceedings{BP91, author = {F.~de~Boer and C.~Palamidessi}, title = {A Fully Abstract Model for Concurrent Constraint Programming}, booktitle = {TAPSOFT/CAAP}, year = {1991}, editor = {S.~Abramsky and T.S.E. Maibaum}, number = {493}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{BP92, author = {F. de~Boer and C.~Palamidessi}, title = {On the semantics of concurrent constraint programming}, booktitle = {ALPUK 92, Workshops in Computing}, pages = {145-173}, year = {1992}, editor = S-V} @InProceedings {BR86, author = "F. Bancilhon and R. Ramakrishnan", title = "An amateur's introduction to recursive query processing strategies", booktitle = "ACM SIGMOD Conference, Washington, U.S.A., May 1986", year = "1986", pages = "16-52", publisher = "ACM", OPTnote = ""} @Article{Buc98, author = {W. Buchholz}, title = {A Note on SLDNF Resolution}, journal = {Journal of Logic and Computation}, year = {1998}, volume = {8}, number = {2}, pages = {159-167}} %%%C @article{CG89, author = "N.\ Carriero and D.\ Gelernter", title = "How to Write Parallel Programs: {A} Guide to the Perplexed", journal = "ACM Computing Surveys", volume = "21", number = "3", pages = "323--357", year = "1989" } @Article{CLM00, author = {B. Crispo and P. Landrock and V. Matyas Jr}, title = {WWW Security and Trusted Third Party Services}, journal = {Future Generation Computer Systems}, year = {2000}, volume = {16}, number = {4}, pages = {331-341} } @Article{Cas98, author = {C. Castro}, title = {Building Constraint Satisfaction Problems Using Rewrite Rules and Strategies}, journal = {Fundamenta Informaticae}, year = {1998}, volume = {34}, number = {3}, OPTpages = {}} @inproceedings{CC77, author = {P. Cousot and R. Cousot}, title = {Abstract {I}nterpretation: {A} {U}nified {L}attice {M}odel for {S}tatic {A}nalysis of {P}rograms by {C}onstruction or {A}pproximation of {F}ixpoints}, booktitle = "Proc. Fourth ACM Symp. Principles of Programming Languages", Year = 1977, pages = {238-252}} @book{CC88, author = "H. Coelho and J. C. Cotta", title = "Prolog by Example", publisher = "Springer-Verlag", address = "Berlin", year = 1988 } @inproceedings{CCC90, AUTHOR = "C. Codognet and P. Codognet and M. Corsini", TITLE = "Abstract {I}nterpretation for {C}oncurrent {L}ogic {L}anguages", BOOKTITLE = naclp90, editor= ednaclp90, PUBLISHER = mit, YEAR = 1990, pages = "215-232"} @InProceedings{CDG93, author = "M. Codish and S. K. Debray and R. Giacobazzi", title = {Compositional Analysis of Modular Logic Programs}, editor = "{ACM}", booktitle = {Twentieth Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages}, publisher = "ACM Press", OPTaddress = "New York, NY, USA", year = "1993", pages = "451--464", OPTkeywords = "Abstract interpretation; Abstract unfolding; Compositional semantics; Modular logic programs; Program predicates", OPTthesaurus = "Logic programming; Program diagnostics" } @article{CFM94, author = {M. Codish and M. Falaschi and K. Marriott}, title = {Suspension {A}nalyses for {C}oncurrent {L}ogic {P}rograms}, journal = toplas, volume = 16, number = 3, pages = "649-686", year = {1994}} @InProceedings {CG94, author = "J. Cook and J.P. Gallagher", title = "A transformation system for definite programs based on termination analysis", booktitle = lopstr94, year = "1994", OPTpages = "51-68", publisher = S-V, editor = edlopstr94, OPTnote = ""} @InProceedings {Cav89, author = "L. Cavedon", title = "Continuity, consistency and completeness properties for logic programs", booktitle = "6 International Conference on Logic Programming", year = "1989", pages = "571-584", publisher = "MIT press", editor = "G. Levi and M. Martelli", OPTnote = ""} @Article {Cav91, author = "L. Cavedon", title = "Acyclic programs and the completeness of {SLDNF}-resolution", journal = "Theoretical Computer Science", volume = "86", year = "1991", pages = "81-92"} @InCollection{Cla78, author = "K. L. Clark", title = "Negation as failure rule", booktitle = "Logic and Data Bases", publisher = "Plenum Press", year = "1978", editor = "H. Gallaire and G. Minker", pages = "293-322"} @InProceedings{CDM96, author = "P. Chambre and P. Deransart and J. {Ma\l uszy{\'n}ski}", title = "A Proof method for safety properties of Clausal Concurrent Constraint Programs", editor = "F. de Boer and M. Gabbrielli", booktitle = "Proc. JICSLP'96 Post-Conference Workshop on Verification and Analysis of Logic Programs", note = "Technical Report TR-96-31, Dipartimento di Informatica di Pisa", year = "1996" } @techreport{CP91, author = "R. Chadha and D.A. Plaisted", title = "Correctness of Unification without Occur Check in {P}rolog", institution = "Department of Computer Science, University of North Carolina, Chapel Hill, N.C.", year = 1991} @article{CP94, author = "R. Chadha and D. A. Plaisted", title = "Correctness of Unification without Occur Check in {P}rolog", journal = jlp, volume = 18, number = 2, pages = "99-122", year = 1994} @InProceedings {CT77, author = "K.L. Clark and S. Tarnlund", title = "A first order theory of data and programs", booktitle = "IFIP 77", year = "1977", pages = "939-944", publisher = "", OPTnote = ""} @InProceedings {CS77, author = "K.L. Clark and S. Sickel", title = "Predicate logic: a calculus for deriving programs", booktitle = "Proceedings of IJCAI'77", year = "1977", pages = "419-120", OPTpublisher = "", OPTnote = ""} %%D @article{DD94, AUTHOR = "D. {De Schreye} and S. Decorte", TITLE = {Termination of Logic Programs: the never-ending story}, JOURNAL = jlp, YEAR = "1994", VOLUME = "19-20", PAGES = "199-260"} @InProceedings{DDF93, author = "S.~Decorte and D.~De Schreye and M.~Fabris.", title = {Automatic inference of norms: a missing link in automatic termination analysis}, editor = edilps93, OPTvolume = "526", number = "526", series = "Lecture Notes in Computer Science", pages = "420--436", booktitle = ilps93, publisher = S-V, year = "1993"} @article{Deb89, author = {S. K. Debray}, title = {Static Inference of Modes and Data Dependencies in Logic Programs}, journal = {ACM Transactions on Programming Languages and Systems}, volume = 11, number = 3, pages = "418-481", year = {1989}} @TechReport{Deb93, author = {S. K. Debray}, title = {{Q}{D}-{J}anus: A Sequential Implementation of Janus in Prolog}, institution = {University of Arizona}, year = {1993}} @article{DeM85, author = "P. Deransart and J. Maluszynski", title = "Relating {L}ogic {P}rograms and {A}ttribute {G}rammars", journal = jlp, volume = 2, year = {1985}, pages = {119-156}} @Article{Der97, author = {N.~Dershowitz}, title = {Termination of Rewriting}, journal = {Journal of Symbolic Computation}, year = {1987}, OPTvolume = {}, number = {8}, pages = {69-116} } @inproceedings{Dix95, author = {J. Dix}, title = {Semantics of {L}ogic {P}rograms: Their Intuition and Formal Properties. {A}n overview.}, booktitle = "Proc. of Konstanz Colloquium in Logic and Information '92", publisher = "DeGruyter", pages = "241-329", year = "1995", note = "See http://www.uni-koblenz.de/~dix/"} @inproceedings{DFS96, author = {N. De Francesco and A. Santone}, title = {Unfold/Fold transformation of concurrent processes}, booktitle = plilp96, volume = 1140, publisher = S-V, editor = edplilp96, pages = "167-181", year = "1996"} @inproceedings{DGB94, author = {S. Debray and D. Gudemann and P. Bigot}, title = {Detection and Optimization of Suspension-free logic programs}, pages = "487-504", booktitle = ilps94, editor = edilps94, publisher = { MIT Press}, year = {1994}} @InProceedings{DGH97, author = "S. Debray and P. L{\'o}pez-Garc{\'\i}a and M. Hermenegildo", title = "{Non-Failure Analysis for Logic Programs}", pages = "48--62", editor = "Lee Naish", booktitle = "Proceedings of the 14th International Conference on Logic Programming", publisher = "MIT Press", address = "Cambridge", year = "1997", } @Article{DGJLMS99, author = {D. De Schreye and R. Gl\"uck and Jesper J\o{}rgensen and M. Leuschel and B. Martens and M. H. S\o{}rensen}, title = {Conjunctive partial deduction: foundations, control, algorithms, and experiments}, journal = jlp, year = 1999, volume = {41}, number = {2-3}, pages = {231-277}, OPTnote = {Partial deduction in the Lloyd-Shepherdson framework cannot achieve certain optimisations which are possible by unfold/fold transformations. We introduce conjunctive partial deduction, an extension of partial deduction accommodating such optimisations, e.g., tupling and deforestation. We first present a framework for conjunctive partial deduction, extending the Lloyd-Shepherdson framework by considering conjunctions of atoms (instead of individual atoms) for specialisation and renaming. Correctness results are given for the framework with respect to computed answer semantics, least Herbrand model semantics, and finite failure semantics. Maintaining the well-known distinction between local and global control, we describe a basic algorithm for conjunctive partial deduction, and refine it into a concrete algorithm for which we prove termination. The problem of finding suitable renamings which remove redundant arguments turns out to be important, so we give an independent technique for this. A fully automatic implementation has been undertaken, which always terminates. Differences between the abstract semantics and Prolog's left-to-right execution motivate deviations from the abstract technique in the actual implementation, which we discuss. The implementation has been tested on an extensive set of benchmarks which demonstrate that conjunctive partial deduction indeed pays off, surpassing conventional partial deduction on a range of small to medium-size programs, while remaining manageable in an automatic and terminating system. }} @incollection{DJ90, author = {N.~Dershowitz and J-P. Jouannaud}, title = {Rewrite {S}ystems}, booktitle = "Handbook of Theoretical Computer Science", volume = "B: Formal Models and Semantics", editor="J. van Leeuwen", publisher = "Elsevier, Amsterdam and The MIT Press, Cambridge", pages="243--320", year= "1990"} @article{DKM84, author = "C. Dwork and P.C. Kanellakis and J.C. Mitchell", title = "On the Sequential Nature of Unification", journal = jlp, volume = 1, number = 1, pages = "35-50", year = 1984 } @InProceedings{DLH97, author = "S. Debray and P. L{\'o}pez-Garc{\'\i}a and M. Hermenegildo", title = "Non-Failure Analysis for Logic Programs", pages = "48--62", OPTISBN = "0-262-64035-X", editor = "Lee Naish", booktitle = "Proceedings of the 14th International Conference on Logic Programming", publisher = "MIT Press", OPTaddress = "Cambridge", year = "1997" } @InProceedings{DOvH97, author = "Y. Deville and O. Barette and P.{Van Hentenryck}", title = "Constraint Satisfaction over Connected Row Convex Constraints", editor = edijcai97, OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = ijcai97, year = 1997, OPTpublisher = "" } @Article{DW89, author = "S. Debray and D. S. Warren", title = "{Functional Computations in Logic Programs}", journal = toplas, year = "1989", volume = "11", number = "3", pages = "451-481", month = "July" } @inproceedings{WG91, author ="D. A. de Waal and J. P Gallagher", title = "Specialization of a unification algorithm", booktitle = lopstr91, year = 1991, editor = edlopstr91, pages = "205-221", publisher = S-V} @BOOK {Dev90, AUTHOR = "Y. Deville", TITLE = "Logic Programming. Systematic Program Development", PUBLISHER = A-W, YEAR = "1990", NOTE = "", ANNOTE = ""} @inproceedings{DKS86, author ="C. Dwork and P. Kannellakis and L. Stockmeyer", title = "Parallel algorithms for term matching", booktitle = "Proc. Eighth International Conference on Automated Deduction", year = 1986, editor = "J. H. Siekmann", series = "Lecture Notes in Computer Science 230", pages = "416-430", publisher = S-V} @inproceedings{DM85, author = "P. Dembinski and J. Maluszynski", title = "{AND}-Parallelism with Intelligent Backtracking for Annotated Logic Programs", booktitle = "Proceedings of the International Symposium on Logic Programming", pages = "29-38", address = "Boston", year = 1985 } @ARTICLE { DM88 , AUTHOR = "W. Drabent and J. Maluszynski", TITLE = "Inductive assertion method for logic programs", JOURNAL = TCS, YEAR = "1988", MONTH = "", VOLUME = "59", NUMBER = "", PAGES = "133-155", ANNOTE = ""} @Article{DPMP95, refkey = "C1345", title = "Negation as Instantiation", author = "Alessandra Di Pierro and Maurizio Martelli and Catuscia Palamidessi", pages = "263--278", journal = "Information and Computation", year = "1995", volume = "120", number = "2", abstract = "We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called ``Negation As Instantiation{"} (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. The set of the atoms whose negation is inferred by the NAI rule is proved equivalent to the complement of $T_C\!\downarrow\!\omega$, where $T_C$ is the immediate consequence operator extended to non-ground atoms (Falaschi et al., 1989). The NAI rule subsumes negation as failure on ground atoms, it excludes floundering and can be efficiently implemented. We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness."} @inproceedings{Dra87, author = {W. Drabent}, title = {Do Logic Programs Resemble Programs in Conventional Languages?}, booktitle ={Proc. Int'l Symposium on Logic Programming}, editor = {E. Wada}, pages = "389-396", publisher = {IEEE Computer Society}, year = {1987}} @inproceedings{Dr87, author = {W. Drabent}, title = {Do Logic Programs Resemble Programs in Conventional Languages ?}, booktitle ={Proc. Int'l Symposium on Logic Programming}, editor = {E. Wada}, pages = "389-396", publisher = {IEEE Computer Society}, year = {1987}} %%E @TechReport{EBC98techrep, author = "S. Etalle and A. Bossi and N. Cocco", title = {Well-Terminating Programs}, institution = "Dip.\ di Informatica, Universit\`a di Venezia", year = "1998", number = "CS798" } @Article{EBC99, author = "S. Etalle and A. Bossi and N. Cocco", title = {Termination of well-moded programs}, year = "1999", journal = jlp, volume = "38", number = "2", pages = "243-257" } @Misc{eclipse, OPTkey = {}, OPTauthor = {}, title = {The ECLiPSe Constraint Logic Programming System}, howpublished = {http://www.icparc.ic.ac.uk/eclipse/index.html}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @TechReport{BCE00-techrep, author = {A. Bossi and N. Cocco and S. Etalle}, title = {A Transformation System Preserving Left Termination and Well-Termination}, institution = {Universit\`a di Venezia}, year = {2000} } @TechReport{EG95-techrep, author = "S. Etalle and M. Gabbrielli", title = "{T}ransformations of {C}{L}{P} {M}odules", INSTITUTION = "CWI, Amsterdam", year = "1994", number = "CS-R9515"} @InProceedings{EG94-gulp, author = "S. Etalle and M. Gabbrielli", title = "{M}odular {T}ransformations of {C}{L}{P} {P}rograms", booktitle = gulpro94, year = "1994", editor = edgulpro94} @InProceedings{EG94-workshop, author = "S. Etalle and M. Gabbrielli", title = "{M}odular {T}ransformations of {C}{L}{P} {P}rograms", booktitle = "Proc. of Post-ILPS'94 Workshop on Constraints and Databases", year = "1994", editor = "P. Revesz, D. Srivastava, P. Stuckey, S. Sudarshan", note = "available on www at http://www.research.att.com/~sudarsha/ILPS94-CDBWorkshop.html"} @InProceedings{EG95, author = "S. Etalle and M. Gabbrielli", title = "A Transformation System for Modular {CLP} Programs", pages = "681--696", ISBN = "0-262-69177-9", editor = "L. Sterling", booktitle = "Proc. of the 12th Int. Conf. on Logic Programming", publisher = "MIT Press", address = "Cambridge", year = "1995", } @InProceedings{EG95-pepm, author = "S. Etalle and M. Gabbrielli", title = "The Replacement Operation for {C}{L}{P} Modules", booktitle = "ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '95)", year = 1995, pages = "168-177", publisher = "ACM press", editor = "N. Jones"} @Article{EG96-tcs, author = "S. Etalle and M. Gabbrielli", title = "Transformations of {C}{L}{P} Modules", journal = tcs, year = "1996", volume = "166", number = "1", pages = "101-146", issn = "0304-3975"} @Article{EG96-jflp, author = "S. Etalle and M. Gabbrielli", title = "On the Correctness of the Replacement Operation for CLP Modules", journal = "Journal of Functional and Logic Programming", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", month = "February", issn = "1080-5230", note = "available at http://danae.uni-muenster.de/lehre/kuchen/JFLP/", } @InProceedings{EG96-workshop, author = "S. Etalle and M. Gabbrielli", title = "Layered Modes", editor = "F. de Boer and M. Gabbrielli", booktitle = "Proc. JICSLP'96 Post-Conference Workshop on Verification and Analysis of Logic Programs", note = "Tehcnical Report TR-96-31, Dipartimento di Informatica di Pisa", year = "1996" } @Article{EG98, author = "S. Etalle and M. Gabbrieli", title = "Partial evaluation of concurrent constraint languages", journal = "ACM Computing Surveys", volume = "30", number = "3es", month = "September", year = "1998", coden = "CMSVAN", ISSN = "0360-0300", note = "Article 11.", annote = "Available at \verb+http://www.acm.org:80/pubs/citations/journals/surveys/1998-30-3es/a11-etalle/+"} @Article{EG99, author = "Sandro Etalle and Maurizio Gabbrieli", title = "Layered Modes", journal = "The Journal of Logic Programming", year = "1999", volume = "39", number = "1--3", pages = "225--244" } @InProceedings{EGM97, author = "S.~Etalle and M.~Gabbrielli and E.~Marchiori", title = "A {T}ransformation {S}ystem for {C}{L}{P} with {D}ynamic {S}cheduling and {C}{C}{P}", year = "1997", OPTISSN = "0362-1340", booktitle = "ACM--SIGPLAN Symposium on Partial Evaluation and Semantic Based Program Manipulation", editor = "C. Consel", publisher = "ACM Press" } @Article{EGM97-sigplan, author = {S.~Etalle and M.~Gabbrielli and E.~Marchiori}, title = {A {T}ransformation {S}ystem for {C}{L}{P} with {D}ynamic {S}cheduling and {C}{C}{P}}, journal = {ACM SIGPLAN Notices}, year = {1997}, volume = {32}, number = {12}, pages = {137--150}, ISBN={0-89791-917-3}, note = http://doi.acm.org/10.1145/258994.259014}} @InProceedings{EGM98, author = "S.~Etalle and M.~Gabbrielli and M.~C.~Meo", title = "{Unfold/Fold Transformations of CCP Programs}", year = "1998", booktitle = "CONCUR98 -- 1998 International Conference on Concurrency Theory", series = "LNCS 1466", pages = "348--363", ISSN = "0302-9743", editor = "D.~Sangiorgi and R. de Simone", publisher = s-v } @Article{EGM01, author = "S.~Etalle and M.~Gabbrielli and M.~C.~Meo", title = {Transformations of CCP programs}, journal = {ACM Transactions on Programming Languages and Systems}, year = {2001}, volume = "23", number = "3", pages = "304--395", note = {Available also at CoRR http://arXiv.org/}} @TechReport{EM00-techrep, author = {S. Etalle and J. Mountjoy}, title = {The Lazy Functional Side of Logic Programming}, institution = {Universiteit Maastricht}, year = {2000}, number = {CS 00-02}, note = {Available at the CoRR at the address http://arXiv.org/abs/cs/0003070} } @InProceedings{ET96, author = "S.~Etalle and F.~Teusink", title = "A Compositional Semantics for Normal Open Programs", year = "1996", booktitle = "Joint Intermational Conference and Symposium on Logic Programming", editor = "M. Maher", pages = "468--482", ISBN = "0-262-63173-3", publisher = "The MIT press", } @techreport{EHV98, author = {S. Etalle and P. H. Hartel and W. G. Vree}, title = {Declarative solutions to partitioned-grid problems}, institution = {Dept. of Electr. and Comp. Sci, Univ. of Southampton, England}, type = {Technical report}, number = {DSSE-TR-98-12}, month = {Nov}, year = {1998}, url = {www.dsse.ecs.soton.ac.uk/techreports/98-12.html}} @MISC {Eta91, AUTHOR = "S. Etalle", TITLE = "Transformazione dei programmi logici con negazione, {T}esi di {L}aurea, {D}ip. {M}atematica {P}ura e {A}pplicata, {U}niversit\`{a} di {P}adova, {P}adova, {I}taly", HOWUBLISHED = "Tesi di Laurea, Universit\`{a} di Padova", YEAR = "1991", MONTH = "July"} @TechReport{Eta94, author = "S. Etalle", title = "More (on) Unification-Free Prolog Programs", institution = "CWI, Amsterdam", year = 1994, number = "CS-R9454", month = "September", note = "The final version will appear on ``Journal of Programming Languages.'' Chapman \& Hall, London" } @PhdThesis{Eta95, author = {S. Etalle}, title = {Transformation and Analysis of (Constraint) Logic Programs}, school = {ILLC - University of Amsterdam}, year = {1995}} @Article{Eta96, author = "S. Etalle", title = "Unification-Free Prolog Programs Revisited", journal = "Journal of Programming Languages", year = "1996", volume = "4", OPTnumber = "4", pages = "187-210", OPTmonth = "", note = "Available at http://compscinet.dcs.kcl.ac.uk/JP/PDFPapers/jp040401.pdf" } @Article{Eta, author = "S. Etalle", title = "A Semantics for Modular General Logic Programs", journal = "Theoretical Computer Science", note = "To Appear" } @Article{Eta98, title = "A semantics for modular general logic programs", author = "S. Etalle", pages = "51--80", journal = "Theoretical Computer Science", year = "1998", volume = "206", number = "1--2", note = "Fundamental Study", references = "\cite{JLOGP::AptB1994} \cite{POPL::BossiBGLM1993} \cite{JLOGC::BossiCE1996} \cite{TCS::BossiGLM1994} \cite{JLOGP::BugliesiLM1994} \cite{JLOGP::Fitting1985} \cite{JLOGC::GabbrielliDL1995} \cite{POPL::GaifmanS1989} \cite{POPL::JaffarL1987} \cite{JLOGP::JaffarM1994} \cite{JLOGP::Kunen1987} \cite{TCS::LassezM1984} \cite{TCS::Maher1993} \cite{JLOGP::Miller1989} \cite{TCS::Sato1992} \cite{PODS::GelderRS1988}", } @InProceedings{EvR98, author = "S. Etalle and F. van Raamsdonk", title = "Beyond Success and Failure", pages = "190--204", ISBN = "0-262-60031-5", editor = "J. Jaffar", booktitle = "Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming ({JICSLP}-98)", month = jun # "15--19~", publisher = "MIT Press", OPTaddress = "Cambridge", year = "1998", ISBN = "0-262-60031-5"} @InProceedings{EvR99, author = "S. Etalle and F. van Raamsdonk", title = "Logic Programming with Requests", pages = "558--572", ISSN = "1061-0464", ISBN = "0-262-54104-1", editor = "D. De Schreye", booktitle = "Proceedings of the 1999 International Conference and on Logic Programming ({ICLP}-99)", publisher = "MIT Press", OPTaddress = "Cambridge", year = "1999" } %%F @InProceedings{FAM96b, author = "S. Abdennadher and Th. Fr{\"u}hwirth and H. Meuss", title = "On Confluence of Constraint Handling Rules", series = "LNCS 1118", booktitle = "Second International Conference on Principles and Practice of Constraint Programming (CP'96)", publisher = "Springer", year = "1996", url = "http://www.pms.informatik.uni-muenchen.de/publikationen/PMS-FB/PMS-FB-1996-8.ps.gz", } @Article{FGMP97, author = {M.~Falaschi and M.~Gabbrielli and K.~Marriot and C.~Palamidessi}, title = {Constraint logic programming with dynamic scheduling: a semantics based on closure operators}, journal = {Information and Computation}, year = {1997}, volume = {137}, number = {1}, pages = {41-67}} @ARTICLE {Fit85, AUTHOR = {M. Fitting}, TITLE = {A {K}ripke-{K}leene semantics for {L}ogic {P}rograms}, JOURNAL = "Journal of Logic Programming", YEAR = 1985, volume = 2, number = 4, pages = "295-312", ANNOTE = ""} @INPROCEEDINGS{FL95, author = "G\'{e}rard Ferrand and Arnaud Lallouet", title = "A Compositional Proof Method of Partial Correctness for Normal Logic Programs", booktitle = "Proceedings of the International Logic Programming Symposium", editor = "John Lloyd", year = "1995", pages = "209-223" } @InProceedings {FLMP88, author = "M. Falaschi and G. Levi and M. Martelli and C. Palamidessi", title = "A new declarative semantics for logic languages", booktitle = "ICLP '88", year = 1988, pages = "993-1005", publisher = "The Mit Press"} @ARTICLE {FLMP89a, AUTHOR = "M. Falaschi and G. Levi and M. Martelli and C. Palamidessi", TITLE = {Declarative Modeling of the Operational Behavior of Logic Languages}, JOURNAL = TCS, YEAR = "1989", MONTH = "", VOLUME = "69", NUMBER = "3", PAGES = "289-318", ANNOTE = ""} @article{FLMP89b, author = {M. Falaschi and G. Levi and M. Martelli and C. Palamidessi}, title = "A {M}odel-{T}heoretic {R}econstruction of the {O}perational {S}emantics of {L}ogic {P}rograms", year = {1993}, journal= {Information and Computation}, volume= 102, number=1, pages="86-113"} @Article{FW92, key = "Freuder \&{} Wallace", author = "E. C. Freuder and R. J. Wallace", title = "Partial Constraint Satisfaction", journal = "Artificial Intelligence", pages = "21--70", volume = "58", number = "1-3", OPTmonth = dec, year = "1992" } @InCollection{Fru95, author = "Thom Fr{\"{u}}hwirth", title = "{Constraint Handling Rules}", booktitle = "Constraint Programming: Basics and Trends", editor = "Andreas Podelski", publisher = "Springer", series = "LNCS 910", year = "1995", OPTnote = "(Ch{\^{a}}tillon-sur-Seine Spring School, France, May 1994)"} @Article{Fru98, author = "Th. Fr{\"u}hwirth", title = "Theory and Practice of Constraint Handling Rules, Special Issue on Constraint Logic Programming", editors = "P. Stuckey and K. Marriot", journal = "Journal of Logic Programming", volume = "19-20", number = "1", pages = "95--138", year = "1998", url = "http://www.pst.informatik.uni-muenchen.de/personen/fruehwir/drafts/jlp-chr1.ps.Z", } %%G @phdthesis{Gab92, author = {M. Gabbrielli}, title = {The semantics of Logic Programming as a Programming Language}, school = {Universit\`a di {P}isa}, year = {1992}} @TechReport{Gal91, author = {J. P. Gallagher}, title = {A System for Specializing Logic Programs}, institution = {University of Bristol}, year = {1991}, number = {91-32}} @Article{GB91, author = {J. P. Gallagher and M. Bruynooghe}, title = {The Derivation of an Algorithm for Program Specialisation}, journal = {New Generation Computing}, year = {1991}, volume = {9}, number = {3/4}, pages = {305-334} } @article{GDL95, author = {M. Gabbrielli and G.M. Dore and G. Levi}, title = {Observable {S}emantics for {C}onstraint {L}ogic {P}rograms}, journal = jlc, volume = "5", number = "2", pages = "133-171", year = {1995}} @inproceedings{GL88, author = "M. Gelfond and V. Lifshitz", title = "The {S}table {M}odel {S}emantics for {L}ogic {P}rograms", booktitle = "Fifth international Conference and Symposium on Logic programming, Seattle, U.S.A.", year = "1988", pages = "1070-1080", publisher = "", OPTnote = ""} @inproceedings{Gla90b, author={R.J. van Glabbeek}, title={The Linear Time - Branching Time spectrum}, booktitle={Proc. of CONCUR 90}, editor = {J.C.M. Baeten and J.W. Klop}, pages = {278-297}, publisher = {Springer-Verlag}, series = lncs, volume = 458, address = {Amsterdam}, Year = 1990} @InProceedings{GM97, author = "M. Gengler and M. Martel", title = "Self-Applicable Partial Evaluation for Pi-Calculus", pages = "36--46", OPTISSN = "0362-1340", booktitle = "Proceedings of the {ACM} {SIGPLAN} Symposium on Partial Evaluation and Semantics-Based Program Manipulation ({PEPM}-97)", series = "ACM SIGPLAN Notices", volume = "32, 12", publisher = "ACM Press", address = "New York", year = "1997"} @inproceedings{GMS95, author = {M. Garcia de la Banda and K. Marriott and P. Stuckey}, title = {Efficient Analysis of Logic Programs with Dynamic Scheduling}, pages = "417-431", booktitle = ilps95, editor = edilps95, publisher = { MIT Press}, year = {1995}} @book{Gr87, author = "S. Gregory", title = {Parallel {L}ogic {P}rogramming in {PARLOG}: the {L}anguage and its {I}mplementation}, publisher = "Addison-Wesley", year = "1987"} @inproceedings{GRS88, author = {A. van Gelder and K. Ross and J. S. Schlipf}, title = {Unfounded {S}ets and {W}ell-{F}ounded {S}emantics for {G}eneral {P}rograms}, booktitle = "Proc. ACM Symp. on Principles of Database Systems", year = "1988", publisher = "ACM", pages = {221-230} } @InCollection{GS91, author = "P.A. Gardner and J.C. Shepherdson", title = "Unfold/Fold Transformations of Logic Programs", booktitle = "Computational Logic: Essays in Honor of Alan Robinson", publisher = mit, year = "1991", editor = "J-L Lassez and G. Plotkin"} @inproceedings{GS89a, author = {H. Gaifman and E. Shapiro}, title = {Fully Abstract Compositional Semantics for Logic Programs}, booktitle = popl89, publisher = {ACM}, year = {1989}, pages = {134-142} } @InProceedings{GW92, author = "H. Ganzinger and U. Waldmann", title = "{Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems}", pages = "430--437", year = "1992", OPTmonth = jul # "~8--10,", editor = "Micha{\"e}l Rusinowitch and Jean-Luc R{\'e}my", booktitle = "Conditional Term Rewriting Systems, Third International Workshop", OPTaddress = "Pont-{\`a}-Mousson, France", series = "LNCS 656", publisher = "Springer-Verlag", } %%H @ARTICLE{Han94, author = "Hanus, M.", title = "The Integration of Functions into Logic Programming: From Theory to Practice", year = "1994", journal = "Journal of Logic Programming", volume = "19\&20", pages = "583-628", abstract = { Functional and logic programming are the most important declarative programming paradigms, and interest in combining them has grown over the last decade. Early research concentrated on the definition and improvement of execution principles for such integrated languages, while more recently efficient implementations of these execution principles have been developed so that these languages became relevant for practical applications. In this paper we survey the development of the operational semantics as well as the improvement of the implementation of functional logic languages. } } @INPROCEEDINGS{Han95LOPSTR, author = "Hanus, M.", title = "Efficient Translation of Lazy Functional Logic Programs into Prolog", year = "1995", pages = "252-266", publisher = "Springer LNCS 1048", booktitle = "Proc.\ Fifth International Workshop on Logic Program Synthesis and Transformation", abstract = { In this paper, we present a high-level implementation of lazy functional logic programs by transforming them into Prolog programs. The transformation is controlled by generalized definitional trees which specify the narrowing strategy to be implemented. Since we consider a sophisticated narrowing strategy, a direct mapping of functions into predicates is not possible. Therefore, we present new techniques to reduce the interpretational overhead of the generated Prolog code. This leads to a portable and efficient implementation of functional logic programs. }, } @INPROCEEDINGS{Han95ICLP, author = "Hanus, M.", title = "On Extra Variables in (Equational) Logic Programming", year = "1995", booktitle = "Proc. Twelfth International Conference on Logic Programming", publisher = "MIT Press", pages = "665-679", abstract = { Extra variables in a clause are variables which occur in the body but not in the head. It has been argued that extra variables are necessary and contribute to the expressive power of logic languages. In the first part of this paper, we show that this is not true in general. For this purpose, we provide a simple syntactic transformation of each logic program into a logic program without extra variables, and we show a strong correspondence between the original and the transformed program. In the second and main part of this paper, we use a similar technique to provide new completeness results for equational logic programs with extra variables. In equational logic programming it is well known that extra variables cause problems since narrowing, the standard operational semantics for equational logic programming, may become incomplete in the presence of extra variables. Using a simple syntactic transformation, we derive a number of new completeness results for narrowing. In particular, we show the completeness of narrowing strategies in the presence of nonterminating functions and extra variables in right-hand sides of rewrite rules. Using these results, current functional logic languages can be extended in a practically useful way. } } @INPROCEEDINGS{Han97POPL, author = "Hanus, M.", title = "A Unified Computation Model for Functional and Logic Programming", year = "1997", booktitle = "Proc. 24st ACM Symposium on Principles of Programming Languages (POPL'97)", pages = "80-93", abstract = { We propose a new computation model which combines the operational principles of functional languages (reduction), logic languages (non-deterministic search for solutions), and integrated functional logic languages (residuation and narrowing). This computation model combines efficient evaluation principles of functional languages with the problem-solving capabilities of logic programming. Since the model allows the delay of function calls which are not sufficiently instantiated, it also supports a concurrent style of programming. We provide soundness and completeness results and show that known evaluation principles of functional logic languages are particular instances of this model. Thus, our model is a suitable basis for future declarative programming languages. } } @InProceedings{HSC96, author = "F. Henderson and Z. Somogyi and T. Conway", title = {Determinism analysis in the Mercury compiler}, pages = "337-346", booktitle = "Australian Computer Science Conference", year = "1996", note = "Available at http://www.cs.mu.oz.au/mercury/papers.html" } @book{vH89, author = "Pascal {Van Hentenryck}", title = "Constraint Satisfaction in Logic Programming", year = 1989, publisher = "MIT Press", address = "Cambridge, MA", isbn = "0-262-08181-4", } @InProceedings{vH97, author = "Pascal {Van Hentenryck}", title = "Numerica: A Modeling Language for Global Optimization ", editor = edijcai97, OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = ijcai97, year = 1997, OPTpublisher = "", note = "Invited talk", OPTannote = "" } @techrep{Hi74, author = "R. Hill", title = "{L}{U}{S}{H}-{R}esolution and its {C}ompleteness" , INSTITUTION = "Department of {A}rtificial {I}ntelligence, {U}niversity of {E}dinnburgh", number = "{M}emo 78", year = "1974"} @InProceedings{HKY96, author = {H. Hosoya and N. Kobayashi and A. Yonezawa}, title = {Partial evaluation scheme for concurrent languages and its correctness}, booktitle = {Euro-Par'96}, pages = {625-632}, year = {1996}, editor = {L.~Boug{\'e} et~al.}, number = {1123}, series = {LNCS}, publisher = S-V} @Book{HL94, author = "P. M. Hill and J. W. Lloyd", title = "The G{\"o}del programming language", publisher = "The MIT Press", year = "1994" } @ARTICLE { Hog81, AUTHOR = "C.J. Hogger", TITLE = "Derivation of Logic Programs", JOURNAL = JACM, YEAR = "1981", MONTH = "April", VOLUME = "28", NUMBER = "2", PAGES = "372-392", ANNOTE = ""} @PhdThesis{Hos98, author = {H. Hosobe}, title = {Theoretical Properties and Efficient Satisfaction of Hierarchical Constraint Systems}, school = {Dept. of Computer Science, University of Tokyo}, year = {1998}} @inproceedings{HMS87, author = "Nevin Heintze and Spiro Michaylov and Peter J. Stuckey", title = "{CLP(${\cal R}$)} and Some Electrical Engineering Problems", booktitle = "{ICLP'87}: Proceedings 4th International Conference on Logic Programming", address = "Melbourne, Victoria, Australia", pages = "675--703", month = may, year = 1987, publisher = "MIT Press", editor = "Jean-Louis Lassez", note = "Also in Journal of Automated Reasoning vol.\ 9, pages 231--260, October 1992", } @Article{HMS92, author = "Nevin Heintze and Spiro Michaylov and Peter J. Stuckey", title = "{CLP(${\cal R}$)} and Some Electrical Engineering Problems", OPTcrossref = "", OPTkey = "", journal = "Journal of Automated Reasoning", year = "1992", volume = "9", number = "2", pages = "231-260", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{HMT71, author = "L.~Henkin and J.D. Monk, and A.~Tarski", title = "Cylindric Algebras (Part I)", publisher = "North-Holland", year = "1971"} @BOOK {Hog84, AUTHOR = "C.J. Hogger", TITLE = "Introduction to Logic Programming", PUBLISHER = AP, YEAR = "1984", NOTE = "", ANNOTE = ""} @ARTICLE{HP92, AUTHOR = {P. Hudak (ed) and S. L. {Peyton Jones} (ed) and P. L. Wadler (ed)}, JOURNAL = {ACM SIGPLAN notices}, MONTH = {May}, NUMBER = {5}, PAGES = {1-162}, TITLE = {Report on the programming language {Haskell} -- A non-strict purely functional language, Version 1.2}, VOLUME = {27}, YEAR = {1992} } @ARTICLE{HPW92, AUTHOR = {P. Hudak (ed) and S. L. {Peyton Jones} (ed) and P. L. Wadler (ed)}, JOURNAL = {ACM SIGPLAN notices}, MONTH = {May}, NUMBER = {5}, PAGES = {1-162}, TITLE = {Report on the programming language {Haskell} -- A non-strict purely functional language, Version 1.2}, VOLUME = {27}, YEAR = {1992} } %%I %%J @techreport{JL86, author = "J. Jaffar and J.-L. Lassez", title = {Constraint {L}ogic {P}rogramming}, institution = {Department of Computer Science, Monash University}, year = "June 1986"} @inproceedings{JL87, author = "J. Jaffar and J.-L. Lassez", title = {Constraint {L}ogic {P}rogramming}, booktitle = popl87, pages ="111-119", publisher = {ACM}, year = "1987"} @article{JM94, author = "Joxan Jaffar and Michael J. Maher", title = "Constraint Logic Programming: A Survey", journal = jlp, year = 1994, volume = "19/20", pages = "503--581", } @InProceedings{JMM91, author = "Niels J\o{}rgensen and Kim Marriott and Spiro Michaylov", title = "Some global compile-time optimizations for {CLP(${\cal R}$)}", editor = "Vijay Saraswat and Kazunori Ueda", pages = "420--434", booktitle = "International Logic Programming Symposium", year = "1991", OPTorganization = "", publisher = "MIT Press", address = "San Diego" } @ARTICLE {JMS92, AUTHOR = "J. Jaffar and S. Michaylov and P. Stuckey", TITLE = "The CLP($\cal R$) language and System", JOURNAL = toplas, YEAR = "1992", MONTH = "July", VOLUME = "14", NUMBER = "3", PAGES = "339-395", ANNOTE = ""} @inproceedings{JM84, author = {N. Jones and A. Mycroft}, title = {Stepwise {D}evelopment of {O}perational and {D}enotational {S}emantics for {P}rolog}, booktitle = iclp84, editor = ediclp84, pages = {281-288}, year = 1984}} %%K @BOOK {Kle52, AUTHOR = "S.C. Kleene", TITLE = "Introduction to Metamathematics", PUBLISHER = "D. van Nostrand", ADDRESS = "Princeton, New Jersey", YEAR = "1952", ANNOTE = "A profound treatment of recursive function theory, this book studies properties of the class of partial recursive functions and operations on codes for functions in much detail. Among other things, the S-m-n theorem, enumeration, and the first and second recursion theorems are treated."} @TechReport{KS94, author = "M. R. K. Krishna Rao and R. K. Shyamasundar", title = "Unification-free Execution of Well-Moded Prolog Programs", INSTITUTION = "TIFR, Bombay, India", month = "March", year = "1994"} @inproceedings{KK88, author = "T. Kawamura and T. Kanamori", title = {Preservation of {S}tronger {E}quivalence in {U}nfold/{F}old {L}ogic {P}rogramming {T}ransformation}, booktitle = fgcs88, pages = "413-422", organization = icot, year = "1988"} @article{KK90, author = "T. Kawamura and T. Kanamori", title = {Preservation of {S}tronger {E}quivalence in {U}nfold/{F}old {L}ogic {P}rogramming {T}ransformation}, journal = TCS, volume = 75, number = "1\&2", year = 1990, pages = {139-156}} @inproceedings{Kom82, author = "H. Komorowski", title = {Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of {P}rolog.}, booktitle = {\em Ninth ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico}, pages = "255--267", organization = "ACM", year = "1982"} @Article{Kow79, author = {R.~A.~Kowalski}, title = {{A}lgorithm = {L}ogic + {C}ontrol}, journal = {Communications of the ACM}, year = 1979, volume = 22, number = 7, pages = {424--436}} @article{Kun87, author = {K. Kunen}, title = {Negation in {L}ogic {P}rogramming}, journal = JLP, volume = 4, year = 1987, pages = {289-308}} %%L @InProceedings{Lau93, author ="J. Launchbury", booktitle = "Principles of Programming Languages", title= "{A} Natural Semantics for Lazy Evaluation", year= "1993", abstract-url= "http://www.cse.ogi.edu/~jl/biblio.html", address= "Charleston", url= "http://www.cse.ogi.edu/~jl/Papers/lazySem.ps", scope= "defin" } @Article{LAY87, author = "C.~Lassez and K.~McAloon and R.~Yap", title = "Constraint {L}ogic {P}rogramming and {O}ption {T}rading", journal = "IEEE Expert", year = "1987", volume = "2", number = "3", pages = "42-50" } @book{Llo87, author = "J. W. Lloyd", title = "Foundations of {L}ogic {P}rogramming", note = "Second edition", OPTSERIES = "Symbolic Computation -- Artificial Intelligence", publisher = springer, year = "1987"} @article{LM84, author = "J.-L. Lassez and M. J. Maher", title = "Closures and {F}airness in the {S}emantics of {P}rogramming {L}ogic", journal = tcs, volume = "29", pages = "167-184", year = "1984"} @TechReport {LM88, author = "G. Levi and P. Mancarella", title = "The unfolding semantics of logic programs", institution = "Dipartimento di Informatica, Universit\'{a} di Pisa, Italy", year = "1988", number = "13/88", month = "September"} @incollection{LMM88, author = "J.-L. Lassez and M. J. Maher and K. Marriott", title = {Unification {R}evisited}, booktitle = "Foundations of Deductive Databases and Logic Programming", editor = "J. Minker", publisher = "Morgan Kaufmann, Los Altos, Ca.", year = "1988", pages = "587-625"} @InProceedings{LMS97, author = {M, Leuschel and B. Martens and K. Sagonas}, title = {Preserving Termination of Tabled Logic Programs While Unfolding}, booktitle = {LOPSTR'97, Logic Program Synthesis and Transformation}, pages = {189-205}, year = {1997}, editor = {N. Fuchs}, OPTvolume = {}, OPTnumber = {}, OPTseries = {LNCS}, publisher = {Springer-Verlag}, OPTnote = {We provide a first investigation of the specialisation and transformation of tabled logic programs through unfolding. We show that - surprisingly - unfolding, even determinate, can worsen the termination behaviour in the context of tabling. We therefore establish two criteria which ensure that such mishaps are avoided. We also briefly discuss the influence of some other transformation techniques on the termination and efficiency of tabled logic programs.}} @InProceedings{LM99, author = {M. Leuschel and T. Massart}, title = {Infinite State Model Checking by Abstract Interpretation and Program Specialisation}, booktitle = lopstr99, pages = {63-82}, year = {1999}, editor = {A. Bossi}, number = {1817}, series = {LNCS}, publisher = {Springer-Verlag}} @TechReport{LM00, author = "M. Leuschel and T. Massart", title = "How to Make {FDR} Spin, {LTL} Model Checking of {CSP} by Refinement", institution = "ULB", year = "2000", number = "426", abstract = "We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying certain temporal properties. To remedy this problem, we show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between {"}classical{"} model checking and refinement checking.", keywords = "CSP,LTL,FDR,Refinement", postscript = "http://www.ulb.ac.be/di/ssd/tmassart/pub/ltl-fdr-fme2001.ps", } @Article{LS88, author = "A.~Lakhotia and L.~Sterling", title = "Composing recursive logic programs with clausal join", journal = "New Generation Computing", year = "1988", volume = "6", number = "2,3", pages = "211-225", } @article{LS91, author = {J. W. Lloyd and J. C. Shepherdson}, title = {Partial {E}valuation in {L}ogic {P}rogramming}, journal = jlp, volume = 11, pages = {217-242}, year = 1991}} @InProceedings{Lut90, author = {S. L\"{u}ttringhaus-Kappel}, title = "An Experiment in Using When-Declarations to Control Unfolding of Logic Programs", booktitle = "ICLP Workshop on Partial Deduction and Partial Evaluation", year = "1990", note = "http://www.informatik.uni-bonn.de/~stefan/Papers-WWW/publications.html" } @MastersThesis{Lui94, author = {I. Luitjes}, title = {Logic Programming and dynamic selection rules}, school = {University of Amsterdam}, year = {1994} } @inproceedings{Lut93, author = {S. L\"{u}ttringhaus-Kappel}, title = {Control Generation for Logic Programs}, booktitle = iclp93, editor = ediclp93, pages = "478-495", publisher = { MIT Press} , year = {1993}} @PhdThesis{Lut92, author = {S. L\"{u}ttringhaus-Kappel}, title = {Laziness in Logic Programming}, school = {Friedrich-Wilhelms-Universit\"at Bonn}, year = {1992}, OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } %%M @InProceedings{MK97, author = {J.~C. Martin and A.~M. King}, booktitle = {Proc.\ Tapsoft'97}, title = {Generating Efficient, Terminating Logic Programs}, pages = {273-184}, year = {1997}, editor = {M.~Bidoit and M.~Dauchet}, OPTnumber = {}, series = {LNCS}, publisher = S-V } @phdthesis{Mah85, author = {M. Maher}, title = {Semantics of {L}ogic {P}rogramming}, school = {University of Melbourne, Computer Science Department}, year = {1985}} @TechReport{Mah87, author = "M.J. Maher", title = "Correctness of a Logic Program Transformation System", institution = "T.J. Watson Research Center", type ="IBM Research Report", number ="RC13496", year = "1987"} @inproceedings{Mah87b, author = "M. J. Maher", title = "Logic semantics for a class of committed-choice programs", editor = ediclp87, booktitle = iclp87, pages= "858-876", publisher = mit, year = "1987"} @InCollection{Mah88, author = "M.J. Maher", title = "Equivalences of Logic Programs", booktitle = "Foundation of Deductive Databases and Logic Programming", publisher = "Morgan Kaufmann", year = "1988", editor = "J. Minker, editor", pages = "627-658"} @inproceedings{Mah89, author = "M.J. Maher", title = "A Transformation System for Deductive Databases Modules with Perfect Model Semantics", booktitle = "Proceedings of the 9th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India. LNCS 405.", year = "1989", pages = "", publisher = "Sringer-Verlag", OPTnote = "to appear on Theoretical Computer Science"} @TechReport{Mah90, author = "M.J. Maher", title = "Reasonings about {S}table Models (and other Unstable Semantics)", institution = "T.J. Watson Research Center", type = "IBM Research Report", year = "1990"} @inproceedings{Mah92, author = "M. J. Maher", title = "A {C}{L}{P} view of {L}ogic {P}rogramming", booktitle = {Proc. of the Third Int'l Conf. on Algebraic and Logic Programming}, series = lncs, publisher= springer, editor = "H. Kirchner and G. Levi", year = {1992}, volume = 632, pages = "364-383"} @article {Mah93, author = "M.J. Maher", title = "A Transformation System for Deductive Databases with Perfect Model Semantics", journal = tcs, year = "1993", month = "March", volume = "110", number = "2", pages = "377-403", annote = ""} @unpublished {Mah2, author = "M.J. Maher", title = "Reasonings about {S}table Models (and other Unstable Semantics), submitted for publication"} @Article{Mar97, author = {K. Marriot}, title = {Algebraic and logical semantics for CLP languages with dynamic scheduling}, journal = {Journal of Logic Programming}, year = {1997}, volume = {32}, number = {1}, pages = {71-84}} @inproceedings{Mar94, author ="M. Marchiori", title = "Localizations of Unification Freedom through Matching Directions", booktitle = ilps94, year = 1994, editor = edilps94, publisher = "MIT Press"} % pages = "37-51" @InProceedings{Mar94-trs, title = "{Logic Programs as Term Rewriting Systems}", author = "M.~ Marchiori", pages = "223--241", editor = "Giorgio Levi and Mario Rodr{\'\i}guez-Artalejo", booktitle = "Algebraic and Logic Programming, 4th International Conference, {ALP}'94", OPTaddress = "Madrid, Spain", OPTmonth = "14--16 " # sep, year = "1994", series = "lncs", volume = "850", publisher = S-V } @InProceedings{Mar95, author = "M. Marchiori", title = "{The Functional Side of Logic Programming}", booktitle = "Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture ({FPCA}'95)", address = "La Jolla, California", publisher = "ACM Press", year = "1995", pages = "55--65" } @Article{Mel85, author = "C. S. Mellish", title = "Some global optimizations for a Prolog compiler", journal = jlp, year = "1985", volume = "2", number = "1", pages = "43-66", month = "April" } @TechReport{Mel81, Author ="C. S. Mellish", Title ={{T}he {A}utomatic {G}eneration of {M}ode {D}eclarations for {P}rolog {P}rograms}, Type ={DAI Research Paper}, Number ={163}, Institution ={Department of Artificial Intelligence, Univ. of Edinburgh}, Month ={August}, Year =1981 } @InProceedings{MG97, author = "M. Marinescu and B. Goldberg", title = "Partial-Evaluation Techniques for Concurrent Programs", pages = "47--62", OPTISSN = "0362-1340", booktitle = "Proceedings of the {ACM} {SIGPLAN} Symposium on Partial Evaluation and Semantics-Based Program Manipulation ({PEPM}-97)", OPTmonth = jun # "~12--13", series = "ACM SIGPLAN Notices", volume = "32, 12", publisher = "ACM Press", address = "New York", year = "1997"} @inproceedings{MGH94, author = {K. Marriott and M. Garcia de la Banda and M. Hermenegildo}, title = {Analyzing Logic Programs with Dynamic Scheduling}, pages = "240-253", booktitle = popl94, publisher = { ACM Press}, year = {1994}} @inproceedings{Mil86, author = {D. Miller}, title = {A {T}heory of {M}odules for {L}ogic {P}rogramming}, booktitle={Proceedings IEEE Symposium on Logic Programming}, year=1986, pages={106-114}} @inproceedings{Mil89a, Author = "D. Miller", Title = "Lexical {S}coping as {U}niversal {Q}uantification", Booktitle = iclp89, Year = 1989, Publisher = mit, editor = ediclp89, pages = {268-283}} @article{Mil89, author = {D. Miller}, title = {A {L}ogical {A}nalysis of {M}odules in {L}ogic {P}rogramming}, journal=jlp, year=1989, volume=6, pages={79-108}} @Book{Miln89, author = "R.~Milner", title = "Communication and Concurrency", publisher = "Prentice-Hall", year = "1989"} @inproceedings{MK85, author = "J. Maluszynski and H. J. Komorowski", title = "Unification-free Execution of Logic Programs", booktitle = "Proceedings of the 1985 IEEE Symposium on Logic Programming", pages = "78-86", publisher = "IEEE Computer Society Press", address= "Boston", year = 1985 } @InProceedings{MS90, author = "K.~Marriott and H.~S{\o}ndergaard", title = "Analysis of constraint logic programs", editor = "Saumya Debray and Manuel Hermenegildo", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "531--547", booktitle = "Proceedings North American Conference on Logic Programming", year = "1990", OPTorganization = "", publisher = "MIT Press" } @InCollection{MS97, author = "T.~Mogensen and P.~Sestoft", title = "Partial Evaluation", booktitle = "Encyclopedia of Computer Science and Technology", year = "1997", editor = "A.~Kent and J.G.~Williams", publisher = "M.~Dekker", volume = "37", pages = "247-279" } @Article{MT92, author = "M.~Martelli and C.~Tricomi", title = "A new {SLDNF}-tree", journal = "Information Processing Letters", volume = "43", number = "2", pages = "57--62", year = "1992"} @inproceedings{MP88, author = "P. Mancarella and D. Pedreschi", title = "An {A}lgebra of {L}ogic {P}rograms", Booktitle = iclp88, Year = 1988, Publisher = mit, editor = ediclp88, pages = {1006-1023} } @inproceedings{MS93, author = "K. Marriott and P. J. Stuckey", title = "The 3 R's of Optimizing Constraint Logic Programs: Refinement, Removal and Reordering", booktitle = "{POPL'93}: Proceedings {ACM} {SIGPLAN} Symposium on Principles of Programming Languages", year = 1993, address = "Charleston", month = jan, } @article{MS93-ngc, author = "K. Marriot and H. Sondergaard", title = "Difference-list {T}ransformation for {P}rolog", journal = "New Generation Computing", volume = 11, pages = "125-177", year = "1993"} @Book{MS98, author = {K. Marriott and P. J. Stuckey}, title = {Programming with Constraints: An Introduction}, publisher = {The MIT Press}, year = {1998}} @inproceedings{MT95, author = {E. Marchiori and F. Teusink}, title = {Proving termination of Logic programs with Delay Declarations}, booktitle = ilps95, editor = edilps95, publisher = {MIT Press}, year = {1995} } %%N @inproceedings{Nec97, author = {G. C. Necula}, title = {Proof-carrying code}, booktitle = {Proc.\ 24th Symposium on Principles of programming languages ({POPL})}, publisher = {ACM, New York}, year = {1997}, pages = {106-119}} @TechReport{Nai82, author = "L. Naish", title = {An Introduction to MU-Prolog}, institution = "The University of Melbourne", year = "1982", number = "82/2" } @book{Na86, author = {L. Naish}, title = {Negation and {C}ontrol in {P}rolog}, publisher = springer, Year = 1986, series = lncs, volume = {238}} @book{Nai86, author = {L. Naish}, title = {Negation and control in {Prolog}}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, address = {New York}, number = {238}, year = {1986}, comment = {Technical report 85/12, Department of Computer Science, University of Melbourne} } @inproceedings{Nai88, author = {L. Naish}, title = {Parallelizing {NU-Prolog}}, booktitle = {Proceedings of the Fifth International Conference/Symposium on Logic Programming}, address = {Seattle, Washington}, year = {August 1988}, editor = {Kenneth A. Bowen and Robert A. Kowalski}, pages = {1546--1564}, comment = {Technical report 87/17, Department of Computer Science, University of Melbourne} } @techreport{Nai92, author = "L. Naish", title = {Coroutining and the Construction of Terminating Logic Programs}, institution = {Department of Computer Science, University of Melbourne}, number = {92/5}, year = {1992} } @Article{Nar86, author = "S.~Narain", title = {A technique for doing lazy evaluation in Prolog}, OPTcrossref = "", OPTkey = "", journal = jlp, year = "1986", volume = "3", number = "3", pages = "259-276" } %%O @inproceedings{OM94, author = "M.~A.~Orgun and W.~Ma", title = "An Overview of Temporal and Modal Logic Programming", booktitle = "Proceedings of {ICTL}'94: The 1st International Conference on Temporal Logic", publisher = "Springer-Verlag", editor = "D.~Gabbay and H.~Ohlbach", pages = "445--479", year = "1994", url = "citeseer.nj.nec.com/orgun94overview.html" } @inproceedings{OK85, author = "R. A. O'Keefe", title = "Towards an {A}lgebra for {C}onstructing {L}ogic {P}rograms", Booktitle = "Proc. IEEE Symp. on Logic Programming", Year = 1985, pages = {152-160}} @book{O'K90, author = "R.A. O'Keefe", title = "The Craft of Prolog", publisher = "MIT Press", year = 1990 } @book{Old91, author="E.R. Olderog", title="Nets, Terms and Formulas", publisher="Cambridge Univ. Press", series = {Cambridge Tracts in Theoretical Computer Science 23}, year=1991} %%P @Article{PRS02, author = {D. Pedreschi and S. Ruggieri and J.-G. Smaus}, title = {Classes of Terminating Logic Programs}, journal = {Theory and Practice of Logic Programming}, year = {2002}, volume = {3}, number = {2}, pages = {369-418}, note = {Available also at CoRR http://arXiv.org/}} @inproceedings{Park81, author = {D.M.R. Park}, title = {Concurrency and automata on infinite sequences}, booktitle ={Proc. of the 5th GI conference}, year=1981, editor={P. Deussen}, publisher = {Springer-Verlag}, series = lncs, pages = {167-183}} @inproceedings{Ped94, author ="D. Pedreschi", title = "A Proof Method for Run-Time Properties of {P}rolog programs", booktitle = iclp94, year = 1994, editor = "P. van Hentenryck", publisher = "MIT Press"} % pages = "37-51" @Misc{Pey97, author = "S. L. {Peyton Jones}", title = "A New View of Guards", howpublished = "http://www.dcs.gla.ac.uk/$\tilde{\phantom{a}}$simonpj/", year = 1997 } @techreport{Pl81, author = "G. Plotkin", title = "A structured approach to operational semantics", number = "DAIMI FN-19", institution = "Computer Science Department", address = "Aarhus University", year = "1981"} @TechReport {PP88, author = "M. Proietti and A. Pettorossi", title = "Techniques for the automatic Improvement of Logic Programs", institution = "IASI-CNR, Roma, Italy", year = "1988", number = "Tech. Report IASI-CNR R231", month = ""} @InProceedings {PP89, author = "A. Pettorossi and M. Proietti", title = "Decidability results and characterization of strategies for the development of logic programs", booktitle = "6th International Conference on Logic Programming", year = "1989", pages = "539-553", editor = "G. Levi and M. Martelli", publisher = "The Mit Press", OPTnote = ""} @InProceedings {PP90, author = "M. Proietti and A. Pettorossi", title = "The synthesis of Eureka predicates for developing logic programs", booktitle = "ESOP'90, (Lecture Notes in Computer Science, Vol. 432)", year = "1990", pages = "306-325", editor = "N. Jones", publisher = S-V, OPTnote = ""} @InProceedings{PP91, author = "M. Proietti and A. Pettorossi", title = "Unfolding, Definition, Folding, in this Order for Avoiding Unnecessary Variables in Logic Programs", booktitle = "PLILP 91, Passau, Germany (Lecture Notes in Computer Science, Vol.528)", year = "1991", editor = "Maluszynski and M. Wirsing", pages = "347-358", publisher = "Springer-Verlag"} @InProceedings{PP91-pepm, author = "M. Proietti and A. Pettorossi", title = "Semantics Preserving Transformation Rules for Prolog", booktitle = "ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '91)", year = "1991", publisher = "ACM press"} @InProceedings{PP93, author = "M. Proietti and A. Pettorossi", title = "Synthesis of Programs from Unfold/Fold Proofs", booktitle = lopstr93, year = "1993", editor = edlopstr93, publisher = "Springer-Verlag"} @ARTICLE {PP94, AUTHOR = "A. Pettorossi and M. Proietti", TITLE = "Transformation of Logic Programs: Foundations and Techniques", JOURNAL = jlp, YEAR = "1994", VOLUME = "19,20", PAGES = "261-320", ANNOTE = ""} @InProceedings{PP94b, author = "M. Proietti and A. Pettorossi", title = "Total Correctness of a Goal Replacement Rule Based of the Unfold/Fold Proof Method", booktitle = gulpro94, year = "1994", editor = edgulpro94, ?pages = "347-358", ?publisher = "Springer-Verlag"} @InBook{PP98, author = {M. Proietti and A. Pettorossi}, editor = {D. M. Gabbay and C. J. Hogger and J. A. Robinson}, title = {Handbook of Logic in Artificial Intelligence}, chapter = {Transformation of Logic Programs}, publisher = {Oxford University Press}, year = {1998}, volume = {5}, pages = {697-787}, OPTnote = {downloaded}, OPTannote = {} } @Article{PP99, author = "M. Proietti and A. Pettorossi", title = "Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs", journal = "Journal of Logic Programming", year = "1999", volume = "41", number = "2-3", pages = "197-230"} @ARTICLE { PS83, AUTHOR = "H. Partsch and R. Steinbruggen", TITLE = "{Program Transformation Systems}", JOURNAL = "ACM Computing Surveys", YEAR = "1983", MONTH = "September", VOLUME = "15", NUMBER = "3", PAGES = "199-236", ANNOTE = ""} @TechReport{PR97, author = "D. Pedreschi and S. Ruggieri", title = "{On Logic Programs That Do Not Fail}", institution = "Dipartimento di Informatica", number = "TR-97-21", OPTmonth = oct # " 08", year = "1997", keywords = "Guarded logic programs, Dynamic selection rules, Don't care non determinism, Termination, Parallel Programming", url = "ftp://ftp.di.unipi.it/pub/techreports/TR-97-21.ps.Z", abstract = "This paper investigates the advantages of reasoning on logic programs and queries that have only successful derivations. We consider an extension of the logic programming paradigm that combines guarded clauses, in the style of concurrent logic languages, and dynamic selection rules. Some general conditions for a class of programs and queries are stated, which characterize when successful derivations only are present. A few practical instances of the general conditions are studied, and their applicability to real programs demonstrated. The main contributions of the proposed method are: (i) don't care non determinism can be safely adopted for programs that do not fail, (ii) termination of process networks expressed as logic programs can be proved, by means of a simple proof method developed for a fixed selection rule, and (iii) a strategy for parallelizing terminating Prolog programs is identified." } @Article{PR99, author = {D. Pedreschi and S. Ruggieri}, title = {On Logic Programs That Do Not Fail}, booktitle = {Proc. ICLP99 Workshop on Verification of Logic Programs}, year = {1999}, editor = {S. Etalle and J-G. Smaus}, volume = {30}, number = {1}, series = {Electronic Notes in Theoretical Computer Science}, note = {http://www.elsevier.nl/locate/entcs/} } @TechReport{Pre92, author = {S. Prestwich}, title = {The PADDY Partial Deduction System}, institution = {ECRC GmbH, Munich, Germany}, year = {1992}, number = {92-6}} @InProceedings {Prz88, author = "T. C. Przymusinki", title = "Perfect model semantics", booktitle = "Fifth international Conference and Symposium on Logic programming, Seattle, U.S.A.", year = "1988", pages = "1081-1096", publisher = "", OPTnote = ""} @inproceedings{Prz89, author = "T. Przymusinski", title = "Every logic program has a natural stratification and an iterated least fixed point model", booktitle = "Proceedings of the Eighth Symposium on Principles of Database Systems", pages = "11-21", publisher = "ACM SIGACT-SIGMOD", year = 1989 } %%Q @manual{Quintus, Title ={Quintus Prolog User's Guide and Reference Manual---Version 6}, HowPublished ={Quintus Computer Systems Inc., Mountain View CA 94041}, key ={Quintus}, Month ={April}, Year =1986 } %%R @InProceedings{vRaa97, author = "F. van Raamsdonk", title = "{Translating Logic Programs into Conditional Rewriting Systems}", pages = "168--182", OPTISBN = "0-262-64035-X", editor = "Lee Naish", booktitle = "Proceedings of the 14th International Conference on Logic Programming", OPTmonth = jul # "8--11~", publisher = "MIT Press", OPTaddress = "Cambridge", year = "1997" } @inproceedings{R84, author = "U.S. Reddy", title = "Transformation of {L}ogic {P}rograms into {F}unctional {P}rograms", Booktitle = "Proc. of Symposium on Logic Programming - Atlantic City", publisher = "IEEE Computer Society", pages = {188-196}, Year = 1984} @InProceedings{Red84, Author ="U. S. Reddy", Title ={Transformation of Logic Programs into Functional Programs}, BookTitle ={International Symposium on Logic Programming}, Organization ={Atlantic City}, Publisher ={IEEE Computer Society}, Address ={Silver Spring, MD}, Pages ={187--198}, Month ={February}, Year =1984 } @incollection{Red86, Author = "U.S. Reddy", Title = "{On the Relationship Between Logic and Functional Languages}", Booktitle="Functional and Logic Programming", Editor="D. DeGroot and G. Lindstrom", Publisher="Prentice-Hall", Year="1986", pages = {3-36} } @InProceedings{vRDW87, author = "P.\ {Van Roy} and B. Demoen and Y. D. Willems", title = "Improving the execution speed of compiled {P}rolog with modes, clause selection and determinism", editor = "H. Ehrig, R. Kowalski, G. Levi and A. Montanari", number = "250", series = lncs, pages = "111-125", booktitle = "TAPSOFT87", year = "1987", publisher = S-V } @InProceedings{vRD92, author = "P. {Van Roy} and A. Despain", title = "High Performance Logic Programming with the {A}quarius Prolog Compiler", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", pages = "54-68", booktitle = "IEEE Computer", year = "1992", OPTorganization = "", publisher = "IEEE Computer Society Press", month = "January" } @Article{kRKS98, author = "M. R. K. Krishna Rao and D. Kapur and R. K. Shyamasundar", title = "{Transformational Methodology for Proving Termination of Logic Programs}", journal = jlp, year = 1998, volume = "34", number = "1", pages = "1-41" } @Article{kRKS98-GHC, author = "M. R. K. Krishna Rao and D. Kapur and R. K. Shyamasundar", title = "{Proving Termination of GHC Programs}", journal = "New Generation Computing", year = "1997", volume = "15", number = "3", pages = "293-33"} @InProceedings{RKRR99-asian, author = {A. Roychoudhury and K. Narayan Kumar and C.R. Ramakrishnan and I.V. Ramakrishnan}, title = {Beyond Tamaki-Sato style Unfold/fold Transformations for normal logic programs}, booktitle = {Asian Computing Science Conference (ASIAN)}, pages = {322-333}, year = {1999}, OPTeditor = {}, number = {1742}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{RKRR99-ppdp, author = {A. Roychoudhury and K. Narayan Kumar and C.R. Ramakrishnan and I.V. Ramakrishnan}, title = {A Parameterized Unfold/Fold Transformation Framework for Definite Logic Programs}, booktitle = {International Conference on Principles and Practice of Declarative Programming (PPDP)}, pages = {396-413}, year = {1999}, editor = {G. Nadathur}, number = {1702}, series = {LNCS}, publisher = {Springer-Verlag}} @InProceedings{RKRRS00, author = {A. Roychoudhury and K. Narayan Kumar and C.R. Ramakrishnan and I.V. Ramakrishnan and S. A. Smolka}, title = {Verification of Parameterized Systems using Logic Program Transformations}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000)}, pages = {172-187}, year = {2000}} @techreport{Ros91, author = "D.A. Rosenblueth", title = "Using Program Transformation to obtain Methods for eliminating Backtracking in Fixed-Mode Logic Programs", institution = "Universidad Nacional Autonoma de Mexico, Instituto de Investigaciones en Matematicas Aplicadas y en Sistemas", number = 7, year = 1991} @InProceedings{Ros92, author = "D. Rosenblueth", title = "Chart parsers as proof procedures for fixed-mode logic programs", pages = "1125-1132", booktitle = "Proceedings of the International Conference on Fifth Generation Computer Systems", publisher = "ICOT, Japan", series = "ACM", year = "1992"} @InProceedings{Rug94, author = " S. Ruggieri", title = "Proving (total) correctness of prolog programs", booktitle = "Proc. the W2 Post-Conference Workshop of the 1994 Int.'l Conference on Logic Programming", year = "1994", editor = "F. de Boer and M. Gabbrielli", pages = "43-57", publisher = " Vrije Universiteit Amsterdam"} %%S @InProceedings{Sho00, author = {V. Shoup}, title = {Practical Threshold Signatures}, booktitle = {Proc.\ 17th Conference on the Theory and Application of Cryptographic Techniques (EUROCRYPT'00)}, pages = {207--220}, year = {2000}, OPTeditor = {}, number = {1807}, series = {LNCS}, publisher = {Springer-Verlag}} @InProceedings{Sto01, author = {S. Stoller}, title = {A Bound on Attacks on Payment Protocols}, booktitle = {Proc.\ 16th Annual IEEE Symposium on Logic in Computer Science {LICS'01}}, pages = {61--70}, year = {2001}, publisher = {IEEE Computer Society Press}} @InProceedings{Sah90, author = "D. Sahlin", title = "The {Mixtus} Approach to Automatic Partial Evaluation of Full {Prolog}", booktitle = "Logic Programming: Proceedings of the 1990 North American Conference, Austin, Texas, October 1990", year = "1990", editor = "S. Debray and M. Hermenegildo", pages = "377-398", publisher = "MIT Press"} @Article{Sah93, author = {D. Sahlin}, title = {Mixstus: An Automatica Partial Evaluator for Full Prolog}, journal = {New Generation Computing}, year = {1993}, OPTvolume = {}, number = {12}, pages = {7-51}} @InProceedings{Sah90, author = "D. Sahlin", title = "The {Mixtus} Approach to Automatic Partial Evaluation of Full {Prolog}", booktitle = "Logic Programming: Proceedings of the 1990 North American Conference, Austin, Texas, October 1990", year = "1990", editor = "S. Debray and M. Hermenegildo", pages = "377-398", publisher = "MIT Press"} @InProceedings{Sah95, author = "D. Sahlin", title = "Partial {E}valuation of {A}{K}{L}", booktitle = "Proceedings of the First International Conference on Concurrent Constraint Programming", year = "1995"} @InProceedings{San95, author = "D. Sands", title = "Total Correctness by Local Improvement in Program Transformation", booktitle = "Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)", year = 1995, publisher = "ACM Press"} @InProceedings{Sands95TAPSOFT, author = "D. Sands", year = "1995", title = "Proving the Correctness of Recursion-Based Automatic Program Transformations", booktitle = "Sixth International Joint Conference on Theory and Practice of Software Development (TAPSOFT)", editor = "P. Mosses and M. Nielsen and M. Schwartzbach", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", volume = "915", pages = "681--695", summary = "This paper shows how the Improvement Theorem---a semantic condition for the total correctness of program transformation on higher-order functional programs---has practical value in proving the correctness of automatic techniques, including deforestation and supercompilation.", semno = "D-222", puf = "Artikel i proceedings (med censur)", id = "KonR", } @Article{San96tcs, author = "D. Sands", title = "Proving the correctness of recursion-based automatic program transformations", journal = "Theoretical Computer Science", volume = "167", number = "1--2", pages = "193--233", year = "1996" } @InCollection{San97, author = "D. Sands", title = "Improvement theory and its applications", booktitle = "Higher-Order operational Techniques in Semantics", publisher = "Cambridge University Press", year = "1997", editor = " A. D. Gordon and A. Pitts" } @Article{San96, author = "D. Sands", title = "Total correctness by local improvement in the transformation of functional programs", journal = "ACM Transactions on Programming Languages and Systems", volume = "18", number = "2", pages = "175--234", year = "1996", url = "http://www.acm.org/pubs/toc/Abstracts/0164-0925/227716.html", abstract = "The goal of program transformation is to improve efficiency while preserving meaning. One of the best-known transformation techniques is Burstall and Darlington's unfold-fold method. Unfortunately the unfold-fold method itself guarantees neither improvement in efficiency nor total correctness. The correctness problem for unfold-fold is an instance of a strictly more general problem: transformation by locally equivalence-preserving steps does not necessarily preserve (global) equivalence. This article presents a condition for the total correctness of transformations on recursive programs, which, for the first time, deals with higher-order functional languages (both strict and nonstrict) including lazy data structures. The main technical result is an {\em improvement theorem} which says that if the local transformation steps are guided by certain optimization concerns (a fairly natural condition for a transformation), then correctness of the transformation follows. The improvement theorem makes essential use of a formalized improvement theory; as a rather pleasing corollary it also guarantees that the transformed program is a formal improvement over the original. The theorem has immediate practical consequences: it is a powerful tool for proving the correctness of existing transformation methods for higher-order functional programs, without having to ignore crucial factors such as {\em memoization} or {\em folding}, and it yields a simple syntactic method for guiding and constraining the unfold-fold method in the general case so that total correctness (and improvement) is always guaranteed.", keywords = "languages; verification", subject = "{\bf D.2.4}: Software, SOFTWARE ENGINEERING, Program Verification, Correctness proofs. {\bf D.1.1}: Software, PROGRAMMING TECHNIQUES, Applicative (Functional) Programming. {\bf F.3.1}: Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS, Specifying and Verifying and Reasoning about Programs." } @inproceedings{Sa87a, author = {V. A. Saraswat}, title = {The Concurrent Logic Programming Language {CP}: definition and operational semantics}, booktitle = popl87, year = 1987, publisher = {ACM}, pages = {49-63}} @inproceedings{Sa87b, author = {V. A. Saraswat}, title = {{GHC}: operational semantics, problems and relationship with {CP}($\downarrow,\mid$)}, booktitle = {IEEE Int'l Symp. on Logic Programming}, year = {1987}, publisher = {IEEE}, pages = {347-358}} @phdthesis{Sa89a, author = {V. A. Saraswat}, title = {Concurrent Constraint Programming Languages}, school ={Carnegie-Mellon University}, month = {January}, year=1989} @phdthesis{Sar89, author = {V. A. Saraswat}, title = {Concurrent Constraint Programming Languages}, school ={Carnegie-Mellon University}, month = {January}, year=1989} @inproceedings{Sar90, author = "V. Saraswat", title = "Concurrent {C}onstraint {P}rogramming", Booktitle = popl90, year = {1990}, pages = {232-244}} @Book{Sar93, author = "V. Saraswat", title = "Concurrent {C}onstraint {P}rogramming", publisher = "MIT press", year = "1993", series = "Logic Programming Series" } @InProceedings {Sato90, author = "T. Sato", title = "{An Equivalence Preserving First Order Unfold/Fold Transformation System}", booktitle = "Second Int. Conference on Algebraic and Logic Programming, Nancy, France, October 1990, (Lecture Notes in Computer Science, Vol. 463)", year = "1990", pages = "175-188", publisher = S-V, OPTnote = ""} @article{Sato90b, author = {T. Sato}, title = {Completed {L}ogic {P}rograms and {T}heir {C}onsistency}, journal = jlp, volume = {9}, number = {1}, year = {1990}, pages = {33-44}} @article{Sato92, author = {T. Sato}, title = {Equivalence-Preserving First-Order Unfold/Fold Transformation System}, journal = TCS, volume = {105}, number = "1", year = {1992}, pages = {57-84}} @InProceedings{Sc82, author = "D.~Scott", title = "Domains for denotational semantics", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "ICALP", year = "1982" } @InProceedings{Sch97, author = {C. Schulte}, title = {Programming Constraint Inference Engines}, booktitle = cp97, pages = {519-533}, year = {1997}, editor = edcp97, volume = volcp97, series = {LNCS}, publisher = S-V } @book{Sed90, author = "R. Sedgewick", title = "Algorithms in C", publisher = "Addison-Wesley", year = 1990 } @InProceedings {Seki89, author = "H. Seki", title = "{Unfold/Fold Transformation of Stratified Programs}", booktitle = "6th International Conference on Logic Programming", year = "1989", pages = "554-568", editor = "G. Levi and M. Martelli", publisher = "The MIT Press", OPTnote = ""} @InProceedings{Seki90, author = "H. Seki", title = "A comparative study of the {W}Ell-{F}ounded and {S}table Model Semantics: Transformation's viewpoint.", booktitle = "Workshop on Logic Programming and Non-Monotonic Logic, Austin, Texas, October 1990", year = "1990", editor = "W. Marek, A. Nerode, D. Pedreschi and V.S. Subrahmanian", publisher = {Association for Logic Programming and Mathematical Sciences Institute, Cornell University}, pages = "115-123"} @Article {Seki91, author = "H. Seki", title = "Unfold/fold transformation of stratified programs", journal = "Theoretical Computer Science", volume = "86", number = "1", year = "1991", pages = "107-139"} @article{Seki93, author = "H. Seki", title = "Unfold/fold transformation of general logic programs for the {W}Ell-{F}ounded Semantics", journal = jlp, volume = 16, number = "1\&2", year = 1993, pages = {5-23}} @techreport{Sh83, author = {E. Y. Shapiro }, title = {A subset of {C}oncurrent {P}rolog and its interpreter}, number = {TR-003}, institution = {ICOT}, address = {Tokyo}, year = 1983} @article{Sh86, author = "E. Y. Shapiro", title = {Concurrent {P}rolog: A progress report}, journal = "Computer", volume = "19", number = "8", year = "1986", pages = "44-58"} @book{Sh88, author = {E. Y. Shapiro}, title = {Concurrent {P}rolog: {C}ollected {P}apers}, publisher = mit, year = 1988} @article{Sha89, author = {E. Y. Shapiro}, title = {The Family of Concurrent Logic Programming Languages}, year = {1989}, Journal = {ACM Computing Surveys}, volume = {21}, number = {3}, pages = {412-510} } @ARTICLE { She84, AUTHOR = "J. C. Shepherdson", TITLE = "Negation as failure: a comparision of Clark's Completed Data Base and Reiter's Closed World Assumption.", JOURNAL = "Journal of Logic Programming", YEAR = "1984", NUMBER = "1", PAGES = "1-48", ANNOTE = ""} @InCollection{She88, author = "J. C. Shepherdson", title = "Negation in Logic Programming", booktitle = "Foundation of Deductive Databases and Logic Programming", publisher = "Morgan Kaufmann", year = "1988", editor = "J. Minker, editor", pages = "19-88"} @TechReport {She88b, author = "J. C. Shepherdson", title = "Language and equality theory in Logic Programming", institution = "University Walk, Bristol, England", year = "1988", number = "PM-88-08"} @InProceedings{SHC95, author = "Z. Somogyi and F. Henderson and T. Conway", title = {Mercury: an efficient purely declarative logic programming language}, OPTpages = "499-512", booktitle = "Australian Computer Science Conference", year = "1995", OPTorganization = "", OPTpublisher = "", OPTaddress = "", note = "available at http://www.cs.mu.oz.au/mercury/papers.html" } @Article{, author = {}, title = {}, journal = {}, year = {}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{SHC96, author = "Z. Somogyi and F. Henderson and T. Conway", title = {The Execution Algorithm of {Mercury}, an Efficient Purely Declarative Logic Programming Language}, journal = jlp, year = "1996", volume = "29", number = "1-3", pages = "17-64", } @InProceedings{SHCB96, author = "Z. Somogyi and F. Henderson and T. Conway and A. Bromage and T. Dowd and D. Jeffery and P. Ross and P. Schachte and S. Taylor", title = "Status of the {M}ercury system", booktitle = "JICSLP '96 Workshop on Parallelism and Implementation Technology for (Constraint) Logic Programming Languages", year = "1996", note = "available at http://www.cs.mu.oz.au/mercury/papers.html" } @PhdThesis{Sij88, author = "B.~A.~Sijtsma", title = {Verification and Derivation of Infinite-List Programs}, school = "Rijksuniversiteit Groningen", year = "1988"} @InProceedings{SHK98, author = {J.-G.~Smaus and P.~M.~Hill and A.~M.~King}, title = {Termination of Logic Programs with {\tt block} Declarations Running in Several Modes}, booktitle = {Proceedings of the 10th Symposium on Programming Language Implementations and Logic Programming}, year = 1998, editor = {C.~Palamidessi}, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{SHK99, author = {J.-G.~Smaus and P.~M.~Hill and A.~M.~King}, title = {Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using {\tt block} Declarations}, booktitle = {Proceedings of the 8th International Workshop on Logic-based Program Synthesis and Transformation}, year = 1999, pages = {289--307}, editor = {P.~Flener}, publisher = {Springer-Verlag}, series = {LNCS} } @PhdThesis{smaus-thesis, author = {J.-G.~Smaus}, title = {Modes and Types in Logic Programming}, school = {University of Kent at Canterbury}, year = 1999, month = {October}, note = {Draft available from {\tt www.cs.ukc.ac.uk/people/staff/jgs5/thesis.ps}} } @PhdThesis{Sma99a, author = {J.-G.~Smaus}, title = {Modes and Types in Logic Programming}, school = {University of Kent at Canterbury}, year = 1999, month = {October}, note = {Draft available from {\tt www.cs.ukc.ac.uk/people/staff/jgs5/thesis.ps}} } @InProceedings{Sma99-ICLP, author = {J.-G.~Smaus}, title = {Proving Termination of Input-Consuming Logic Programs}, booktitle = {Proceedings of the 16th International Conference on Logic Programming}, year = 1999, pages= {335-349}, editor = {D.~De Schreye}, publisher = {MIT Press}} @TechReport{Sma99-tech, author = {J.-G.~Smaus}, title = {Proving Termination of Input-Consuming Logic Programs}, institution = {Computing Laboratory, University of Kent at Canterbury, United Kingdom}, year = 1999, number = {10-99} } @InCollection{Smo95, author = "G.~Smolka", title = "The {O}z Programming Model", booktitle = "Computer Science Today", year = "1995", editor = "Jan van Leeuwen ", number = "1000", publisher = S-V, series = "LNCS", OPTpages = "324-343", note = "see www.ps.uni-sb.de/oz/" } @InProceedings{Som87, author = "Z. Somogyi", title = "A system of precise modes for logic programs", editor = ediclp87, booktitle = iclp87, pages= "769-787", publisher = mit, year = "1987"} @PhdThesis{Som89, author = "Z. Somogy", title = "A Parallel Logic Programing System based on Strong and Precise Modes", school = "University of Melbourne", year = "1989", note = "Also Technical Report 89/4, University of Melbourne. Available at http://www.cs.mu.oz.au/~zs/papers/papers.html" } @InProceedings {SF87, author = "H. Seki and K. Furukawa", title = "Notes on transformation techniques for generate and test logic programs", booktitle = "Symposium on Logic Programming, San Francisco, California, August 1987", year = "1987", pages = "215-223", publisher = "IEEE", OPTnote = ""} @PhdThesis{Sma99phd, author = {J. G. Smaus}, title = {Modes and types in logic programming}, school = {University of Kent at Canterbury}, year = {1999}} @InProceedings{Sma99, author = {J. G. Smaus}, title = {Proving Termination of Input-Consuming Logic Programs}, booktitle = {16th International Conference on Logic Programming}, pages = {335--349}, year = {1999}, editor = {D.~De Schreye}, publisher = {MIT press} } @INPROCEEDINGS{SMI95, AUTHOR = "Suzuki, Taro and Middeldorp, Aart and Ida, Tetsuo", TITLE = "Level-confluence of conditional rewrite systems with extra variables in right-hand sides", BOOKTITLE = "Proceedings of the 6th annual conference on Rewriting Techniques and Applications (RTA '95)", YEAR = 1995, EDITOR = "Hsiang, Jieh", PAGES = "179--193", ADDRESS = "Kaiserslautern, Germany", MONTH = apr, SERIES = lncs, VOLUME = 914 } @manual{SIC98, key = "SICStus", title = {{SICS}tus {P}rolog {U}ser's Manual}, organization = {Intelligent Systems Laboratory}, address = {Swedish Institute of Computer Science, PO Box 1263, \mbox{S-164 29} Kista, Sweden}, note = {{\tt http://www.sics.se/isl/sicstus/sicstus\_toc.html}}, year = 1998 } @Manual{Sicstus, Author = "M. Carlsson", Title = {{SICS}tus {P}rolog {U}ser's {M}anual}, Institution = {Swedish Institute of Computer Science}, Address = {Po Box 1263, S-16313 Spanga, Sweden}, Month = {February}, Year = 1988} } @manual{sicstus, key = "SICStus", title = {{SICS}tus {P}rolog {U}ser's Manual}, organization = {Intelligent Systems Laboratory}, address = {Swedish Institute of Computer Science, PO Box 1263, \mbox{S-164 29} Kista, Sweden}, note = {{\tt http://www.sics.se/isl/sicstus/sicstus\_toc.html}}, year = 1997 } @manual{Sicstus97, key = "SICStus", title = {{SICS}tus {P}rolog {U}ser's Manual}, organization = {Intelligent Systems Laboratory}, address = {Swedish Institute of Computer Science, PO Box 1263, \mbox{S-164 29} Kista, Sweden}, note = {{\tt http://www.sics.se/isl/sicstus/sicstus\_toc.html}}, year = 1997 } @Manual{Sicstus88, Author = "M. Carlsson", Title = {{SICS}tus {P}rolog {U}ser's {M}anual}, Institution = {Swedish Institute of Computer Science}, Address = {Po Box 1263, S-16313 Spanga, Sweden}, Month = {February}, Year = 1988} } @InProceedings{SRP91, author = "V.A. Saraswat and M.~Rinard and P.~Panangaden", title = {Semantics foundations of Concurrent Constraint Programming}, booktitle = popl91, year = "1991", publisher = "ACM Press" } @inproceedings{SR90, author = {V.A. Saraswat and M. Rinard}, title = {Concurrent Constraint Programming}, booktitle = {Proc. of the Seventeenth ACM Symposium on Principles of Programming Languages}, pages = {232-245}, publisher = {ACM, New York}, year = {1990}} @book{SS86, author = "L. Sterling and E. Shapiro", title = "The Art of Prolog", publisher = "MIT Press", year = 1986 } @Article{SS00-jucs, author = {S. Seres and M.~J.Spivey}, title = {Functional Reading of Logic Programs}, journal = {Journal of Universal Computer Science}, year = {2000}, volume = {6}, number = {4}, month = {April}, note = {See \verb+http://http://www.jucs.org/+}} @Unpublished{SS99, author = {S. Seres and M.~J.Spivey}, title = {Embedding Prolog into Haskell}, note = {Proceedings of HASKELL'99 workshop. Available at \verb+http://web.comlab.ox.ac.uk/oucl/work/silvija.seres/+}, OPTkey = {}, OPTmonth = {}, year = {1999}, OPTannote = {} } @InProceedings{SSS97, author = "C.~Speirs and Z.~Somogyi and H.~S{\o}ndergaard.", title = "Termination analysis for {M}ercury", OPTeditor = "", OPTvolume = "", number = "1302", series = "LNCS", pages = "157--171", booktitle = "Static Analysis, Fourth International Static Analysis Symposium, (SAS'97)", year = "1997", OPTorganization = "", publisher = S-V } @InProceedings {ST84, author = "T. Sato and H. Tamaki", title = "Transformational logic program systhesis", booktitle = "International Conference on Fifth Generation Computer Systems, Tokyo, Japan, November 1984", year = "1984", pages = "195-201", publisher = "ICOT", OPTnote = ""} @article{Str93, author = "K. Stroetman", title = "A Completeness Result for {SLDNF} Resolution", journal = "The Journal of Logic Programming", volume = "15", pages = "337-357", year = 1993 } %%T @Article{Tick95, author = "E.~Tick", title = " The Deevolution of Concurrent Logic Programming Languages", journal = jlp, year = "1995", volume = "23", number = "2", pages = "89-123" } @TechReport {TS83, author = "H. Tamaki and T. Sato", title = "A transformation system for logic programs which preserves equivalence", institution = "ICOT, Tokyo, Japan", year = "1983", number = "ICOT TR-018", month = "August"} @inproceedings{TS84, author = {H. Tamaki and T. Sato}, title = {Unfold/{F}old {T}ransformations of {L}ogic {P}rograms}, booktitle = iclp84, editor = ediclp84, pages = {127-139}, year = 1984} @TechReport {TS86, author = "H. Tamaki and T. Sato", title = "A generalized correctness proof of the {U}nfold/{F}old Logic Program transformation", institution = "Ibaraki University, Tokyo, Japan", year = "1986", number = "86-4", month = "August"} %%U @inproceedings{Ueda86, author = {K. Ueda}, title = {Guarded {H}orn {C}lauses}, booktitle ={Logic {P}rogramming `85}, editor = {E. Wada}, pages = "168-179", series=lncs, volume=221, publisher = springer, year = {1986} } @Article{UM94, author = "K. Ueda and M. Morita", title = "Moded Flat {GHC} and Its Message-Oriented Implementation Technique", journal = NGC, year = "1994", volume = "13", number = "1", pages = "3-43"} @incollection{Ueda87, author = "K. Ueda", title = {Guarded {H}orn {C}lauses}, editor = "E.Y. Shapiro", booktitle = "Concurrent Prolog: Collected Papers", volume ="1", publisher = mit, pages = "140-156", year = "1987"} @inproceedings{Ueda88, author = {K. Ueda}, title = {{G}uarded {H}orn {C}lauses, A Parallel Logic Programming Language with the Concept of a Guard}, booktitle = {Programming of Future Generation Computers}, year = {1988}, publisher = {North Holland, Amsterdam}, editor = {M. Nivat and K. Fuchi}, pages = {441-456} } @inproceedings{UF88, author = "K. Ueda and K. Furukawa", title = {Transformation rules for {G}{H}{C} {P}rograms}, booktitle = fgcs88, pages = "582-591", organization = icot, year = "1988"} @InProceedings{Ueda94, author = "K. Ueda", title = "{I}/{O} Mode Analysis in Concurrent Logic Languages", editor = edtppp94, volume = voltppp94, series = lncs, pages = "356-368", booktitle = tppp94, year = "1995", publisher = S-V} @TechReport{Ueda95, author = {K. Ueda}, title = {Guarded Horn Clauses}, institution = {Institute for New Generation Computer Technology (ICOT)}, year = {1995}, number = {TR-103}, note = {Revised version in Proc. Logic Programming '85, Wada, E.(ed.), Lecture Notes in Computer Science 221, Springer-Verlag, Berlin Heidelberg New York Tokyo, 1986, pp.168-179. Also in Concurrent Prolog: Collected Papers, Shapiro, E.Y. (ed.), The MIT Press, Cambridge, 1987, pp.140-156.}, annote = {downloaded as Ueda95GHC.ps.gz} } %%V @INPROCEEDINGS{EL82, AUTHOR = "M.H. van Emden and G.J. de Lucena", TITLE = "Predicate Logic as a Language for Parallel Programming", BOOKTITLE = "Logic Programming", editor = "K.L. Clark and S.-A. T{\"{a}}rnlund", PUBLISHER = "Academic Press", SERIES = "", ADDRESS = "London", ?pages = "189-198", YEAR = 1982, NOTE = "" } @ARTICLE { EK76 , AUTHOR = "M.H. van Emden and R.A. Kowalski", TITLE = "The Semantics of Predicate Logic as a Programming Language", JOURNAL = JACM, YEAR = "1976", MONTH = "October", VOLUME = "23", NUMBER = "4", PAGES = "733-742", ANNOTE = ""} @Article{vEK76, author = "M. H. van Emden and R. Kowalski", title = "{The Semantics of Predicate Logic as Programming Language}", journal = "Journal of ACM", pages = "733--743", year = "1976", volume = "23", number = "4", } @Article{vEOT86, author = "M. H. van Emden and M. Ohki and A. Takeuchi", title = "{Spreadsheets with Incremental Queries as as User Interface for Logic Programming}", journal = "New Generation Computing", volume = "4", pages = "287--304", year = "1986", } @article{vGRS91, author = {A. Van Gelder and K. Ross and J. Schlipf}, title = {The well-founded semantics for general logic programs}, journal = {Journal of ACM}, volume = {38}, number = {3}, year = {1991}, pages = {619--649}, doi = {http://doi.acm.org/10.1145/116825.116838}, publisher = {ACM Press} } @InProceedings {VGRS88, author = "A. Van Gelder and K. Ross and J. S. Schlipf", title = "Unfounded sets and the {W}ell-{F}ounded {S}emantics for {G}eneral {L}ogic {P}rograms", booktitle = "Proc. Seventh ACM symposium on Principles of Database System", year = "1988", pages = "211-230"} @TechReport {Vie86, author = "L. Vielle", title = "Recursion in Deductive Databases: a DB-complete proof procedure based on SLD-resolution", institution = "ECRC", year = "1986", number = "Tech. Report Kb-15", month = ""} %W @inproceedings{WWJ04, author = {L. Wang and D. Wijesekera and S. Jajodia}, title = {A logic-based framework for attribute based access control}, booktitle = {Proc.\ 2004 ACM workshop on Formal methods in security engineering FMSE'04}, year = {2004}, isbn = {1-58113-971-3}, pages = {45--55}, doi = {http://doi.acm.org/10.1145/1029133.1029140}, publisher = {ACM Press}} @InProceedings{Wad85, author = "P.~Wadler", title = "{How to Replace Failure by a List of Successes --- {A} Method for Exception Handling, Backtracking, and Pattern Matching in Lazy Functional Languages}", booktitle = "Proceedings of the Second Conference on Functional Programming Languages and Computer Architecture", OPTaddress = "Nancy, France", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", OPTmonth = sep # " 16--19,", year = "1985", pages = "113--128" } @InCollection{Wad87, author = "P. Wadler", title = "List comprehensions", booktitle = "The Implementation of Functional Programming Languages", publisher = "Prentice-Hall International", year = "1987", editor = "S.L. {Peyton Jones}", chapter = "7", pages = "127--138"} @INPROCEEDINGS{Wad92, AUTHOR = {P. Wadler}, ADDRESS = {Santa Fe, New Mexico}, BOOKTITLE = {19'th Annual Symposium on Principles of Programming Languages ({POPL})}, TITLE = {The Essence of Functional Programming}, YEAR = {1992} } @Article{WB93, author = "M. Wilson and A. Borning", title = {Hierarchical Constraint Logic Programming}, journal = "Journal of Logic Programming", year = "1993", volume = "16", number = "3", pages = "277--318", OPTmonth = jul, mynote = "(Also available as Technical Report 93-01-02 from the University of Washington, Seattle), wilson_borning:93JLP:hier_CLP.ps.gz" } @inproceedings{WML84, author = {D.~A. Wolfram and M.J. Maher and J-L. Lassez}, title = {A {U}nified {T}reatment of {R}esolution {S}trategies for {L}ogic {P}rograms}, booktitle = iclp84, editor = ediclp84, pages = {263-276}, year = 1984} @inproceedings{WV93, author = "Mark Wallace and Andr{\'{e}} Veron", title = "Two Problems -- Two Solutions: One System -- {ECLiPSe}", booktitle = "Proceedings {IEEE} Colloquium on Advanced Software Technologies for Scheduling", year = 1993, address = "London", month = apr, } @Article{WNS97, author = {M.~G.~ Wallace and S.~Novello and J.~Schimpf}, title = {ECLiPSe : A platform for constraint logic programming}, journal = {ICL Systems Journal}, year = {1997}, volume = {12}, number = {1}} %Y @InCollection{YFS92, author = "E. Yardeni and T. Fr{\"{u}}hwirth and E. Shapiro", title = "Polymorphically Typed Logic Programs", booktitle = "Types in Logic Programming", publisher = "MIT Press", year = "1992", editor = "F. Pfenning", pages = "63-90", address = "Cambridge, Massachussets" } %W @InProceedings{WAN04, author = {N.~Whitehead and M.~Abadi and G.~C. Necula}, title = {By reason and authority: A system for authorization of proof-carrying code}, booktitle = {Proc.\ of the 17th Computer Security Foundations Workshop}, pages = {236-250}, year = {2004}, publisher = {IEEE Computer Society Press} } %%Z @InProceedings {ZS87, author = "C. Zaniolo and D. Sacc\'{a}", title = "Implementation of recursive queries for a language based on pure Horn logic", booktitle = "4th International Conference on Logic Programming, Melbourne, Australia, May 1987", year = "1987", editor = "J.-L. Lassez", pages = "104-135", publisher = "The MIT Press", OPTnote = ""} @ARTICLE {Zhu94, AUTHOR = "H. Zhu", TITLE = "{How Powerful Are Folding/Unfolding Transformations?}", JOURNAL = JFP, YEAR = "1994", MONTH = "January", VOLUME = "4", NUMBER = "1", PAGES = "89-112", ANNOTE = ""} @InProceedings {ZG88, author = "J. Zhang and P. W. Grant", title = "An {A}utomatic {D}ifference-list {T}ransformation {A}lgorithm for {P}rolog", booktitle = "Proceedings of the {E}uropean {C}onference on {A}rtificial {I}ntelligence,{ECAI}'88", year = "1988", pages = "320-325", publisher = "Pitman"} @InProceedings{BR87, author = "C. Beeri and R. Ramakrishnan", title = "On the Power of Magic", booktitle = "ACM SIGACT-SIGMOD Symp. on Principles of Database Systems, San Diego", year = "1987" } @InProceedings{BMSU86, author = {F.~Bancilhon and D.~Maier and Y~Sagiv and J.~Ullman}, title = {Magic Sets and other strange ways to implement logic programs}, booktitle = "ACM SIGACT-SIGMOD Symp. on Principles of Database Systems, Washington", publisher = {ACM Press}, year = "1986" } @Article{BR91, author = "C. Beeri and R. Ramakrishnan", title = "On the Power of Magic", journal = "The Journal of Logic Programming", volume = "10", year = "1991" } @inproceedings{FGR98, author = {N. Fuhr and and N. G{\"o}vert and T. R{\"o}lleke}, title = {{DOLORES}: A System for Logic-Based Retrieval of Multimedia Objects}, booktitle = {{ACM SIGIR}, 21st Annual International Conference on Research and Development in Information Retrieval}, publisher = {ACM Press}, year = 1998, editor = "R. Wilkinson", pages = {257--265} } @InProceedings{FR98, author = "N. Fuhr and T. Roelleke", title = "{HySpirit} --- {A} Probabilistic Inference Engine for Hypermedia Retrieval in Large Databases", editor = "H-J. Schek and F. Saltor and I. Ramos and G. Alonso", booktitle = "EDBT'98, 6th International Conference on Extending Database Technology", series = "Lecture Notes in Computer Science", volume = "1377", OPTpages = "24--38", year = "1998", annote = "downloaded"} @InProceedings{Fuhr95, author = "N. Fuhr", title = "Probabilistic Datalog -- {A} Logic for Powerful Retrieval Methods", booktitle = "{ACM SIGIR}, Eighteenth Annual International Conference on Research and Development in Information Retrieval", editor = "E. A. Fox and P. Ingwersen and R. Fidel", pages = "282--290", year = "1995", abstract = "In the logical approach to information retrieval, retrieval is considered as uncertain inference. Here we present a new, powerful inference method for this purpose which combines Datalog with probability theory on the basis of intensional semantics. We describe syntax and semantics of probabilistic Datalog and also present an evaluation method and a prototype implementation. This approach allows for easy formulation of specific retrieval models for arbitrary applications, and classical probabilistic IR models can be implemented by specifying the appropriate rules. In comparison to other approaches, the possibility of recursive rules allows for more powerful inferences. Finally, probabilistic Datalog can be used as a query language for integrated information retrieval and database systems." } @Article{Fuhr99, author = "N. Fuhr", title = "Towards Data Abstraction in Networked Information Retrieval Systems", journal = "Information Processing and Management", year = "1999", OPTvolume = "", number = "35", note = "to appear", abstract = "Networked information retrieval aims at the interoperability of heterogeneous information retrieval (IR) systems. In this paper, we show how differences concerning search operators and database schemas can be handled by applying data abstraction concepts in combination with uncertain inference. Different data types with vague predicates are required to allow for queries referring to arbitrary attributes of documents. Physical data independence separates search operators from access paths, thus solving text search problems related to noun phrases, compound words and proper nouns. Projection and inheritance on attributes support the creation of unified views on a set of IR databases. Uncertain inference allows for query processing even on incompatible database schemas" } @InProceedings{KS95, author = "D. Konopnicki and O. Shmueli", title = "{W3QS}: {A} Query System for the {World-Wide Web}", editor = "Umeshwar Dayal and Peter M. D. Gray and Shojiro Nishio", booktitle = "{VLDB} '95: proceedings of the 21st International Conference on Very Large Data Bases", publisher = "Morgan Kaufmann Publishers", year = "1995", pages = "54--65", year = "1995" } @Article{KS98, author = "D. Konopnicki and O. Shmueli", title = "WWW Information Gathering : The W3QL Query Language and the W3QS System", journal = "ACM TODS", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", month = "September", OPTnote = "", OPTannote = "" } @InProceedings{MR89, author = "M. J. Maher and R. Ramakrishnan", title = "{D}{\'e}j{\`a} Vu in Fixpoints of Logic Programs", pages = "963--980", ISBN = "0-262-62064-2", editor = "Ross A. {Lusk, Ewing L.; Overbeek}", booktitle = "Proceedings of the North American Conference on Logic Programming ({NACLP} '89)", address = "Cleveland, Ohio", year = 1989, publisher = "MIT Press" } @InProceedings{NR90, author = "J. F. Naughton and R. Ramakrishnan", title = "How to Forget the Past Without Replicating It", booktitle = "Proc. Int'l. Conf. on Very Large Data Bases", pages = "278", address = "Brisbane, Australia", year = "1990", keywords = "VLDB" } @InCollection{NR91, author = "J. N. Naughton and R. Ramakrishnan", title = "Bottom-Up Evaluation of Logic Programs", booktitle = "Computational Logic: Essays in Honor of Alan Robinson", publisher = "The MIT Press", year = "1991", editor = "J-L Lassez and G. Plotkin"} @Article{NR94, author = "J. F. Naughton and R. Ramakrishnan", title = "How to Forget the Past without Repeating It", journal = "Journal of the ACM", volume = 41, number = 6, pages = "1151--1177", year = 1994, url = "http://www.acm.org/pubs/toc/Abstracts/0004-5411/195634.html", abstract = "Bottom-up evaluation of deductive database programs has the advantage that it avoids repeated computations by storing all intermediate results and replacing recomputation by table lookup. However, in general, storing all intermediate results for the duration of a computation wastes space. In this paper, we propose an evaluation scheme that avoids recomputation, yet for a fairly general class of programs at any given time stores only a small subset of the facts generated. The results constitute a significant first step in compile-time garbage collection for bottom-up evaluation of deductive database programs.", keywords = "algorithms; languages; theory", subject = "{\bf H.2.3}: Information Systems, DATABASE MANAGEMENT, Languages, Query languages. {\bf I.2.4}: Computing Methodologies, ARTIFICIAL INTELLIGENCE, Knowledge Representation Formalisms and Methods, Representations (procedural and rule-based). {\bf I.2.3}: Computing Methodologies, ARTIFICIAL INTELLIGENCE, Deduction and Theorem Proving. {\bf H.2.4}: Information Systems, DATABASE MANAGEMENT, Systems." } @InProceedings{PF95, author = "U. Pfeifer and N. Fuhr", title = "Efficient Processing of Vague Queries using a Data Stream Approach", booktitle = "Proceedings of the Eighteenth International ACM SIGIR Conference on Research and Development in Information Retrieval", editor = "R. Korfhage and E. Rasmussen and P. Willett", pages = "189--197", year = "1995", publisher = "ACM press", abstract = "In this paper, we consider vague queries in text and fact databases. A vague query can be formulated as a combination of vague criteria. A single database object can meet a vague criterion to a certain degree. We confine ourselves to queries for which the answer can be computed efficiently by (perhaps repetitive) combination of rankings to new rankings. Since users usually will inspect some of the best answer objects only, the corresponding rankings need to be computed just as far as necessary to generate these first answer objects. In this contribution we describe an approach for estimating the number of elements needed from the basic rankings to compute a given number of elements of the resulting ranking. Experiments with a large text database prove the applicability of our approach." } @InProceedings{PP97, author = "U. Pfeifer and S. Pennekamp", title = "Incremental Processing of Vague Queries in Interactive Retrieval Systems", editor = "N. Fuhr and G. Dittrich and K. Tochtermann", booktitle = "Hypertext - Information Retrieval - Multimedia '97: Theorien, Modelle und Implementierungen integrierter elektronischer Informationssysteme, HIM'97", year = "1997", pages = "223-235", publisher = "Universit{\"a}tsverlag Konstanz" } @InProceedings{Ram88, author = "Raghu Ramakrishnan", title = "Magic: {A} Spellbinding Approach to Logic Programs", booktitle = "Proceedings of the Fifth International Conference and Symposium on Logic Programming", organization = "ALP, IEEE", year = "1988", editor = "Robert A. Kowalski and Kenneth A. Bowen", publisher = "The MIT Press", pages = "140--159" } @Article{Ram91, author = "R. Ramakrishnan", title = "Magic Templates: {A} Spellbinding Approach to Logic Programs", journal = "Journal of Logic Programming", pages = "189--216", volume = "11", number = "3\&{}4", year = "1991"} @InProceedings{RB97, author = "T. R{\"o}lleke and M. Bl{\"o}mer", title = "Probabilistic Logical Information Retrieval for Content, Hypertext, and Database Querying", editor = "N. Fuhr and G. Dittrich and K. Tochtermann", booktitle = "Hypertext - Information Retrieval - Multimedia '97: Theorien, Modelle und Implementierungen integrierter elektronischer Informationssysteme, HIM'97", year = "1997", pages = "147-160", publisher = "Universit{\"a}tsverlag Konstanz" } @InProceedings{RF96, author = "Thomas R{\"o}lleke and Norbert Fuhr", title = "Retrieval of Complex Objects Using a Four-Valued Logic", pages = "206--215", editor = "Hans-Peter Frei and Donna Harman and Peter Sch{\"a}uble and Ross Wilkinson", booktitle = "Proceedings of the Nineteenth Annual International {ACM} {SIGIR} Conference on Research and Development in Information Retrieval", month = aug # "18--22~", publisher = "ACM Press", address = "New York", year = "1996", annote ="downloaded" } @InCollection{RSS92bottom-up, author = "R. Ramakrishnan, D. Srivastava and S. Sudarshan", title = {Efficient Bottom-Up Evaluation of Logic Programs}, booktitle = "The State of the Art in Computer Systems and Software Engineering", publisher = "Kluwer Academic Publishers", year = "1992", editor = "J. Vandewalle" } @InProceedings{RSS92, author = "R. Ramakrishnan and D. Srivastava and Sudarshan.S.", title = "{CORAL}: {A} Deductive Database Programming Language", booktitle = "Proceedings of the 18th Conference on Very Large Databases, Morgan Kaufman pubs. (Los Altos CA), Vancouver", year = "1992", annote = "CORAL is a modular declarative query language/programming language that supports Horn clauses with complex terms, set-grouping, aggregation, negation, and relations with tuples that contain (universally quantified) variables; uses the EXODUS storage manager and has an interface to C++", } @Article{RSSS94, title = "The {CORAL} Deductive System", author = "Raghu Ramakrishnan and Divesh Srivastava and S. Sudarshan and Praveen Seshadri", journal = "The VLDB Journal", pages = "161--210", month = "April", year = "1994", volume = "3", number = "2", annote = Ramakr_etal94_Coral_jou.ps.gz } @InProceedings{Ull89, author = "J. D. Ullman", title = "Bottom-up beats top-down for datalog", editor = "{ACM}", booktitle = "{PODS} '89. Proceedings of the Eighth {ACM} {SIGACT-SIGMOD-SIGART} Symposium on Principles of Database Systems, March 29--31, 1989, Philadelphia, {PA}", publisher = "ACM Press", address = "New York, NY 10036, USA", year = "1989", pages = "140--149", year = "1989", url = "http://www.acm.org:80/pubs/citations/proceedings/pods/73721/p140-ullman/", keywords = "algorithms; design; languages; theory", subject = "{\bf F.4.1} Theory of Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical Logic, Lambda calculus and related systems. {\bf H.2.4} Information Systems, DATABASE MANAGEMENT, Systems, Query processing. {\bf H.2.3} Information Systems, DATABASE MANAGEMENT, Languages, Datalog." } @InProceedings{Seki89-Alexander, author = {H.~Seki}, title = {On the power of Alexander templates}, booktitle = "ACM SIGACT-SIGMOD Symp. on Principles of Database Systems, Philadelphia, Pennsylvania", publisher = {ACM Press}, year = "1989" } @Article{vET86, author = "M. H. van Emden and M. Ohki and A. Takeuchi", title = "{Spreadsheets with Incremental Queries as as User Interface for Logic Programming}", journal = "New Generation Computing", volume = "4", pages = "287--304", year = "1986" } %$# TOBE RECONSIDERED @Article{ST05, author = {V. Shmatikov and C. Talcott}, title = {{Reputation-Based Trust Management}}, journal = {Journal of Computer Security}, publisher = {IOS Press}, pages = {167--190}, volume = {13}, number = {1}, year = {2005}} @inproceedings{SWY+02, author = {K.\ Seamons and M.\ Winslett and T.\ Yu and B.\ Smith and E.\ Child and J. Jacobson and H. Mills and and L. Yu}, title = {{Requirements for Policy Languages for Trust Negotiation}}, booktitle = {Proc.\ 3rd International Workshop on Policies for Distributed Systems and Networks (POLICY 2002)}, pages = {68-80}, publisher = {IEEE Computer Society}, url = {http://isrl.cs.byu.edu/pubs/policy2002.pdf}, year = {2002} } @inproceedings{BS04:wits, author = {M. Y. Becker and P. Sewell}, title = {Cassandra: flexible trust management, applied to electronic health records}, booktitle = {Proc.\ 5th 17th IEEE Computer Security Foundations Workshop (CSFW 2004)}, pages = {139-154}, year = {2004}, publisher = {IEEE Computer Society Press} } @inproceedings{BS04, author = {M. Y. Becker and P. Sewell}, title = {{Cassandra: Distributed Access Control Policies with Tunable Expressiveness}}, booktitle = {Proc.\ 5th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY 2004)}, pages = {159-168}, month = {July}, year = {2004}, publisher = {IEEE Computer Society Press} } @article{RGA02, author = {C. M. Ridingsa and D. Gefenb and B. Arinze}, title = {Some antecedents and effects of trust in virtual communities}, journal = {Journal of Strategic Information Systems}, publisher = {Elsevier Science}, pages = {271-295}, volume = {11}, year = {2002} } @inproceedings{LVL02, author = {F. Lee and D. Vogel and M. Limayem}, title = {Adoption of Informatics to Support Virtual Communities}, booktitle = {HICSS '02: Proc.\ of the 35th Annual Hawaii International Conference on System Sciences (HICSS'02)-Volume 8}, year = {2002}, isbn = {0-7695-1435-9}, pages = {214}, publisher = {IEEE Computer Society Press} } @inproceedings{PWF+02, author = {L. Pearlman and V. Welch and I. T. Foster and C. Kesselman and S. Tuecke}, title = {A Community Authorization Service for Group Collaboration}, booktitle = {POLICY}, publisher = {IEEE Computer Society Press}, year = {2002}, pages = {50-59} } @inproceedings{AH00, author = {A. Abdul-Rahman and S. Hailes}, title = {Supporting Trust in Virtual Communities}, booktitle = {HICSS '00: Proc.\ of the 33rd Hawaii International Conference on System Sciences-Volume 6}, year = {2000}, isbn = {0-7695-0493-0}, pages = {6007}, publisher = {IEEE Computer Society Press} } @inproceedings{BT04, author = {G. Boella and L. van der Torre}, title = {Permission and Authorization in Policies for Virtual Communities of Agents}, booktitle = {Proc.\ of Agents and P2P Computing Workshop at AAMAS'04}, year = {2004}, publisher = {Springer Verlag} } \InProceedings{XL03, author = {L. Xiong and L. Liu}, title = {A reputation-based trust model for peer-to-peer ecommerce communities.}, booktitle = {ACM Conference on Electronic Commerce}, publisher = {ACM}, year = {2003}, pages = {228-229} } @inproceedings{BFK99, author = {M. Blaze and J. Feigenbaum and A. D. Keromytis}, title = {KeyNote: Trust Management for Public-Key Infrastructures (Position Paper).}, booktitle = {Security Protocols Workshop}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {1550}, year = {1999}, pages = {59-63}, ee = {http://link.springer.de/link/service/series/0558/bibs/1550/15500059.htm}, crossref = {DBLP:conf/spw/1998}, bibsource = {DBLP, http://dblp.uni-trier.de} }