red
tr(replace(
@String{'TCS =    "Theoretical Computer Science"}
@String{'POPL =   "ACM~Symp. Principles of Programming Languages"}
@String{'SIGMOD = "ACM~SIGMOD Conf. on Management of Data"}
@String{'SIGPLAN = "ACM~SIGPLAN Notices"}
@String{'STOC =   "ACM~SIGACT Symp. on the Theory of Computing"}
@String{'ComACM = "Communications of the ACM"}
@String{'JACM =   "Journal ACM"}
@Unpublished{'00:_maude_web_site,
  key =          "MaudeWeb",
  title =        "{Maude Web Site}",
  year =         "2000",
  note =         "\url{http://maude.csl.sri.com/}"
}
@Proceedings{'88:_ieee_comput_secur_found_works,
  key =          "CSFW",
  title =        "{IEEE Computer Security Foundations Workshop}",
  booktitle =    "{IEEE Computer Security Foundations Workshop}",
  year =         "1988-2000",
  publisher =    "IEEE Computer Society",
  note =         "\url{http://www.csl.sri.com/csfw/}"
}

@Proceedings{'98:_ieee_comput_secur_found_works,
  title =        "{11th IEEE Computer Security Foundations Workshop, Rockport, Massachusetts, June 1998}",
  booktitle =    "{11th IEEE Computer Security Foundations Workshop, Rockport, Massachusetts, June 1998}",
  year =         "1998",
  publisher =    "IEEE Computer Society"
}
@Proceedings{'99:_ieee_comput_secur_found_works,
  title =        "{12th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 1999}",
  booktitle =    "{12th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 1999}",
  year =         "1999",
  publisher =    "IEEE Computer Society"
}

@InProceedings{'agha97:_abstr,
  author =	 "G. Agha",
  title =	 "{Abstracting interaction patterns: A programming paradigm for open distribute systems.}",
  booktitle =	 "{Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), Volume 2, IFIP TC6 WG6.1 Intern.\ Workshop, 21-23 July, Canterbury, Kent, UK}",
  year =	 "1997",
  editor =	 "H. Bowman and J. Derrick",
  pages =	 "135-153",
  organization = "",
  publisher =	 "Chapman & Hall",
  address =	 "",
  month =	 "",
  note =	 ""
}
@InProceedings{'basin00:_maude_haskel,
  author =       "D. Basin and G. Denker",
  title =        "{Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis}",
  year =         "2000",
  pages =        "235-256",
  organization = "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'bellovin93:_augmen_encry_key_exchan,
  author =       "S. M. Bellovin and M. Merritt",
  title =        "{Augmented Encrypted Key Exchange: A Password-Based Protocol Secure Against Dictionary Attacks and Password File Compromise}",
  booktitle =    "{1st ACM Conf. on Computer and Communications Security}",
  year =         "1993",
  pages =        "244-250",
  organization = "ACM SIGSAC",
  publisher =    "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'borovansky97:_strat_rewrit_elan,
  author =       "P. Borovansk\'y and C. Kirchner and H. Kirchner",
  title =        "{Strategies and Rewriting in {ELAN}}",
  booktitle =    "{Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia, July 1997)}",
  year =         "1997",
  editor =       "B. Gramlich and H. Kirchner",
  pages =        "",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'borovansky:_elan,
  author =       "P. Borovansk\'y and C. Kirchner and H. Kirchner and P.-E. Moreau and M. Vittek",
  title =        "{{ELAN}: A logical framework based on computational systems}",
  pages =        "",
  organization = "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'brackin99:_capsl_inter_nrl_protoc_analy,
  author =       "S. Brackin and C. Meadows and J. Millen",
  title =        "{CAPSL Interface for the NRL Protocol Analyzer}",
  booktitle =    "{IEEE Symposium on Application-Specific Systems and Software Engineering Technology, ASSET '99, Dallas }",
  year =         "1999",
  pages =        "",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "To appear"
}
@InProceedings{'brackin:_autom_detec_most_vulner_crypt_protoc,
  author =       "S. Brackin",
  title =        "{Automatically Detecting Most Vulnerabilities in Cryptographic Protocols}",
  pages =        "251-266",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "\url{http://schafercorp-ballston.com/discex/}"
}
@Proceedings{'budkowski98:_proc,
  editor =       "S. Budkowski and A. Cavalli and E. Najm",
  title =        "{Proc.\ Formal Description Techniques And Protocol Specification, Testing and Verification, FORTE XI/PSTV XVIII'98, 3-6 November, Paris, France}",
  booktitle =    "{Proc.\ Formal Description Techniques And Protocol Specification, Testing and Verification, FORTE XI/PSTV XVIII'98, 3-6 November, Paris, France}",
  publisher =    "Kluwer Academic Publishers",
  year =         "1998"
}
@Article{'chandy81:_proof_networ_proces,
  author =       "K. M. Chandy and J. Misra",
  title =        "Proofs of Networks of Processes",
  journal =      "{IEEE} Transactions on Software Engineering",
  volume =       "7",
  number =       "4",
  year =         "1981",
  pages =        "417-426"
}
@Book{'chandy88:_paral_progr_desig,
  author =       "K. Mani Chandy and Jayadev Misra",
  title =        "{Parallel Program Design: A Foundation}",
  publisher =    "Addison-Wesley",
  year =         "1988",
  address =      "",
  volume =       "",
  series =       "",
  edition =      "",
  month =        "",
  note =         ""
}
@Misc{'clavel98:_build_equat_provin_tools_reflec_rewrig_logic,
  author =       "M. Clavel and F. Dur{\'a}n and S. Eker and J. Meseguer",
  title =        "{Building Equational Proving Tools by Reflection in Rewriging Logic}",
  booktitle =    "{Proc.\ of the CafeOBJ Symp.'98, April, Japan}",
  year =         "1998",
  note =         ""
}
@Manual{'clavel99:_maude,
  title =        "{Maude: Specification and Programming in Rewriting Logic}",
  author =       "M. Clavel and F. Dur{\'a}n and S. Eker and P. Lincoln and N. Mart\'{\i}-Oliet and J. Meseguer and J. Quesada",
  organization = "SRI International, Computer Science Laboratory",
  address =      "Menlo Park, CA",
  edition =      "",
  month =        "january",
  year =         "1999",
  note =         "\url{http://maude.csl.sri.com/manual/}"
}
@InProceedings{'clavel:_princ_maude,
  author =       "M. Clavel and S. Eker and P. Lincoln and J. Meseguer",
  title =        "{Principles of Maude}",
  pages =        "65-89"
}
@InProceedings{'clavel:_reflec_strat_rewrit_logic,
  author =       "M. Clavel and J. Meseguer",
  title =        "{Reflection and Strategies in Rewriting Logic}",
  pages =        "125-147"
}
@TechReport{'denker00:_capsl_integ_protoc_envir,
  author =       "G. Denker and J. Millen",
  title =        "{The CAPSL Integrated Protocol Environment}",
  institution =  "{Computer Science Laboratory, SRI International, Menlo Park, CA 94025}",
  type =         "{CSL Report}",
  year =         "2000",
  number =       "{SRI-CSL-2000-02}",
  address =      "",
  month =        "",
  note =         "\url{http://www.csl.sri.com/~denker/pub_99.html}"
}
@InProceedings{'denker00:_optim_protoc_rewrit_rules_cil_specif,
  author =       "G. Denker and J. Millen and J. Kuester-Filipe and A. Grau",
  title =        "Optimizing Protocol Rewrite Rules of {CIL} Specifications",
  booktitle =    "13th IEEE Computer Security Foundations Workshop",
  year =         "2000",
  pages =        "52-62",
  publisher =    "IEEE Computer Society"
}
@InProceedings{'denker00:_rewrit_seman_meta_objec_compos_distr_servic,
  author =       "G. Denker and J. Meseguer and C. Talcott",
  title =        "{Rewriting Semantics of Meta-Objects and Composable Distributed Services}",
  year =         "2000",
  pages =        "407-427",
  organization = "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'denker98:_protoc_specif_analy_maude,
  author =       "G. Denker and J. Meseguer and C. Talcott",
  title =        "{Protocol Specification and Analysis in Maude}",
  booktitle =    "{Proc.\ of Workshop on Formal Methods and Security Protocols, 25 June 1998, Indianapolis, Indiana}",
  year =         "1998",
  editor =       "N. Heintze and J. Wing",
  pages =        "",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "\url{http://www.cs.bell-labs.com/who/nch/fmsp/index.html}"
}
@Article{'denker98:_schrit_schrit_ziel_entwur_infor_verfein,
  author =       "G. Denker",
  title =        "{Schritt f\"ur Schritt zum Ziel - Entwurf von Informationssystemen durch Verfeinerung}",
  journal =      "{erscheint in: Carolo-Wilhelmina-Mitteilungen, Sonderheft ``25 Jahre Informatik in Braunschweig''}",
  year =         "1998",
  volume =       "",
  number =       "",
  pages =        "",
  month =        "",
  note =         ""
}
@TechReport{'denker99:_capsl_cil_languag_desig,
  author =       "G. Denker and J. Millen",
  title =        "{CAPSL and CIL Language Design: A Common Authentication Protocol Specification Language and Its Intermediate Language}",
  institution =  "{Computer Science Laboratory, SRI International, Menlo Park, CA 94025}",
  type =         "{CSL Report}",
  year =         "1999",
  number =       "{SRI-CSL-99-02}",
  address =      "",
  month =        "",
  note =         "\url{http://www.csl.sri.com/~denker/pub_99.html}"
}
@InProceedings{'denker99:_specif_analy_reliab_broad_protoc_maude,
  author =       "G. Denker and J. J. Garcia-Luna-Aceves and J. Meseguer and P. {\"O}lveczky and J. Raju and B. Smith and C. Talcott",
  title =        "{Specification and Analysis of a Reliable Broadcasting Protocol in Maude}",
  booktitle =    "{Proc. 37th Allerton Conference on Communication, Control and Computation}",
  year =         "1999",
  editor =       "B. Hajek and R. S. Sreenivas",
  pages =        "",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "url{http://www.comm.csl.uiuc.edu/allerton}"
}
@TechReport{'denker99:_specif_reliab_broad_protoc_maude,
  author =       "G. Denker and J. J. Garcia-Luna-Aceves and J. Meseguer and P. {\"O}lveczky and J. Raju and B. Smith and C. Talcott",
  title =        "{Specifying a Reliable Broadcasting Protocol in Maude}",
  institution =  "{Computer Science Laboratory, SRI International, Menlo Park, CA 94025}",
  type =         "Internal report",
  year =         "1999",
  address =      "",
  month =        "",
  note =         "\url{http://www.csl.sri.com/~denker/pub_99.html}"
}
@InProceedings{'denker:_capsl_integ_protoc_envir,
  author =       "G. Denker and J. Millen",
  title =        "{CAPSL Integrated Protocol Environment}",
  pages =        "207-222",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "\url{http://schafercorp-ballston.com/discex/}"
}
@InProceedings{'denker:_capsl_inter_languag,
  author =       "G. Denker and J. Millen",
  title =        "{CAPSL Intermediate Language}",
  pages =        "",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "\url{http://cm.bell-labs.com/cm/cs/who/nch/fmsp99/}"
}
@InProceedings{'denker:_formal_specif_analy_activ_networ_commun_protoc,
  author =       "G. Denker and J. Meseguer and C. Talcott",
  title =        "{Formal Specification and Analysis of Active Networks and Communication Protocols: The Maude Experience}",
  pages =        "251-266",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "\url{http://schafercorp-ballston.com/discex/}"
}
@InProceedings{'denker:_from_rewrit_theor_tempor_logic_theor,
  author =       "G. Denker",
  title =        "{From Rewrite Theories to Temporal Logic Theories}",
  pages =        "",
  note =         ""
}
@Article{'denning81:_times_key_distr_protoc,
  author =       "D. E. Denning and G. M. Sacco",
  title =        "{Timestamps in Key Distribution Protocols}",
  journal =      'ComACM,
  year =         "1981",
  volume =       "24",
  number =       "8",
  pages =        "533-536",
  month =        "",
  note =         ""
}
@Article{'dolev83,
  author =       "D. Dolev and A. Yao",
  title =        "On the security of public key protocols",
  journal =      "IEEE Transactions on Information Theory",
  year =         "1983",
  volume =       "IT-29",
  pages =        "198-208",
  note =         "Also STAN-CS-81-854, May 1981, Stanford U."
}
@InProceedings{'duran:_exten_modul_algeb_for_maude,
  author =       "F. Dur{\'a}n and J. Meseguer",
  title =        "{An Extensible Module Algebra For Maude}",
  pages =        "",
  note =         "{\em to appear}"
}
@InProceedings{'dutertre97:_using_pvs_embed_csp_verif_authen_protoc,
  author =       "B. Dutertre and S. Schneider",
  title =        "{Using a PVS Embedding of CSP to Verify Authentication Protocols}",
  booktitle =    "{Theorem Proving in Higher Order Logics, TPHOL's 97}",
  year =         "1997",
  pages =        "121-136",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 1275"
}
@Misc{'feldmeier99:_protoc_boost,
  title =        "{Protocol Boosters}",
  author =       "D. Feldmeier and A. McAuley and J. Smith and D. Bakin and W. Marcus and T. Raleigh",
  howpublished = "",
  month =        "",
  year =         "1999",
  note =         "{Accepted for IEEE JSAC Special Issue on Protocol Architecures for the 21st Century.  Available at \url{http://carin.bellcore.com:8000/boosters/} under papers}"
}
@Proceedings{'futatsugi00:_third_inter,
  editor =       "K. Futatsugi",
  title =        "{Third Intern.\ Workshop on Rewriting Logic and Its Applications, Kanazawa City Cultural Hall, Kanazawa, Japan, September 18-20, 2000}",
  booktitle =    "{Third Intern.\ Workshop on Rewriting Logic and Its Applications, Kanazawa City Cultural Hall, Kanazawa, Japan, September 18-20, 2000}",
  publisher =    "Volume 36 of Elsevier Science B.V., Electronic Notes in Theoretical Computer Science, \url{http://www.elsevier.nl/locate/entcs/volume36 .html}",
  year =         "2000"
}
@Misc{'garcia-luna98:_reliab_broad_comput_networ,
  author =       "J. J. Garc\'{\i}a-Luna",
  title =        "{Reliable Broadcasing in Computer Networks}",
  howpublished = "{Manuscript; University of California at Santa Cruz, Computer Science Department}",
  month =        "january",
  year =         "1998",
  note =         ""
}
@Article{'goguen92:_order_i,
  author =       "J. Goguen and J. Meseguer",
  title =        "{Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations}",
  journal =      'TCS,
  year =         "1992",
  volume =       "2",
  number =       "105",
  pages =        "",
  month =        "",
  note =         ""
}
@Article{'goldschlag99:_onion_routin_anony_privat_inter_connec,
  author =       "D. Goldschlag and M. Reed and P. Syverson",
  title =        "Onion Routing for Anonymous and Private Internet Connections",
  journal =      "Communications of the ACM",
  year =         "1999",
  volume =       "42",
  number =       "2",
  pages =        "",
  month =        "february"
}
@InProceedings{'gray95:_using_tempor_logic_specif_verif,
  author =       "J. W. Gray and J. D. McLean",
  title =        "{Using Temporal Logic to Specify and Verify Cryptographic Protocols (Progress Report)}",
  booktitle =    "{Proc. of the 8th IEEE Computer Security Foundations Workshop}",
  year =         "1995",
  pages =        "108-116",
  organization = "",
  publisher =    "IEEE Computer Society Press",
  address =      "",
  month =        "",
  note =         ""
}
@Proceedings{'heintze99:_works_formal_method_secur_protoc,
  editor =       "N. Heintze and E. Clarke",
  title =        "{Workshop on Formal Methods and Security Protocols (FMSP'99), July 5, 1999, Trento, Italy (part of FLOC'99)}",
  booktitle =    "{Workshop on Formal Methods and Security Protocols (FMSP'99), July 5, 1999, Trento, Italy (part of FLOC'99)}",
  year =         "1999",
  publisher =    ""
}

@InProceedings{'hicks98:_plan,
  author =       "M. Hicks and P. Kakkar and J. T. Moore and C. A. Gunter and S. Nettles",
  title =        "{PLAN: A Packet Language for Active Networks}",
  booktitle =    "Proceedings of the Third {ACM} {SIGPLAN} International Conference on Functional Programming Languages",
  year =         "1998",
  pages =        "86-93",
  publisher =    "ACM",
  url =          "http://www.cis.upenn.edu/~switchware/papers/plan.ps"
}
@Book{'hoare85:_commun_sequen_proces,
  author =       "C. A. R. Hoare",
  title =        "{Communicating Sequential Processes}",
  publisher =    "Prentice Hall International",
  year =         "1985",
  note =         ""
}
@TechReport{'johnson00:_introd_ip_multic_routin,
  author =       "V. Johnson and M. Johnson",
  title =        "{Introduction to IP Multicast Routing. An IP Multicast Initiative White Paper}",
  institution =  "{IP Multicast Initiative (IPMI), Stardust Technologies, Inc}",
  type =         "",
  year =         "2000",
  address =      "",
  month =        "",
  note =         "\url{http://www.ipmulticast.com/community/whitepapers/intror outing.html}"
}
@InProceedings{'kiczales97:_aspec_orien_progr,
  author =       "G. Kiczales and J. Lamping and A. Mendhekar and C. Maeda and C. Lopes and J.-M. Loingtier and J. Irwin",
  title =        "{Aspect-Oriented Programming}",
  booktitle =    "{Proc.\ of the European Conference on Object-Oriented Programming (ECOOP'97), Finland}",
  year =         "1997",
  editor =       "M. Aksit and S. Matsuoka",
  pages =        "220-242",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "{LNCS 1241, \url{http://www.parc.xerox.com/spl/groups/eca/pu bs/papers/Kiczales-ECOOP97/}}"
}
@Proceedings{'kirchner98:_int,
  editor =       "H. Kirchner and C. Kirchner",
  title =        "{2nd Int.\ Workshop on Rewriting Logic and Its Applications (WRLA'98), Pont-A-Mousson, France, September 1-4, 1998}",
  booktitle =    "{2nd Int.\ Workshop on Rewriting Logic and Its Applications (WRLA'98), Pont-A-Mousson, France, September 1-4, 1998}",
  publisher =    "{Elsevier Science B.V., Volume 15 of Electronic Notes in Theoretical Computer Science, \url{http://www.elsevier.nl/locate/entcs/volume15 .html}}",
  year =         "1998"
}
@InProceedings{'kosiuczenko95:_timed_rewrit_logic_specif_time_sensit_system,
  author =       "P. Kosiuczenko and M. Wirsing",
  title =        "{Timed Rewriting Logic for the Specification of Time-Sensitive Systems}",
  booktitle =    "{Proc.\ of the Intern.\ Summer School on Proof and Computation}",
  year =         "1995",
  editor =       "H. Schwichtenberg",
  pages =        "",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "NATO-ASI Series"
}
@Article{'lam90,
  author =       "Simon S. Lam and A Udayar Shankar",
  title =        "{A relational notation for state transition systems}",
  journal =      'SE,
  year =         "1990",
  volume =       "16",
  number =       "7",
  pages =        "755-775",
  month =        "july",
  note =         ""
}
@InProceedings{'laporta:_protoc_featur_inter,
  author =       "T. F. LaPorta and D. Lee and Y.-J. Lin and M. Yannakakis",
  title =        "{Protocol Feature Interactions}",
  pages =        "59-74",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'lechner96:_modal,
  author =       "U. Lechner and C. Lengauer",
  title =        "{Modal--$\mu$--Maude --- Specification and Properties of Concurrent Objects}",
  booktitle =    "{Object Orientation with Parallelism and Persistence}",
  year =         "1996",
  editor =       "{B.~Freitag and C. B.~Jones and C.~Lengauer and H.-J.~Schek}",
  pages =        "23-46",
  organization = "",
  publisher =    "Kluwer",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'lopes98:_recen_devel_aspec,
  author =       "C. Lopes and G. Kiczales",
  title =        "{Recent Developments in AspectJ}",
  booktitle =    "{ECOOP'98 Workshop Reader, Workshop on Aspect-Oriented Programming}",
  year =         "1998",
  pages =        "",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 1543, \url{http://www.parc.xerox.com/spl/groups/eca/pub s/papers/Lopes-AOPW-ECOOP98/}"
}
@InProceedings{'lowe96:_break_fixin_needh_schroed_public,
  author =       "G. Lowe",
  title =        "{Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR}",
  booktitle =    "{Second Intern.\ Workshop TACAS'96, Passau, Germany, March 1996}",
  year =         "1996",
  pages =        "147-166",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 1055"
}
@Misc{'mallet98:_operat_system_suppor_protoc_boost,
  author =       "A. Mallet and J. D. Chung and J. M. Smith",
  title =        "{Operating System Support for Protocol Boosters}",
  howpublished = "",
  month =        "",
  year =         "1998",
  note =         "{available at \url{http://carin.bellcore.com:8000/boosters/} under papers}"
}
@TechReport{'marti-oliet93:_rewrit_logic_logic_seman_framew,
  author =       "N. Mart\'{\i}-Oliet and J. Meseguer",
  title =        "{Rewriting Logic as a Logical and Semantic Framework}",
  institution =  "SRI International, Computer Science Laboratory, Menlo Park, CA",
  type =         "{CSL Technical Report}",
  year =         "1993",
  number =       "{93-05}",
  address =      "",
  month =        "august",
  note =         ""
}
@InCollection{'marti-oliet94:_gener_logic_logic_framew,
  author =       "N. Mart\'{\i}-Oliet and J. Meseguer",
  title =        "General {L}ogics and {L}ogical {F}rameworks",
  editor =       "D. Gabbay",
  booktitle =    "What is a Logical System?",
  year =         "1994",
  pages =        "355-392",
  publisher =    "Oxford University Press"
}
@TechReport{'marti-oliet96:_action_chang_rewrit_logic,
  author =       "N. Mart\'{\i}-Oliet and J. Meseguer",
  title =        "{Action and Change in Rewriting Logic}",
  institution =  "SRI International, Menlo Park, CA",
  type =         "{CSL Technical Report}",
  year =         "1996",
  number =       "{}",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'marti-oliet:_rewrit_logic_logic_seman_framew,
  author =       "N. Mart\'{\i}-Oliet and J. Meseguer",
  title =        "{Rewriting Logic as a Logical and Semantic Framework}",
  pages =        "189-225"
}
@Proceedings{'maughan00:_proc,
  editor =       "D. Maughan and G. Koob and S. Saydjari",
  title =        "{Proc.\ DARPA Information Survivability Conference and Exposition, DISCEX2000, January 25-27, Hilton Head Island, SC, USA}",
  booktitle =    "{Proc.\ DARPA Information Survivability Conference and Exposition, DISCEX2000, January 25-27, Hilton Head Island, SC, USA}",
  publisher =    "IEEE Computer Society Press",
  year =         "2000"
}
@InProceedings{'meadows95:_formal_verif_crypt_protoc,
  author =       "C. A. Meadows",
  title =        "{Formal Verification of Cryptographic Protocols: A Survey}",
  booktitle =    "{Advances in Cryptology - Asiacrypt '94}",
  year =         "1995",
  editor =       "J. Pieprzyk and R. Savafi-Naini",
  pages =        "133-150",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 917"
}
@InProceedings{'meadows96:_analy_needh_schroed_public_key_protoc,
  author =       "C. A. Meadows",
  title =        "{Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches}",
  booktitle =    "{Proc.\ of European Symposium on Research in Computer Security (ESORICS'96)}",
  year =         "1996",
  editor =       "E. Bertino and H. Kurth and G. Martella and E. Montolivo",
  pages =        "351-364",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 1146"
}
@InProceedings{'meadows96:_languag_gener_verif_nrl_protoc_analy,
  author =       "C. A. Meadows",
  title =        "{Language Generation and Verification in the NRL Protocol Analyzer}",
  booktitle =    "{Proc. 9th Computer Security Foundations Workshop}",
  year =         "1996",
  pages =        "48-61",
  organization = "",
  publisher =    "IEEE Computer Society Press",
  address =      "",
  month =        "june",
  note =         ""
}
@Article{'meseguer92:_condit_rewrit_logic_unified_model_concur,
  author =       "J. Meseguer",
  title =        "{Conditional Rewriting Logic as a Unified Model of Concurrency}",
  journal =      'TCS,
  year =         "1992",
  volume =       "96",
  number =       "1",
  pages =        "73-155",
  month =        "",
  note =         ""
}
@InCollection{'meseguer93:_logic_theor_concur_objec_its,
  author =       "J. Meseguer",
  title =        "{A Logical Theory of Concurrent Objects and Its Realization in the Maude Language}",
  booktitle =    "Research Directions in Concurrent Object-Oriented Programming",
  publisher =    "The MIT Press",
  year =         "1993",
  editor =       "G. Agha and P. Wegner and A. Yonezawa",
  chapter =      "",
  pages =        "314-390",
  address =      "",
  month =        "",
  note =         ""
}
@Proceedings{'meseguer96:_rewrit_logic_its_applic_first,
  editor =       "J. Meseguer",
  title =        "{Rewriting Logic and Its Applications, First International Workshop, Asilomar Conference Center, Pacific Grove, CA, September 3-6, 1996}",
  booktitle =    "{Rewriting Logic and Its Applications, First International Workshop, Asilomar Conference Center, Pacific Grove, CA, September 3-6, 1996}",
  publisher =    "Elsevier Science B.V., Electronic Notes in Theoretical Computer Science, Volume 4, \url{http://www.elsevier.nl/locate/entcs/volume4.ht ml}",
  year =         "1996"
}

@InProceedings{'meseguer96:_rewrit_logic_seman_framew_concur,
  author =       "J. Meseguer",
  title =        "{Rewriting Logic as a Semantic Framework for Concurrency: A Progress Report}",
  booktitle =    "{Proc.\ 7th Intern.\ Conf.\ on Concurrency Theory: CONCUR'96, Pisa, August 1996}",
  year =         "1996",
  editor =       "U. Montanari and V. Sassone",
  pages =        "331-372",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "LNCS 1119"
}
@InCollection{'meseguer98:_resear_direc_rewrit_logic,
  author =       "J. Meseguer",
  title =        "{Research Directions in Rewriting Logic}",
  booktitle =    "{Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 -- August 6, 1997}",
  publisher =    "{Springer Verlag}",
  year =         "1998",
  editor =       "{U. Berger and H. Schwichtenberg}",
  chapter =      "",
  pages =        "347-398",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'meseguer99:_partial_order_event_model_concur_objec,
  title =        "{A Partial Order Event Model for Concurrent Objects}",
  author =       "J. Meseguer and C. Talcott",
  booktitle =    "{Proc.\ 10th Intern.\ Conf.\ on Concurrency Theory (CONCUR'99), Eindhoven, The Netherlands, August 1999}",
  editor =       "J. C. M Baeten and S. Mauw",
  year =         "1999",
  pages =        "415-430",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 1664"
}
@TechReport{'millen98:_neces_concur_attac,
  author =       "J. Millen",
  title =        "{A Necessarily Concurrent Attack}",
  institution =  "SRI International, Menlo Park, CA 94025",
  type =         "",
  year =         "1998",
  number =       "{}",
  address =      "",
  month =        "",
  note =         "\url{www.csl.sri.com/~millen}"
}
@InProceedings{'millen99:_local_recon_polic,
  author =       "J. Millen",
  title =        "{Local Reconfiguration Policies}",
  booktitle =    "{IEEE Symposium on Security and Privacy}",
  year =         "1999",
  pages =        "",
  organization = "IEEE Computer Society",
  publisher =    "",
  address =      "",
  month =        "",
  note =         "{\em To appear}"
}
@Misc{'mitchell98,
  title =         "Overview of Formal Methods for Security Protocol Analysis",
  author =       "J. Mitchell",
  howpublished = "Invited Talk, CAV'98, slides",
  month =        "",
  year =         "1998",
  note =         "\url{http://theory.stanford.edu/people/jcm/home.html}"
}
@Article{'needham78:_using,
  author =       "R. Needham and M. Schroeder",
  title =        "{Using encryption for authentication in large networks of computers}",
  journal =      'ComACM,
  year =         "1978",
  volume =       "21",
  number =       "12",
  pages =        "993-999",
  month =        "",
  note =         ""
}
@TechReport{'oelveczky97:_objec_orien_algeb_steam_boiler_contr_specif,
  author =       "P. {\"O}lveczky and P. Kosiuczenko and M. Wirsing",
  title =        "{An Object-Oriented Algebraic Steam-Boiler Control Specification}",
  institution =  "Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen, Inst. f. Informatik",
  type =         "{Technical report}",
  year =         "1997",
  number =       "{9701}",
  address =      "",
  month =        "january",
  note =         ""
}
@InProceedings{'oelveczky:_specif_real_time_system_rewrit_logic,
  author =       "P. {\"O}lveczky and J. Meseguer",
  title =        "{Specifying Real-Time Systems in Rewriting Logic}",
  pages =        "283-308"
}
@Article{'paulson98,
  author =       "L Paulson",
  title =        "The inductive approach to verifying cryptographic protocols",
  journal =      "Journal of Computer Security",
  year =         "1998",
  volume =       "6",
  number =       "1",
  pages =        "85-128"
}
@InProceedings{'peleska94,
  author =       "J. Peleska",
  title =        "{On a unified formal approach for the development of fault-tolerant and secure systems}",
  booktitle =    "{Nordic Seminar on Dependable Computing Systems, Lyngby, Denmark, August 1994. Technical University of Denmark}",
  year =         "1994",
  editor =       "H. Rischel",
  pages =        "69-80",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'pita:_maude_specif_objec_orien_datab,
  author =       "I. Pita and N. Mart\'{\i}-Oliet",
  title =        "{A Maude Specification of an Object Oriented Database Model for Telcommunication Networks}",
  pages =        "404-422"
}
@Book{'project98:_proc,
  author =       "{CafeOBJ Project}",
  title =        "Proc. of the Cafe{OBJ} Symposium '98, Numazu, Japan",
  year =         "1998",
  month =        "april"
}
@Article{'rushby94:_critic_system_proper,
  author =       "J. Rushby",
  title =        "Critical System Properties: Survey and Taxonomy",
  journal =      "Reliability Engineering and System Safety",
  year =         "1994",
  volume =       "43",
  number =       "2",
  pages =        "189-219"
}
@Misc{'rushby94:_fault_toler_secur,
  author =       "J. Rushby",
  title =        "Fault Tolerance and Security",
  year =         "1994"
}
@TechReport{'rushby95:_combin_system_proper,
  author =       "J. Rushby",
  title =        "Combining System Properties: {A} Cautionary Example and Formal Examination",
  institution =  "{Computer Science Laboratory, SRI International}",
  year =         "1995",
  month =        "june",
  address =      "{Menlo Park, CA}",
  note =         "Unpublished project report; available at \url{http://www.csl.sri.com/~ rushby/combined.html}"
}
@Book{'schneier95:_applied_crypt,
  author =       "B. Schneier",
  title =        "{Applied Cryptography}",
  publisher =    "John Wiley & Sons",
  year =         "1995",
  address =      "",
  volume =       "",
  series =       "",
  edition =      "2nd",
  month =        "",
  note =         ""
}
@InProceedings{'shmatikov:_effic_finit_state_analy_large_secur_protoc,
  author =       "V. Shmatikov and U. Stern",
  title =        "{Efficient Finite State Analysis for Large Security Protocols}",
  pages =        "106-115"
}
@Book{'snyder91:_proof_theor_gener_unific,
  author =       "W. Snyder",
  title =        "{A Proof Theory for General Unification}",
  publisher =    "Birkh{\"a}user",
  year =         "1991",
  address =      "",
  volume =       "",
  series =       "",
  edition =      "",
  month =        "",
  note =         ""
}
@InProceedings{'stehr99:_pure_type_system_rewrit_logic,
  author =       "M.-O. Stehr and J. Meseguer",
  title =        "{Pure Type Systems in Rewriting Logic}",
  booktitle =    "{Proc. of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999}",
  year =         "1999",
  pages =        "",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "",
  note =         ""
}
@InProceedings{'syverson93:_logic_languag_specif_crypt_protoc_requir,
  author =       "P. Syverson and C. A. Meadows",
  title =        "{A Logical Language for Specifying Cryptographic Protocol Requirements}",
  booktitle =    "{Proc.\ IEEE Computer Society Symp. on Research in Security and Privacy, Oakland, CA}",
  year =         "1993",
  pages =        "165-177",
  organization = "",
  publisher =    "",
  address =      "",
  month =        "may",
  note =         ""
}
@InProceedings{'syverson95:_formal_requir_key_distr_protoc,
  author =       "P. Syverson and C. A. Meadows",
  title =        "{Formal Requirements for Key Distribution Protocols}",
  booktitle =    "{Advances in Cryptology - EUROCRYPT'94}",
  year =         "1995",
  editor =       "A. De Santis",
  pages =        "320-331",
  organization = "",
  publisher =    "Springer",
  address =      "",
  month =        "",
  note =         "LNCS 950"
}
@Article{'syverson96:_formal_languag_crypt_protoc_requir,
  author =       "P. Syverson and C. Meadows",
  title =        "{A Formal Language for Cryptographic Protocol Requirements}",
  journal =      "Designs, Codes, and Cryptography",
  year =         "1996",
  volume =       "7",
  number =       "",
  pages =        "27-59",
  month =        "",
  note =         ""
}
@InProceedings{'syverson:_onion_routin_acces_config,
  author =       "P. Syverson and M. Reed and D. Goldschlag",
  title =        "{Onion Routing Access Configurations}",
  pages =        "34-40"
}
@InProceedings{'venkatasubramanian95:_reason_meta_level_activ_open_distr_system,
  author =       "N Venkatasubramanian and C. L. Talcott",
  title =        "{Reasoning about Meta Level Activities in Open Distributed Systems}",
  booktitle =    "{Principles of Distributed Computation}",
  year =         "1995",
  pages =        "",
  organization = "",
  publisher =    "ACM",
  address =      "",
  month =        "",
  note =         ""
}


))
.