@InCollection{ABB02,
  author        = {Alessandro Armando and David Basin and Mehdi Bouallagui
                  and Yannick Chevalier and Luca Compagna and Sebastian
                  M{\"o}dersheim and Michael Rusinowitch and Mathieu Turuani
                  and Luca Vigan{\`o} and Laurent Vigneron},
  title         = {The AVISS Security Protocol Analysis Tool},
  booktitle     = {Computer-Aided Verification CAV'02},
  pages         = {349--353},
  publisher     = {Springer-Verlag},
  series        = {Lecture Notes in Computer Science 2404},
  year          = 2002
}

@INPROCEEDINGS{AB02,
  AUTHOR = {Mart{\'\i}n Abadi and Bruno Blanchet},
  TITLE = {Analyzing {S}ecurity {P}rotocols with {S}ecrecy {T}ypes and {L}ogic {P}rograms},
  BOOKTITLE = {29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of 
Programming Languages (POPL 2002)},
  PAGES = {33--44},
  YEAR = 2002,
  PUBLISHER = {ACM Press}
}

@TechReport{AG98,
  author = 	 {M. Abadi and A. Gordon},
  title = 	 {A calculus for cryptographic protocols: the
{Spi} Calculus},
  institution =  {Digital Systems Research Center},
  year = 	 1998,
  number =	 {SRC-149}
}

@inproceedings{AKN01,
  author        = {Y. Amir and Y. Kim and C. Nita-Rotaru and J. Schultz and 
J. Stanton and G. Tsudik},
  title         = {Exploring Robustness in Group Key Agreement},
  booktitle     = {Proc. of the 21st IEEE Intern.\ Conf.\ on Distributed 
Computing Systems, Phoenix, Arizona, April 16-19, 2001.},
  publisher     = {},
  pages         = {399-408},
  year          = 2001,
  annote        = {SecureSpread}
}

@InProceedings{AL00,
  author = 	 {R. Amadio and D. Lugiez},
  title = 	 {On the reachability problem in cryptographic protocols},
  booktitle = 	 {CONCUR00},
  year =	 2000,
  number =	 1877,
  series =	 {LNCS},
  publisher =	 {Springer}
}

@TechReport{ALV01,
  author = 	 {R. Amadio and D. Lugiez and V. Vanack\`{e}re},
  title = 	 {On the symbolic reduction of processes with cryptographic
functions},
  institution =  {INRIA},
  year = 	 2001,
  number =	 4147,
  month =	 {March}
}

@InProceedings{AN94,
  author = 	 {M. Abadi and R. Needham},
  title = 	 {Prudent engineering practice for cryptographic protocols},
  booktitle = 	 {IEEE Symposium on Research in Security and Privacy},
  year =	 1994,
  organization = {IEEE Computer Society},
  pages =	 {122-136}
}


@InProceedings{AN95,
  author = 	 {R. Anderson and R. Needham},
  title = 	 {Robustness principles for public key protocols},
  booktitle = 	 {Advances in Cryptology - CRYPTO '95},
  volume =	 963,
  series =	 {Lecture Notes in Computer Science},
  year =	 1995,
  publisher =	 {Springer-Verlag},
  pages =	 {236-247}
}

@Article{AR02,
  author = 	 {M. Abadi and P. Rogaway},
  title = 	 {Reconciling two views of cryptography},
  journal = 	 {J. Cryptology},
  year = 	 2002,
  volume =	 15,
  number =	 2,
  pages =	 {103--127}
}

@InProceedings{AT91,
  author = 	 {M. Abadi and M. Tuttle},
  title = 	 {A semantics for a logic of authentication},
  booktitle = 	 {Proc. Tenth Annual ACM Symposium on Distributed Computing},
  pages =	 {201--216},
  year =	 1991,
  month =	 {August},
  publisher =	 {ACM Press}
}

@inproceedings{BD01,
    author = "David Basin and Grit Denker",
    title = "Maude versus Haskell: an Experimental Comparison in 
Security Protocol Analysis",
    booktitle = "Electronic Notes in Theoretical Computer Science",
    volume = "36",
    publisher = "Elsevier Science Publishers",
    editor = "Kokichi Futatsugi",
    year = "2001"
}

@Article{Bel89,
  author = 	 {S. Bellovin},
  title = 	 {Security Problems in the {TCP}/{IP} Protocol Suite},
  journaL = 	 {Computer Communications Review},
  year = 	 1989,
  volume =	 19,
  number =	 2,
  pages =	 {32-48},
  month =	 {April}
}

@inproceedings{Bas99,
    author = "David Basin",
    title = "Lazy Infinite-State Analysis of Security Protocols",
    booktitle = "SEcure Networking --- {CQRE} [Secure] '99",
    number = "1740",
    publisher = "Springer-Verlag",
    address = "D{\"u}sseldorf, Germany",
    pages = "30--42",
    year = "1999",
}


@InProceedings{Bla01,
  author = 	 {B. Blanchet},
  title = 	 {An efficient cryptographic protocol verifier based on {P}rolog
rules},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop},
  pages =	 {82--96},
  year =	 2001,
  organization = {IEEE Computer Society}
}

\bibitem[Bla01]{Bla01}
B. Blanchet.
\newblock An efficient cryptographic protocol verifier based on Prolog
rules.
\newblock {\em 14th IEEE Computer Security Foundations Workshop}, 2001, 82--96.

@InProceedings{BPW03,
  author = 	 {M. Backes and B. Pfitzmann and M. Waidner},
  title = 	 {A Composable Cryptographic Library with Nested Operations},
  booktitle = 	 {ACM Conference on Computer and Communications Security},
  year =	 2003,
  organization = {ACM SIGSAC}
}

@InProceedings{Ble98,
  author = 	 {D. Bleichenbacher},
  title = 	 {Chosen ciphertext attacks against protocols based on the 
{RSA} encryption standard {PKCS \#1}},
  booktitle = 	 {Advances in Cryptology - CRYPTO '98},
  pages =	 {1--12},
  year =	 1998,
  volume =	 1462,
  series =	 {LNCS},
  publisher =	 {Springer}
}

@InProceedings{BM93,
  author = 	 {S. Bellovin and M. Merritt},
  title = 	 {Augmented encrypted key exchange: a password-based
protocol secure against dictionary attacks and password file compromise},
  booktitle = 	 {First ACM Conference on Computer and
Communications Security},
  pages =	 {244--250},
  year =	 1993,
  organization = {ACM SIGSAC}
}

@InProceedings{BMM99,
  author = 	 {S. Brackin and C. Meadows and J. Millen},
  title = 	 {{CAPSL} interface for the {NRL} protocol analyzer},
  booktitle = 	 {2nd IEEE Workshop on Application-Specific Software Engineering and
Technology (ASSET '99)},
  year =	 1999,
  organization = {IEEE Computer Society}
}


@InProceedings{BMPT00,
  author = 	 {G. Bella and F. Massacci and L. Paulson and P. Tramontano},
  title = 	 {Formal verification of Cardholder Registration in {SET}},
  booktitle = 	 {Computer Security - ESORICS 2000},
  pages =	 {159--174},
  year =	 2000,
  volume =	 {LNCS 1895},
  publisher =	 {Springer}
}

@InProceedings{BMV03,
  author = 	 {D. Basin and S. Moedersheim and L. Vigano},
  title = 	 {Constraint Differentiation: A New Reduction Technique for 
Constraint-Based Analysis of Security Protocols},
  booktitle = 	 {ACM Conference on Computer and Communication Security},
  year =	 2003,
  organization = {ACM SIGSAC}
}

@inproceedings{Bol97,
  author = 	 {D. Bolignano},
  title = 	 {Towards the formal verification of electronic commerce
protocols},
  booktitle = 	 {IEEE Computer Security Foundations Workshop},
  year =	 1997,
  organization = {IEEE Computer Society},
  pages =	 {133--146},
  annote = 	 {Inductive verification using Coq proof assistant}
}

@InProceedings{Bor01,
  author = 	 {M Boreale},
  title = 	 {Symbolic analysis of cryptographic protocols in
the spi-calculus},
  booktitle = 	 {ICALP},
  pages =        {667--681},
  year =	 2001,
  volume =	 {LNCS 2076},
  publisher =	 {Springer}
}

@InProceedings{Bra97,
  author = 	 {S. Brackin},
  title = 	 {An interface specification language for automatically
analyzing cryptographic protocols},
  booktitle = 	 {Symposium on Network and Distributed System Security},
  year =	 1997,
  organization = {Internet Society},
  month =	 {February}
}

@InProceedings{Bra96,
  author = 	 {S. Brackin},
  title = 	 {A {HOL} extension of {GNY} for automatically analyzing
cryptographic protocols},
  booktitle = 	 {9th IEEE Computer Security Foundations Workshop},
  year =	 1996,
  organization = {IEEE Computer Society},
  pages =	 {62--77}
}

@Article{BAN90,
  author = 	 {M. Burrows and M. Abadi and R. Needham},
  title = 	 {A logic of authentication},
  journal = 	 {ACM Transactions on Computer Systems},
  year = 	 1990,
  volume =	 8,
  number =	 1,
  pages =	 {18-36}
}


@Article{BAN90a,
  author = 	 {M. Burrows and M. Abadi and R. Needham},
  title = 	 {Rejoinder to {N}essett},
  journal = 	 {ACM Operating Systems Review},
  year = 	 1990,
  volume =	 24,
  number =	 2,
  month =	 {April},
  pages =	 {39-40}
}

@InProceedings{Bra98,
  author = 	 {S. Brackin},
  title = 	 {Evaluating and improving protocol analysis by automatic proof},
  booktitle = 	 {11th IEEE Computer Security Foundations Workshop},
  year =	 1998,
  organization = {IEEE Computer Society},
  pages =	 {138-152}
}

@InProceedings{Bry97,
  author = 	 {J. Bryans and S. Schneider},
  title = 	 {{CSP}, {PVS}, and a recursive authentication protocol},
  booktitle = 	 {DIMACS Workshop on Design and Verification of Security
Protocols},
  year =	 1997
}

@Unpublished{CAP02,
  author = 	 {J. Millen},
  title = 	 {{CAPSL} {W}eb Site},
  year =         2003,
  note = 	 {{\tt http://www.csl.sri.com/users/millen/capsl}}
}

@InProceedings{Car94,
  author = 	 {U. Carlsen},
  title = 	 {Generating formal cryptographic protocol specifications},
  booktitle = 	 {IEEE Symposium on Research in Security and Privacy},
  year =	 1994,
  organization = {IEEE Computer Society},
  pages =	 {137-146}
}


@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 = 	 {12th IEEE Computer Security Foundations Workshop},
  pages =	 {55-69},
  year =	 1999,
  organization = {IEEE Computer Society}
}

@InProceedings{CDLMS00,
  author = 	 {I. Cervesato and N. Durgin and P. Lincoln and J. Mitchell
and A. Scedrov},
  title = 	 {Relating Strands and Multiset Rewriting for Security Protocol
Analysis},
  booktitle = 	 {13th IEEE Computer Security Foundations Workshop},
  year =	 2000,
  publisher =	 {IEEE Computer Society}
}

@InProceedings{CE02,
  author = 	 {R. Corin and S. Etalle},
  title = 	 {An Improved Constraint-based system for the verification 
of security protocols},
  booktitle = 	 {9th Int. Static Analysis Symp. (SAS)},
  pages =	 {326--341},
  year =	 2002,
  volume =	 {LNCS 2477},
  publisher =	 {Springer-Verlag}
}

@Unpublished{CJ97,
  author = 	 {J. Clark and J. Jacob},
  title = 	 {A Survey of Authentication Protocol Literature},
  note = 	 {{\tt http://www.cs.york.ac.uk/ \~{}jac/papers/drareviewps.ps}},
  year =	 1997
}


@InProceedings{CJM98,
  author = 	 {E. 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. IFIP Working Conference on Programming
Concepts and Methods (PROCOMET)},
  year =	 1998
}


@TechReport{CKRT03,
  author = 	 {Y. Chevalier and R. Kuesters and M. Rusinowitch and M. Turuani},
  title = 	 {Deciding the security of protocols with {D}iffie-{H}ellman
exponentiation and products in exponents},
  institution =  {CAU Kiel},
  year = 	 2003,
  type =	 {IFI-Report},
  number =	 0305
}

@article{CCM01,
    author = {Hubert Comon and V{\'e}ronique Cortier and John Mitchell},
    title = {Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols},
    journal = {Lecture Notes in Computer Science},
    volume = {2076},
    pages = {682--693},
    year = 2001}

@InProceedings{CMR01,
  author = 	 {V. Cortier and J. Millen and H. Rue{\ss}},
  title = 	 {Proving secrecy is easy enough},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop},
  year =	 2001,
  publisher =	 {IEEE Computer Society}
}

@Article{DH76,
  author = 	 {W. Diffie and M. Hellman},
  title = 	 {New directions in cryptography},
  journal = 	 {IEEE Trans. on Information Theory},
  year = 	 1976,
  volume =	 {IT-22},
  number =	 6,
  pages =	 {644--654}
}


@InProceedings{Den00,
  author = 	 {G. Denker},
  title = 	 {Design of a {CIL} connector to {Maude}},
  booktitle = 	 {Workshop on Formal Methods and Comuter Security},
  year =	 2000,
  editor =	 {H. Veith andN. Heintze and E. Clarke},
  month =	 {July},
  publisher =	 {Carnegie Mellon University}
}

@InProceedings{DFG99,
  author = 	 {A. Durante and R. Focardi and R. Gorrieri},
  title = 	 {{CVS}: a compiler for the analysis of cryptographic protocols},
  booktitle = 	 {12th IEEE Computer Security Foundations Workshop},
  pages =	 {203-213},
  year =	 1999,
  organization = {IEEE Computer Society}
}


@InProceedings{DMM02,
  author = 	 {G. Denker and J. Millen and Y. Miyake},
  title = 	 {Cross-Domain Access Control via {PKI}},
  booktitle = 	 {Policies for Distributed Systems and Networks},
  pages =	 {202--205},
  year =	 2002,
  month =	 {June},
  organization = {IEEE Computer Society}
}

@InProceedings{DMT98,
  author = 	 {G. Denker and J. Meseguer and C. Talcott},
  title = 	 {Protocol specification and analysis in {M}aude},
  booktitle = 	 {Formal Methods and Security Protocols},
  year =	 1998,
  note =	 {LICS '98 Workshop}
}

@InProceedings{DM99,
  author = 	 {G. Denker and J. Millen},
  title = 	 {{CAPSL} intermediate language},
  booktitle = 	 {FLoC Workshop on Formal Methods and Security Protocols},
  year =	 1999
}


@TechReport{DM99a,
  author = 	 {G. Denker and J. Millen},
  title = 	 {{CAPSL} and {CIL} language design},
  institution =  {SRI International Computer Science Laboratory},
  year = 	 1999,
  number =	 {SRI-CSL-99-02}
}


@InProceedings{DM00,
  author = 	 {G. Denker and J. Millen},
  title = 	 {{CAPSL} Integrated Protocol Environment},
  booktitle = 	 {DARPA Information Survivability Conference (DISCEX 2000)},
  pages =	 {207--221},
  year =	 2000,
  publisher =	 {IEEE Computer Society}
}

@InProceedings{DM02,
  author = 	 {G. Denker and J. Millen},
  title = 	 {Modeling group communication protocols using multiset
term rewriting},
  booktitle = 	 {4th International Workshop on Rewriting Logic and its Applications},
  year =	 2002,
  volume =	 {ENTCS 71},
  publisher =	 {Elsevier}
}

@TechReport{DMR00,
  author = 	 {G. Denker and J. Millen and H. Ruess},
  title = 	 {The {CAPSL} integrated protocol environment},
  institution =  {SRI International},
  year = 	 2000,
  number =	 {SRI-CSL-2000-02}
}

@InProceedings{DMKFG00,
  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,
  publisher =	 {IEEE Computer Society}
}

@Article{DS81,
  author = 	 {D. Denning and G. Sacco},
  title = 	 {Timestamps in key distribution protocols},
  journal = 	 {Communications of the ACM},
  year = 	 1981,
  volume =	 24,
  number =	 8,
  month =	 {August}
}


@InProceedings{DLMS99,
  author = 	 {N. Durgin and P. Lincoln and J. Mitchell and A. Scedrov},
  title = 	 {Undecidability of bounded security protocols},
  booktitle = 	 {Formal Methods and Security Protocols},
  year =	 1999,
  series =	 {Federated Logic Conference}
}

@TechReport{DS97,
  author = 	 {B. Dutertre and S. Schneider},
  title = 	 {Embedding {CSP} in {PVS}. {A}n application
to verify authentication protocols},
  institution =  {Royal Holloway, University of London},
  year = 	 1997,
  number =	 {CSD-TR-97-11},
  note =	 {To appear in TPHOLS '97}
}

@Article{DY83,
  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{EG83,
  author = 	 {S. Even and O. Goldreich},
  title = 	 {On the security of multi-party ping-pong protocols},
  booktitle = 	 {24th IEEE Symposium on Foundations of Computer Science},
  year =	 1983
}

@InProceedings{FA01,
  author = 	 {M. Fiore and M. Abadi},
  title = 	 {Computing symbolic models for verifying cryptographic protocols},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop},
  pages =	 {160--173},
  year =	 2001,
  organization = {IEEE Computer Society}
}

@Article{GM84,
  author = 	 {S. Goldwasser and S. Micali},
  title = 	 {Probabilistic encryption},
  journal = 	 {Journal of Computer and System Sciences},
  year = 	 1984,
  volume =	 28,
  pages =	 {270--299}
}

@InProceedings{GNY90,
  author = 	 {L. Gong and R. Needham and R. Yahalom},
  title = 	 {Reasoning about belief in cryptographic protocols},
  booktitle = 	 {IEEE Symposium on Research in Security and Privacy},
  year =	 1990,
  organization = {IEEE Computer Society},
  pages =	 {234-248}
}

@Article{Gon89,
  author = 	 {L. Gong},
  title = 	 {Using one-way functions for authentication},
  journal = 	 {Computer Communication Review},
  year = 	 1989,
  volume =	 19,
  number =	 5,
  pages =	 {8--11},
  month =	 {October}
}

@Article{Gon97,
  author = 	 {L. Gong},
  title = 	 {Enclaves: enabling secure collaboration over the {I}nternet},
  journal = 	 {IEEE J. of Selected Areas in Communications},
  year = 	 1997,
  volume =	 15,
  number =	 3,
  pages =	 {567--575},
  month =	 {April}
}

@InProceedings{HL99,
  author = 	 {M. Hui and G. Lowe},
  title = 	 {Safe simplifying transformations for security protocols},
  booktitle = 	 {12th IEEE Computer Security Foundations Workshop},
  year =	 1999,
  organization = {IEEE Computer Society},
  pages =        {32--41}
}

@InProceedings{HLS00,
  author = 	 {J. Heather and G. Lowe and S. Schneider},
  title = 	 {How to prevent type flaw attacks on security protocols},
  booktitle = 	 {13th IEEE Computer Security Foundations Workshop},
  pages =	 {255--268},
  year =	 2000,
  organization = {IEEE Computer Society}
}

@Article{HT96,
  author = 	 {N. Heintze and J. Tygar},
  title = 	 {A model for secure protocols and their compositions},
  journal = 	 {IEEE Transactions on Software Engineering},
  year = 	 1996,
  volume =	 22,
  number =	 1,
  month =	 {January},
  pages =	 {16-30}
}


@InProceedings{Hui99,
  author = 	 {A. Huima},
  title = 	 {Efficient infinite-state analysis of security protocols},
  booktitle = 	 {Workshop on Formal Methods and Security Protocols},
  year =	 1999,
  organization = {FLOC}
}

@inproceedings{JRV00,
    author = "Florent Jacquemard and Michael Rusinowitch and Laurent Vigneron",
    title = "Compiling and Verifying Security Protocols",
    booktitle = "Logic Programming and Automated Reasoning",
    pages = "131-160",
    year = "2000"
}

@Book{KPS95,
  author = 	 {C Kaufman and R. Perlman and M. Speciner},
  title = 	 {Network Security},
  publisher = 	 {Prentice Hall},
  year = 	 1995
}

@Article{Kem89,
  author = 	 {R. Kemmerer},
  title = 	 {Analyzing encryption protocols using formal verification
techniques},
  journal = 	 {IEEE Journal on Selected Areas in Communication},
  year = 	 1989,
  volume =	 7,
  number =	 4,
  month =	 {May}
}

@Article{KMM94,
  author = 	 {R. Kemmerer and C. Meadows and J. Millen},
  title = 	 {Three systems for cryptographic protocol analysis},
  journal = 	 {Journal of Cryptology},
  year = 	 1994,
  volume =	 7,
  number =	 2,
  pages =	 {79-130}
}

@techreport{Kra04,
            Url = {http://ic2.epfl.ch/publications/documents/IC_TECH_REPORT_200414.pdf},
            Title = {{CPL}: An evidence-based 5-dimensional 
logic for the compositional specification and verification of 
cryptographic protocols. {P}art {I}: language, process model, satisfaction},
            Year = 2004,
            Institution = {\'{E}cole Polytechnique F\'{e}d\'{e}rale de Lausanne, 
Switzerland},
            Number = {IC/2004/14},
            Author = {S. Kramer}
}

@InProceedings{KW96,
  author = 	 {D. Kindred and J. Wing},
  title = 	 {Fast, automatic checking of security protocols},
  booktitle = 	 {USENIX 2nd Workshop on Electronic Commerce},
  year =	 1996
}

@Article{Lam78,
  author = 	 {L. Lamport},
  title = 	 {Time, clocks, and the ordering of events in a distributed system},
  journal = 	 {Communications of the ACM},
  year = 	 1978,
  volume =	 21,
  number =	 7,
  pages =	 {558--564}
}

@InProceedings{LMMS98,
  author = 	 {P. Lincoln and J. Mitchell and M. Mitchell and A. Scedrov},
  title = 	 {A probabilistic poly-time framework for protocol analysis},
  booktitle = 	 {5th ACM Conference on Computer and Communications Security},
  pages =	 {112--121},
  year =	 1998,
  organization = {ACM SIGSAC}
}

@Article{Low98,
  author = 	 {G. Lowe},
  title = 	 {Casper: a compiler for the analysis of security protocols},
  journal = 	 {Journal of Computer Security},
  year = 	 1998,
  volume =	 6,
  number =	 1,
  pages =	 {53-84}
}


@InProceedings{Low98a,
  author = 	 {G. Lowe},
  title = 	 {Towards a completeness result for model checking of security
protocols},
  booktitle = 	 {11th IEEE Computer Security Foundations Workshop},
  year =	 1998,
  organization = {IEEE Computer Society},
  pages =	 {96-105}
}

@Article{Low99,
  author = 	 {G. Lowe},
  title = 	 {Towards a completeness result for model checking of security
protocols},
  journal = 	 {Journal of Computer Security},
  year = 	 1999,
  volume =	 7,
  number =	 {2/3},
  pages =	 {89--146}
}

@InProceedings{Low96,
  author = 	 {G. Lowe},
  title = 	 {Breaking and fixing the {N}eedham-{S}chroeder public-key
protocol using {FDR}},
  booktitle = 	 {Proceedings of TACAS},
  volume =	 1055,
  series =	 {Lecture Notes in Computer Science},
  year =	 1996,
  publisher =	 {Springer-Verlag},
  pages =	 {147-166}
}


@InProceedings{LM04,
  author = 	 {C. Lynch and C. Meadows},
  title = 	 {On the Relative Soundness of the Free Algebra Model for Public Key Encryption},
  booktitle = 	 {Workshop on Issues in the Theory of Security (WITS)},
  year =	 2004,
  organization = {IFIP WG 1.7}
}

@InProceedings{MCJ97,
  author = 	 {W. Marrero and E. Clarke and S. Jha},
  title = 	 {Model checking for security protocols},
  booktitle = 	 {DIMACS Workshop on Design and Verification of
Security Protocols},
  year =	 1997,
  organization = {Rutgers U.}
}

@InProceedings{Mea91,
  author = 	 {C. Meadows},
  title = 	 {A system for the specification and verification of key
management protocols},
  booktitle = 	 {IEEE Symposium on Security and Privacy},
  year =	 1991,
  organization = {IEEE Computer Society},
  pages =	 {182-195}
}


@Article{Mea92,
  author = 	 {C. Meadows},
  title = 	 {Applying formal methods to the analysis of a key
management protocol},
  journal = 	 {Journal of Computer Security},
  year = 	 1992,
  volume =	 1,
  number =	 1,
  pages =	 {5-36}
}

@Article{Mea96,
  author = 	 {C. Meadows},
  title = 	 {The {NRL} protocol analyzer: an overview},
  journal = 	 {Journal of Logic Programming},
  year = 	 1996,
  volume =	 26,
  number =	 2,
  pages =	 {113-131}
}


@InProceedings{Mea96a,
  author = 	 {C. Meadows},
  title = 	 {Language generation and verification in the {NRL}
protocol analyzer},
  booktitle = 	 {9th IEEE Computer Security Foundations Workshop},
  year =	 1996,
  organization = {IEEE Computer Society},
  pages =	 {48-61}
}

@InProceedings{Mea99,
  author = 	 {C. Meadows},
  title = 	 {Analysis of the internet key exchange protocol using 
the {NRL} protocol analyzer},
  booktitle = 	 {1999 IEEE Symposium on Security and Privacy},
  pages =	 {216-231},
  year =	 1999,
  organization = {IEEE Computer Society}
}


@InProceedings{Mea99c,
  author = 	 {C. Meadows},
  title = 	 {A formal framework and evaluation method for denial of service},
  booktitle = 	 {12th IEEE Computer Security Foundations Workshop},
  pages =	 {4--13},
  year =	 1999,
  organization = {IEEE Computer Society}
}

@InProceedings{MN02,
  author = 	 {C. Meadows and P. Narendran},
  title = 	 {A unification algorithm for the group {D}iffie-{H}ellman protocol},
  booktitle = 	 {Workshop on Issues in the Theory of Security},
  pages =	 {1--10},
  year =	 2002,
  volume =	 {WITS '02}
}

@InCollection{MG82,
  author = 	 {J. Meseguer and J. Goguen},
  title = 	 {Initiality, induction, and computability},
  booktitle = 	 {Algebraic Methods in Semantics},
  pages =	 {459-541},
  publisher =	 {Cambridge University Press},
  year =	 1982,
  editor =	 {M. Nivat and J. Reynolds}
}

@Article{MCF87,
  author = 	 {J. Millen and S. Clark and S. Freedman},
  title = 	 {The {I}nterrogator: protocol security analysis},
  journal = 	 {IEEE Transactions on Software Engineering},
  year = 	 1987,
  volume =	 {SE-13},
  number =	 2,
  month =	 {February},
  pages =	 {274-288}
}

@Article{MD02,
  author = 	 {J. Millen and G. Denker},
  title = 	 {{CAPSL} and {MuCAPSL}},
  journal = 	 {Journal of Telecommunications and Information Technology},
  year = 	 2002,
  number =	 4,
  pages =	 {16--27}
}

@InProceedings{MD03,
  author = 	 {J. Millen and G. Denker},
  title = 	 {{MuCAPSL}},
  booktitle = 	 {DISCEX III, DARPA Information Survivability Conference
and Exposition},
  pages =	 {238--249},
  year =	 2003,
  organization = {IEEE Computer Society}
}

@InProceedings{Mil01,
    author = {J. Millen},
    title = {Applications of Term Rewriting to Cryptographic Protocol Analysis},
    booktitle = {Electronic Notes in Theoretical Computer Science},
    volume = {36},
    publisher = {Elsevier Science Publishers},
    editor = {Kokichi Futatsugi},
    year = {2001}
}

@InProceedings{Mil95,
  author = 	 {J. Millen},
  title = 	 {The {I}nterrogator model},
  booktitle = 	 {IEEE Symposium on Security and Privacy},
  year =	 1995,
  organization = {IEEE Computer Society},
  pages =	 {251-260}
}


@TechReport{Mil97,
  author = 	 {J. Millen},
  title = 	 {{CAPSL}: {C}ommon {A}uthentication {P}rotocol
{S}pecification {L}anguage},
  institution =  {The MITRE Corporation},
  year = 	 1997,
  number =	 {MP 97B48}
}

@InProceedings{Mil00a,
  author = 	 {J. Millen},
  title = 	 {Applications of Term Rewriting to Cryptographic Protocol
   Analysis},
  booktitle = 	 {The 3rd International Workshop on Rewriting Logic and its
   Applications},
  year =	 2000,
  editor =	 {Kokichi Futatsugi},
  volume =	 36,
  series =	 {Electronic Notes in Theoretical Computer Science},
  publisher =	 {Elsevier Science},
  url =		 {http://www.elsevier.nl/locate/entcs/volume36.html}
}


@InProceedings{Mil00,
  author = 	 {J. Millen},
  title = 	 {A {CAPSL} Connector to {A}thena},
  booktitle = 	 {Workshop of Formal Methods and Computer Security},
  year =	 2000,
  editor =	 {H. Veith and N. Heintze and E. Clarke},
  organization = {CAV}
}

@InProceedings{Mil99,
  author = 	 {J. Millen},
  title = 	 {A necessarily parallel attack},
  booktitle = 	 {FLoC Workshop on Formal Methods and Security Protocols},
  year =	 1999
}

@Article{Mil03,
  author = 	 {J. Millen},
  title = 	 {On the freedom of decryption},
  journal = 	 {Information Processing Letters},
  year = 	 2003,
  volume =	 86,
  number =	 6,
  pages =	 {329--333},
  month =	 {June}
}


@Article{MMDTN03,
  author = 	 {Y. Miyake and J. Millen and G. Denker and T. Tanaka and K. Nakao},
  title = 	 {Notification of certificate revocation status between different
domains under a {PKI} system},
  journal = 	 {J. of the Information Processing Society of Japan},
  year = 	 2003,
  volume =	 44,
  number =	 6,
  pages =	 {1604--1612}
}

@InProceedings{MMS97,
  author = 	 {J. Mitchell and M. Mitchell and U. Stern},
  title = 	 {Automated analysis of cryptographic protocols using {M}ur$\phi$},
  booktitle = 	 {IEEE Symposium on Security and Privacy},
  year =	 1997,
  organization = {IEEE Computer Society},
  pages =	 {141-154}
}


@InProceedings{Mon99,
  author = 	 {D. Monniaux},
  title = 	 {Decision procedures for the analysis of cryptographic
protocols by logics of belief},
  booktitle = 	 {12th IEEE Computer Security Foundations Workshop},
  year =	 1999,
  organization = {IEEE Computer Society},
  pages =        {44-54}
}

@InProceedings{MR00,
  author = 	 {J. Millen and H. Rue{\ss}},
  title = 	 {Protocol-independent secrecy},
  booktitle = 	 {2000 IEEE Symposium on Security and Privacy},
  year =	 2000,
  organization = {IEEE Computer Society}
}

@TechReport{MM01,
  author = 	 {J. Millen and F. Muller},
  title = 	 {Cryptographic Protocol Generation from {CAPSL}},
  institution =  {SRI International},
  year = 	 2001,
  type =	 {Technical Report},
  number =	 {SRI-CSL-01-07},
  month =	 {December}
}

@InProceedings{MS01,
  author = 	 {J. Millen and V. Shmatikov},
  title = 	 {Constraint solving for bounded-process cryptographic
protocol analysis},
  booktitle = 	 {8th ACM
 Conference on Computer and Communication Security},
  pages =	 {166--175},
  year =	 2001,
  month =	 {November},
  organization = {ACM SIGSAC}
}

@InProceedings{MSS98,
  author = 	 {J. Mitchell and V. Shmatikov and U. Stern},
  title = 	 {Finite-State Analysis of {SSL} 3.0},
  booktitle = 	 {Seventh USENIX Security Symposium},
  pages =	 {201--216},
  year =	 1998
}

@InProceedings{MW00,
  author = 	 {J. Millen and R. Wright},
  title = 	 {Reasoning about trust and insurance in a public key infrastructure},
  booktitle = 	 {13th IEEE Computer Security Foundations Workshop},
  pages =	 {16--22},
  year =	 2000,
  organization = {IEEE Computer Society}
}

@InProceedings{MS03,
  author = 	 {J. Millen and V. Shmatikov},
  title = 	 {Symbolic protocol analysis with products and {Diffie-Hellman} exponentiation},
  booktitle = 	 {16th IEEE Computer Security Foundations Workshop},
  pages =	 {47--61},
  year =	 2003,
  organization = {IEEE Computer Society}
}

@Article{NS78,
  author = 	 {R. Needham and M. Schroeder},
  title = 	 {Using encryption for authentication in large networks
of computers},
  journal = 	 {Communications of the ACM},
  year = 	 1978,
  volume =	 21,
  number =	 12,
  month =	 {December},
  pages =	 {993-998}
}


@Article{Nes90,
  author = 	 {D. Nessett},
  title = 	 {A critique of the {B}urrows, {A}badi and {N}eedham logic},
  journal = 	 {ACM Operating Systems Review},
  year = 	 1990,
  volume =	 24,
  number =	 2,
  month =	 {April},
  pages =	 {35-38},
}

@InProceedings{ORS92,
  author = 	 {S. Owre and J. M. Rushby and N. Shankar},
  title = 	 {{PVS}: A Prototype Verification System},
  booktitle = 	 {11th International Conference on Automated Deduction
                (CADE)},
  pages =	 {748--752},
  year =	 1992,
  editor =	 {Deepak Kapur},
  volume =	 607,
  series =	 {Lecture Notes in Artificial Intelligence},
  publisher =	 {Springer-Verlag}
}



@Article{OR87,
  author = 	 {D. Otway and O. Rees},
  title = 	 {Efficient and timely mutual authentication},
  journal = 	 {ACM Operating System Review},
  year = 	 1987,
  volume =	 21,
  number =	 1,
  pages =	 {8-10}
}

@Article{Pau98,
  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{PQ01,
  author = 	 {O. Pereira and J. Quisquater},
  title = 	 {A security analysis of the Cliques protocol suites},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop},
  pages =	 {73--81},
  year =	 2001,
  organization = {IEEE Computer Society}
}


@InProceedings{PS00,
  author = 	 {A. Perrig and D. Song},
  title = 	 {A first step toward the automatic generation of 
security protocols},
  booktitle = 	 {Network and Distributed System Security Symposium},
  year =	 2000,
  month =	 {February},
  organization = {Internet Society}
}

@InProceedings{Ros95,
  author = 	 {A. W. Roscoe},
  title = 	 {Modelling and verifying key-exchange protocols
using {CSP} and {FDR}},
  booktitle = 	 {8th IEEE Computer Security Foundations Workshop},
  year =	 1995,
  organization = {IEEE Computer Society},
  pages =	 {98-107}
}

@inproceedings{RM00,
       AUTHOR = {H. Rue\ss\  and J. Millen},
       TITLE = {Local Secrecy for State-Based Models},
       BOOKTITLE = {Formal Methods in Computer Security, {CAV}
   workshop},
       YEAR = {2000},
       ADDRESS = {Chicago, {IL}},
       month = {july}
}

@InProceedings{RT01,
  author = 	 {M. Rusinowitch and M. Turuani},
  title = 	 {Protocol insecurity with finite number of sessions is
{NP}-complete},
  booktitle = 	 {14th IEEE Computer Security Foundations Workshop},
  pages =	 {174--190},
  year =	 2001,
  organization = {IEEE Computer Society}
}


@Book{RS01,
  author =	 {P. Ryan and S. Schneider},
  title = 	 {Modelling and Analysis of Security Protocols},
  publisher = 	 {Addison-Wesley},
  year = 	 2001
}

@Article{SBP01,
  author = 	 {D. Song and S. Berezin and A. Perrig},
  title = 	 {Athena: a novel approach to efficient automatic
security protocol analysis},
  journal = 	 {Journal of Computer Security},
  year = 	 2001,
  volume =	 9,
  number =	 1,
  pages =	 {47--74}
}

@inproceedings{SC00,
    author = "Paul F. Syverson and Iliano Cervesato",
    title = "The Logic of Authentication Protocols",
    booktitle = "{FOSAD}",
    pages = "63-136",
    year = "2000"}

@Book{Sch96,
  author = 	 {B. Schneier},
  title = 	 {Applied Cryptography},
  publisher = 	 {John Wiley},
  year = 	 1996
}


@Article{Sim94,
  author = 	 {G. Simmons},
  title = 	 {Cryptanalysis and protocol failures},
  journal = 	 {Communications of the ACM},
  year = 	 1994,
  volume =	 37,
  number =	 11,
  pages =	 {56-64},
  month =	 {November}
}


@InProceedings{SM00,
  author = 	 {V. Shmatikov and J. Mitchell},
  title = 	 {Analysis of Abuse-Free Contract Signing},
  booktitle = 	 {Financial Cryptography '00},
  year =	 2000,
  series =	 {LNCS 1962},
  publisher =	 {Springer}
}

@InProceedings{SM00a,
  author = 	 {V. Shmatikov and J. Mitchell},
  title = 	 {Analysis of a Fair Exchange Protocol},
  booktitle = 	 {Seventh Annual Symposium on Network and Distributed System Security},
  pages =	 {119--128},
  year =	 2000
}


@InProceedings{SS98,
  author = 	 {V. Shmatikov and U. Stern},
  title = 	 {Efficient finite-state analysis for large security protocols},
  booktitle = 	 {11th IEEE Computer Security Foundations Workshop},
  pages =	 {106-115},
  year =	 1998,
  organization = {IEEE Computer Society}
}

@Article{Sch98,
  author = 	 {S. Schneider},
  title = 	 {Verifying authentication protocols in {CSP}},
  journal = 	 {IEEE Transactions on Software Engineering},
  year = 	 1998,
  volume =	 24,
  number =	 9,
  month =	 {September},
  pages =	 {741-758}
}


@InProceedings{Shm02,
  author = 	 {V. Shmatikov},
  title = 	 {Probabilistic analysis of anonymity},
  booktitle = 	 {15th IEEE Computer Security Foundations Workshop},
  year =	 2002,
  publisher =	 {IEEE Computer Society}
}

@InProceedings{Son99,
  author = 	 {D. Song},
  title = 	 {Athena: a new efficient automatic checker for security
protocol analysis},
  booktitle = 	 {12th IEEE Computer Security Foundations Workshop},
  pages =	 {192-202},
  year =	 1999,
  organization = {IEEE Computer Society}
}

@InProceedings{SvO94,
  author = 	 {P. Syverson and P. van Oorschot},
  title = 	 {On unifying some cryptographic protocol logics},
  booktitle = 	 {IEEE Symposium on Research in Security and Privacy},
  year =	 1994,
  organization = {IEEE Computer Society},
  pages =	 {14-28}
}


@InProceedings{Sto98,
  author = 	 {S. Stoller},
  title = 	 {Justifying finite resources for adversaries in automated
analysis of authentication protocols},
  booktitle = 	 {Workshop on Formal Methods and Security Protocols},
  year =	 1998,
  organization = {FLOC}
}

@InProceedings{STW96,
  author = 	 {M. Steiner and G. Tsudik and M. Waidner},
  title = 	 {Diffie-{H}ellman key distribution extended to
group communication},
  booktitle = 	 {Proc. 3rd ACM Conference on Computer and Communications
Security},
  year =	 1996
}


@Article{STW00,
  author = 	 {M Steiner and G. Tsudik and M. Waidner},
  title = 	 {Key agreement in dynamic peer groups},
  journal = 	 {IEEE Trans. on Parallel and Distributed Systems},
  year = 	 2000,
  volume =	 11,
  number =	 8,
  pages =	 {769--780}
}

@InProceedings{Syv91,
  author = 	 {P. Syverson},
  title = 	 {The use of logics in the analysis of cryptographic
protocols},
  booktitle = 	 {IEEE Symposium on Research in Security and Privacy},
  year =	 1991,
  organization = {IEEE Computer Society},
  pages =	 {156-169}
}

@InProceedings{THG98,
  author = 	 {J. Thayer and J. Herzog and J. Guttman},
  title = 	 {Honest ideals on strand spaces},
  booktitle = 	 {11th IEEE Computer Security Foundations Workshop},
  year =	 1998,
  publisher =	 {IEEE Computer Society},
  pages =	 {66-78}
}


@InProceedings{THG98a,
  author = 	 {J. Thayer and J. Herzog and J. Guttman},
  title = 	 {Strand Spaces: Why is a Security Protocol Correct?},
  booktitle = 	 {1998 IEEE Symposium on Security and Privacy},
  pages =	 {160--171},
  year =	 1998,
  organization = {IEEE Computer Society}
}

@Article{THG99,
  author = 	 {J. Thayer and J. Herzog and J. Guttman},
  title = 	 {Strand spaces: proving security protocols correct},
  journal = 	 {Journal of Computer Security},
  year = 	 1999,
  volume =	 7,
  number =	 {2/3},
  pages =	 {191--230}
}

@Article{WL94,
  author = 	 {T. Woo and S. Lam},
  title = 	 {A lesson on authentication protocol design},
  journal = 	 {ACM Operating Systems Review},
  year = 	 1994,
  pages =	 {24--37}
}

@InProceedings{WLM00,
  author = 	 {R.Wright and P. Lincoln and J. Millen},
  title = 	 {Efficient Fault-Tolerant Certificate Revocation},
  booktitle = 	 {Conference on Computer and Communication
System Security},
  year =	 2000,
  organization = {ACM},
  month =        {September}
}

@Article{WLM01,
  author = 	 {R.Wright and P. Lincoln and J. Millen},
  title = 	 {Depender Graphs: A method of fault-tolerant certificate
distribution},
  journal = 	 {Journal of Computer Security},
  year = 	 2001,
  volume =	 9,
  number =	 4,
  pages =        {323--338}
}

@TechReport{YW93,
  author = 	 {A. Yasinsac and W. Wulf},
  title = 	 {A formal semantics for evaluating cryptographic protocols},
  institution =  {U. Virginia},
  year = 	 1993,
  number =	 {CS-93-53}
}