$Id: bib90.bib 2001/02/01 denker $ DAML annotation of ca. 90 bibliography entries "MaudeWeb" "{Maude Web Site}" "2000" "url{http://maude.csl.sri.com/}" "CSFW" "{IEEE Computer Security Foundations Workshop}" "{IEEE Computer Security Foundations Workshop}" "1988-2000" "IEEE Computer Society" "url{http://www.csl.sri.com/csfw/}" "{11th IEEE Computer Security Foundations Workshop, Rockport, Massachusetts, June 1998}" "{11th IEEE Computer Security Foundations Workshop, Rockport, Massachusetts, June 1998}" "1998" "IEEE Computer Society" "{12th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 1999}" "{12th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 1999}" "1999" "IEEE Computer Society" "G. Agha" "{Abstracting interaction patterns: A programming paradigm for open distribute systems.}" "{Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), Volume 2, IFIP TC6 WG6.1 Intern. Workshop, 21-23 July, Canterbury, Kent, UK}" "1997" "H. Bowman" "J. Derrick" "135-153" "" "Chapman & Hall" "" "" "" "D. Basin" "G. Denker" "{Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis}" "2000" "235-256" "" "" "" "" "S. M. Bellovin" "M. Merritt" "{Augmented Encrypted Key Exchange: A Password-Based Protocol Secure Against Dictionary Attacks and Password File Compromise}" "{1st ACM Conf. on Computer and Communications Security}" "1993" "244-250" "ACM SIGSAC" "" "" "" "" "P. Borovansk'y" "C. Kirchner" "H. Kirchner" "{Strategies and Rewriting in {ELAN}}" "{Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia, July 1997)}" "1997" "B. Gramlich" "H. Kirchner" "" "" "" "" "" "" "P. Borovansk'y" "C. Kirchner" "H. Kirchner" "P.-E. Moreau" "M. Vittek" "{{ELAN}: A logical framework based on computational systems}" "" "" "" "" "" "S. Brackin" "C. Meadows" "J. Millen" "{CAPSL Interface for the NRL Protocol Analyzer}" "{IEEE Symposium on Application-Specific Systems and Software Engineering Technology, ASSET '99, Dallas }" "1999" "" "" "" "" "" "To appear" "S. Brackin" "{Automatically Detecting Most Vulnerabilities in Cryptographic Protocols}" "251-266" "" "" "" "" "url{http://schafercorp-ballston.com/discex/}" "S. Budkowski" "A. Cavalli" "E. Najm" "{Proc. Formal Description Techniques And Protocol Specification, Testing and Verification, FORTE XI/PSTV XVIII'98, 3-6 November, Paris, France}" "{Proc. Formal Description Techniques And Protocol Specification, Testing and Verification, FORTE XI/PSTV XVIII'98, 3-6 November, Paris, France}" "Kluwer Academic Publishers" "1998" "K. M. Chandy" "J. Misra" "Proofs of Networks of Processes" "{IEEE} Transactions on Software Engineering" "7" "4" "1981" "417-426" "K. Mani Chandy" "Jayadev Misra" "{Parallel Program Design: A Foundation}" "Addison-Wesley" "1988" "" "" "" "" "" "" "M. Clavel" "F. Dur{'a}n" "S. Eker" "J. Meseguer" "{Building Equational Proving Tools by Reflection in Rewriging Logic}" "{Proc. of the CafeOBJ Symp.'98, April, Japan}" "1998" "" "{Maude: Specification and Programming in Rewriting Logic}" "M. Clavel" "F. Dur{'a}n" "S. Eker" "P. Lincoln" "N. Mart'{i}-Oliet" "J. Meseguer" "J. Quesada" "SRI International, Computer Science Laboratory" "Menlo Park, CA" "" "january" "1999" "url{http://maude.csl.sri.com/manual/}" "M. Clavel" "S. Eker" "P. Lincoln" "J. Meseguer" "{Principles of Maude}" "65-89" "M. Clavel" "J. Meseguer" "{Reflection and Strategies in Rewriting Logic}" "125-147" "G. Denker" "J. Millen" "{The CAPSL Integrated Protocol Environment}" "{Computer Science Laboratory, SRI International, Menlo Park, CA 94025}" "{CSL Report}" "2000" "{SRI-CSL-2000-02}" "" "" "url{http://www.csl.sri.com/~denker/pub_99.html}" "G. Denker" "J. Millen" "J. Kuester-Filipe" "A. Grau" "Optimizing Protocol Rewrite Rules of {CIL} Specifications" "13th IEEE Computer Security Foundations Workshop" "2000" "52-62" "IEEE Computer Society" "G. Denker" "J. Meseguer" "C. Talcott" "{Rewriting Semantics of Meta-Objects and Composable Distributed Services}" "2000" "407-427" "" "" "" "" "G. Denker" "J. Meseguer" "C. Talcott" "{Protocol Specification and Analysis in Maude}" "{Proc. of Workshop on Formal Methods and Security Protocols, 25 June 1998, Indianapolis, Indiana}" "1998" "N. Heintze" "J. Wing" "" "" "" "" "" "url{http://www.cs.bell-labs.com/who/nch/fmsp/index.html}" "G. Denker" "{Schritt f\"ur Schritt zum Ziel - Entwurf von Informationssystemen durch Verfeinerung}" "{erscheint in: Carolo-Wilhelmina-Mitteilungen, Sonderheft ``25 Jahre Informatik in Braunschweig''}" "1998" "" "" "" "" "" "G. Denker" "J. Millen" "{CAPSL and CIL Language Design: A Common Authentication Protocol Specification Language and Its Intermediate Language}" "{Computer Science Laboratory, SRI International, Menlo Park, CA 94025}" "{CSL Report}" "1999" "{SRI-CSL-99-02}" "" "" "url{http://www.csl.sri.com/~denker/pub_99.html}" "G. Denker" "J. J. Garcia-Luna-Aceves" "J. Meseguer" "P. {\"O}lveczky" "J. Raju" "B. Smith" "C. Talcott" "{Specification and Analysis of a Reliable Broadcasting Protocol in Maude}" "{Proc. 37th Allerton Conference on Communication, Control and Computation}" "1999" "B. Hajek" "R. S. Sreenivas" "" "" "" "" "" "url{http://www.comm.csl.uiuc.edu/allerton}" "G. Denker" "J. J. Garcia-Luna-Aceves" "J. Meseguer" "P. {\"O}lveczky" "J. Raju" "B. Smith" "C. Talcott" "{Specifying a Reliable Broadcasting Protocol in Maude}" "{Computer Science Laboratory, SRI International, Menlo Park, CA 94025}" "Internal report" "1999" "" "" "url{http://www.csl.sri.com/~denker/pub_99.html}" "G. Denker" "J. Millen" "{CAPSL Integrated Protocol Environment}" "207-222" "" "" "" "" "url{http://schafercorp-ballston.com/discex/}" "G. Denker" "J. Millen" "{CAPSL Intermediate Language}" "" "" "" "" "" "url{http://cm.bell-labs.com/cm/cs/who/nch/fmsp99/}" "G. Denker" "J. Meseguer" "C. Talcott" "{Formal Specification and Analysis of Active Networks and Communication Protocols: The Maude Experience}" "251-266" "" "" "" "" "url{http://schafercorp-ballston.com/discex/}" "G. Denker" "{From Rewrite Theories to Temporal Logic Theories}" "" "" "D. E. Denning" "G. M. Sacco" "{Timestamps in Key Distribution Protocols}" "Communications of the ACM" "1981" "24" "8" "533-536" "" "" "D. Dolev" "A. Yao" "On the security of public key protocols" "IEEE Transactions on Information Theory" "1983" "IT-29" "198-208" "Also STAN-CS-81-854, May 1981, Stanford U." "F. Dur{'a}n" "J. Meseguer" "{An Extensible Module Algebra For Maude}" "" "{em to appear}" "B. Dutertre" "S. Schneider" "{Using a PVS Embedding of CSP to Verify Authentication Protocols}" "{Theorem Proving in Higher Order Logics, TPHOL's 97}" "1997" "121-136" "" "Springer" "" "" "LNCS 1275" "{Protocol Boosters}" "D. Feldmeier" "A. McAuley" "J. Smith" "D. Bakin" "W. Marcus" "T. Raleigh" "" "" "1999" "{Accepted for IEEE JSAC Special Issue on Protocol Architecures for the 21st Century. Available at url{http://carin.bellcore.com:8000/boosters/} under papers}" "K. Futatsugi" "{Third Intern. Workshop on Rewriting Logic and Its Applications, Kanazawa City Cultural Hall, Kanazawa, Japan, September 18-20, 2000}" "{Third Intern. Workshop on Rewriting Logic and Its Applications, Kanazawa City Cultural Hall, Kanazawa, Japan, September 18-20, 2000}" "Volume 36 of Elsevier Science B.V., Electronic Notes in Theoretical Computer Science, url{http://www.elsevier.nl/locate/entcs/volume36 .html}" "2000" "J. J. Garc'{i}a-Luna" "{Reliable Broadcasing in Computer Networks}" "{Manuscript; University of California at Santa Cruz, Computer Science Department}" "january" "1998" "" "J. Goguen" "J. Meseguer" "{Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations}" "Theoretical Computer Science" "1992" "2" "105" "" "" "" "D. Goldschlag" "M. Reed" "P. Syverson" "Onion Routing for Anonymous and Private Internet Connections" "Communications of the ACM" "1999" "42" "2" "" "february" "J. W. Gray" "J. D. McLean" "{Using Temporal Logic to Specify and Verify Cryptographic Protocols (Progress Report)}" "{Proc. of the 8th IEEE Computer Security Foundations Workshop}" "1995" "108-116" "" "IEEE Computer Society Press" "" "" "" "N. Heintze" "E. Clarke" "{Workshop on Formal Methods and Security Protocols (FMSP'99), July 5, 1999, Trento, Italy (part of FLOC'99)}" "{Workshop on Formal Methods and Security Protocols (FMSP'99), July 5, 1999, Trento, Italy (part of FLOC'99)}" "1999" "" "M. Hicks" "P. Kakkar" "J. T. Moore" "C. A. Gunter" "S. Nettles" "{PLAN: A Packet Language for Active Networks}" "Proceedings of the Third {ACM} {SIGPLAN} International Conference on Functional Programming Languages" "1998" "86-93" "ACM" "http://www.cis.upenn.edu/~switchware/papers/plan.ps" "C. A. R. Hoare" "{Communicating Sequential Processes}" "Prentice Hall International" "1985" "" "V. Johnson" "M. Johnson" "{Introduction to IP Multicast Routing. An IP Multicast Initiative White Paper}" "{IP Multicast Initiative (IPMI), Stardust Technologies, Inc}" "" "2000" "" "" "url{http://www.ipmulticast.com/community/whitepapers/intror outing.html}" "G. Kiczales" "J. Lamping" "A. Mendhekar" "C. Maeda" "C. Lopes" "J.-M. Loingtier" "J. Irwin" "{Aspect-Oriented Programming}" "{Proc. of the European Conference on Object-Oriented Programming (ECOOP'97), Finland}" "1997" "M. Aksit" "S. Matsuoka" "220-242" "" "" "" "" "{LNCS 1241, url{http://www.parc.xerox.com/spl/groups/eca/pu bs/papers/Kiczales-ECOOP97/}}" "H. Kirchner" "C. Kirchner" "{2nd Int. Workshop on Rewriting Logic and Its Applications (WRLA'98), Pont-A-Mousson, France, September 1-4, 1998}" "{2nd Int. Workshop on Rewriting Logic and Its Applications (WRLA'98), Pont-A-Mousson, France, September 1-4, 1998}" "{Elsevier Science B.V., Volume 15 of Electronic Notes in Theoretical Computer Science, url{http://www.elsevier.nl/locate/entcs/volume15 .html}}" "1998" "P. Kosiuczenko" "M. Wirsing" "{Timed Rewriting Logic for the Specification of Time-Sensitive Systems}" "{Proc. of the Intern. Summer School on Proof and Computation}" "1995" "H. Schwichtenberg" "" "" "Springer" "" "" "NATO-ASI Series" "Simon S. Lam" "A Udayar Shankar" "{A relational notation for state transition systems}" tr(journal = 'SE) "1990" "16" "7" "755-775" "july" "" "T. F. LaPorta" "D. Lee" "Y.-J. Lin" "M. Yannakakis" "{Protocol Feature Interactions}" "59-74" "" "" "" "" "" "U. Lechner" "C. Lengauer" "{Modal--$mu$--Maude --- Specification and Properties of Concurrent Objects}" "{Object Orientation with Parallelism and Persistence}" "1996" "{B.~Freitag" "C. B.~Jones" "C.~Lengauer" "H.-J.~Schek}" "23-46" "" "Kluwer" "" "" "" "C. Lopes" "G. Kiczales" "{Recent Developments in AspectJ}" "{ECOOP'98 Workshop Reader, Workshop on Aspect-Oriented Programming}" "1998" "" "" "Springer" "" "" "LNCS 1543, url{http://www.parc.xerox.com/spl/groups/eca/pub s/papers/Lopes-AOPW-ECOOP98/}" "G. Lowe" "{Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR}" "{Second Intern. Workshop TACAS'96, Passau, Germany, March 1996}" "1996" "147-166" "" "Springer" "" "" "LNCS 1055" "A. Mallet" "J. D. Chung" "J. M. Smith" "{Operating System Support for Protocol Boosters}" "" "" "1998" "{available at url{http://carin.bellcore.com:8000/boosters/} under papers}" "N. Mart'{i}-Oliet" "J. Meseguer" "{Rewriting Logic as a Logical and Semantic Framework}" "SRI International, Computer Science Laboratory, Menlo Park, CA" "{CSL Technical Report}" "1993" "{93-05}" "" "august" "" "N. Mart'{i}-Oliet" "J. Meseguer" "General {L}ogics and {L}ogical {F}rameworks" "D. Gabbay" "What is a Logical System?" "1994" "355-392" "Oxford University Press" "N. Mart'{i}-Oliet" "J. Meseguer" "{Action and Change in Rewriting Logic}" "SRI International, Menlo Park, CA" "{CSL Technical Report}" "1996" "{}" "" "" "" "N. Mart'{i}-Oliet" "J. Meseguer" "{Rewriting Logic as a Logical and Semantic Framework}" "189-225" "D. Maughan" "G. Koob" "S. Saydjari" "{Proc. DARPA Information Survivability Conference and Exposition, DISCEX2000, January 25-27, Hilton Head Island, SC, USA}" "{Proc. DARPA Information Survivability Conference and Exposition, DISCEX2000, January 25-27, Hilton Head Island, SC, USA}" "IEEE Computer Society Press" "2000" "C. A. Meadows" "{Formal Verification of Cryptographic Protocols: A Survey}" "{Advances in Cryptology - Asiacrypt '94}" "1995" "J. Pieprzyk" "R. Savafi-Naini" "133-150" "" "Springer" "" "" "LNCS 917" "C. A. Meadows" "{Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches}" "{Proc. of European Symposium on Research in Computer Security (ESORICS'96)}" "1996" "E. Bertino" "H. Kurth" "G. Martella" "E. Montolivo" "351-364" "" "Springer" "" "" "LNCS 1146" "C. A. Meadows" "{Language Generation and Verification in the NRL Protocol Analyzer}" "{Proc. 9th Computer Security Foundations Workshop}" "1996" "48-61" "" "IEEE Computer Society Press" "" "june" "" "J. Meseguer" "{Conditional Rewriting Logic as a Unified Model of Concurrency}" "Theoretical Computer Science" "1992" "96" "1" "73-155" "" "" "J. Meseguer" "{A Logical Theory of Concurrent Objects and Its Realization in the Maude Language}" "Research Directions in Concurrent Object-Oriented Programming" "The MIT Press" "1993" "G. Agha" "P. Wegner" "A. Yonezawa" "" "314-390" "" "" "" "J. Meseguer" "{Rewriting Logic and Its Applications, First International Workshop, Asilomar Conference Center, Pacific Grove, CA, September 3-6, 1996}" "{Rewriting Logic and Its Applications, First International Workshop, Asilomar Conference Center, Pacific Grove, CA, September 3-6, 1996}" "Elsevier Science B.V., Electronic Notes in Theoretical Computer Science, Volume 4, url{http://www.elsevier.nl/locate/entcs/volume4.ht ml}" "1996" "J. Meseguer" "{Rewriting Logic as a Semantic Framework for Concurrency: A Progress Report}" "{Proc. 7th Intern. Conf. on Concurrency Theory: CONCUR'96, Pisa, August 1996}" "1996" "U. Montanari" "V. Sassone" "331-372" "" "" "" "" "LNCS 1119" "J. Meseguer" "{Research Directions in Rewriting Logic}" "{Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 -- August 6, 1997}" "{Springer Verlag}" "1998" "{U. Berger" "H. Schwichtenberg}" "" "347-398" "" "" "" "{A Partial Order Event Model for Concurrent Objects}" "J. Meseguer" "C. Talcott" "{Proc. 10th Intern. Conf. on Concurrency Theory (CONCUR'99), Eindhoven, The Netherlands, August 1999}" "J. C. M Baeten" "S. Mauw" "1999" "415-430" "" "Springer" "" "" "LNCS 1664" "J. Millen" "{A Necessarily Concurrent Attack}" "SRI International, Menlo Park, CA 94025" "" "1998" "{}" "" "" "url{www.csl.sri.com/~millen}" "J. Millen" "{Local Reconfiguration Policies}" "{IEEE Symposium on Security and Privacy}" "1999" "" "IEEE Computer Society" "" "" "" "{em To appear}" "Overview of Formal Methods for Security Protocol Analysis" "J. Mitchell" "Invited Talk, CAV'98, slides" "" "1998" "url{http://theory.stanford.edu/people/jcm/home.html}" "R. Needham" "M. Schroeder" "{Using encryption for authentication in large networks of computers}" "Communications of the ACM" "1978" "21" "12" "993-999" "" "" "P. {\"O}lveczky" "P. Kosiuczenko" "M. Wirsing" "{An Object-Oriented Algebraic Steam-Boiler Control Specification}" "Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen, Inst. f. Informatik" "{Technical report}" "1997" "{9701}" "" "january" "" "P. {\"O}lveczky" "J. Meseguer" "{Specifying Real-Time Systems in Rewriting Logic}" "283-308" "L Paulson" "The inductive approach to verifying cryptographic protocols" "Journal of Computer Security" "1998" "6" "1" "85-128" "J. Peleska" "{On a unified formal approach for the development of fault-tolerant and secure systems}" "{Nordic Seminar on Dependable Computing Systems, Lyngby, Denmark, August 1994. Technical University of Denmark}" "1994" "H. Rischel" "69-80" "" "" "" "" "" "I. Pita" "N. Mart'{i}-Oliet" "{A Maude Specification of an Object Oriented Database Model for Telcommunication Networks}" "404-422" "{CafeOBJ Project}" "Proc. of the Cafe{OBJ} Symposium '98, Numazu, Japan" "1998" "april" "J. Rushby" "Critical System Properties: Survey and Taxonomy" "Reliability Engineering and System Safety" "1994" "43" "2" "189-219" "J. Rushby" "Fault Tolerance and Security" "1994" "J. Rushby" "Combining System Properties: {A} Cautionary Example and Formal Examination" "{Computer Science Laboratory, SRI International}" "1995" "june" "{Menlo Park, CA}" "Unpublished project report; available at url{http://www.csl.sri.com/~ rushby/combined.html}" "B. Schneier" "{Applied Cryptography}" "John Wiley & Sons" "1995" "" "" "" "2nd" "" "" "V. Shmatikov" "U. Stern" "{Efficient Finite State Analysis for Large Security Protocols}" "106-115" "W. Snyder" "{A Proof Theory for General Unification}" "Birkh{\"a}user" "1991" "" "" "" "" "" "" "M.-O. Stehr" "J. Meseguer" "{Pure Type Systems in Rewriting Logic}" "{Proc. of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999}" "1999" "" "" "" "" "" "" "P. Syverson" "C. A. Meadows" "{A Logical Language for Specifying Cryptographic Protocol Requirements}" "{Proc. IEEE Computer Society Symp. on Research in Security and Privacy, Oakland, CA}" "1993" "165-177" "" "" "" "may" "" "P. Syverson" "C. A. Meadows" "{Formal Requirements for Key Distribution Protocols}" "{Advances in Cryptology - EUROCRYPT'94}" "1995" "A. De Santis" "320-331" "" "Springer" "" "" "LNCS 950" "P. Syverson" "C. Meadows" "{A Formal Language for Cryptographic Protocol Requirements}" "Designs, Codes, and Cryptography" "1996" "7" "" "27-59" "" "" "P. Syverson" "M. Reed" "D. Goldschlag" "{Onion Routing Access Configurations}" "34-40" "N Venkatasubramanian" "C. L. Talcott" "{Reasoning about Meta Level Activities in Open Distributed Systems}" "{Principles of Distributed Computation}" "1995" "" "" "ACM" "" "" ""