@book{Milner,
 author = {R. Milner},
 title = {Communicating and mobile systems: the pi calculus},
 year = {1999},
 isbn = {052164320},
 publisher = {Cambridge University Press},
 }

@inproceedings{MACF,
  author    = {M. Abadi and C. Fournet},
  title     = {Mobile values, new names, and secure communication},
  booktitle = {POPL},
  year      = {2001},
  pages     = {104-115},
  ee        = {http://doi.acm.org/10.1145/360204.360213},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{MAG,
 author = {M. Abadi and A.D. Gordon},
 title = {A calculus for cryptographic protocols: the spi calculus},
 booktitle = {CCS '97: Proceedings of the 4th ACM conference on Computer and communications security},
 year = {1997},
 isbn = {0-89791-912-2},
 pages = {36--47},
 doi = {http://doi.acm.org/10.1145/266420.266432},
 publisher = {ACM},
 }

@article{MHHL,
 author = {Hennessy, M. and Lin, H.},
 title = {Symbolic bisimulations},
 journal = {Theor. Comput. Sci.},
 volume = {138},
 number = {2},
 year = {1995},
 issn = {0304-3975},
 pages = {353--389},
 doi = {http://dx.doi.org/10.1016/0304-3975(94)00172-F},
 publisher = {Elsevier Science Publishers Ltd.},
 }

 @article{HL96,
  author    = {M. Hennessy and H. Lin},
  title     = {Proof Systems for Message-Passing Process Algebras},
  journal   = {Formal Asp. Comput.},
  volume    = {8},
  number    = {4},
  year      = {1996},
  pages     = {379-407},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{MBR,
  author    = {M. Boreale and
               R. De Nicola},
  title     = {A Symbolic Semantics for the pi-Calculus},
  journal   = {Inf. Comput.},
  volume    = {126},
  number    = {1},
  year      = {1996},
  pages     = {34-52},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{HL,
  author    = {H. Lin},
  title     = {Complete inference systems for weak bisimulation equivalences
               in the pi-calculus},
  journal   = {Inf. Comput.},
  volume    = {180},
  number    = {1},
  year      = {2003},
  pages     = {1-29},
  ee        = {http://dx.doi.org/10.1016/S0890-5401(02)00014-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@inproceedings{LL,
 author = {Liu, J and Lin, H},
 title = {A Complete Symbolic Bisimulation for Full Applied Pi Calculus},
 booktitle = {SOFSEM '10: Proceedings of the 36th Conference on Current Trends in Theory and Practice of Computer Science},
 year = {2010},
 isbn = {978-3-642-11265-2},
 pages = {552--563},
 location = {`pindlerov Ml\'{y}n, Czech Republic},
 doi = {http://dx.doi.org/10.1007/978-3-642-11266-9_46},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 }




@misc{LL09,
   author = {J. Liu and H.Lin},
   title = {A complete symbolic bisimulation for full
applied pi calculus (full version)},
   year = {2009},
   note = {Available at \url{http://lcs.ios.ac.cn/~jliu}}
}

@misc{LL10,
   author = {J. Liu and H.Lin},
   title = {Proof System for applied pi calculus (full version)},
   year = {2010},
   note = {Available at \url{http://lcs.ios.ac.cn/~jliu}}
}

@misc{JCJJ97,
   author = {J. Clark and J. Jacob },
   title = {A survey of authentication
protocol literature},
   year = {1997},
   note = {Available at \url{ http://www.cs.york.ac.uk/~jac/
papers/drareviewps.ps}}
}

@misc{MJBVJP09,
   author = { M. Johansson and B. Victor, and J. Parrow },
   title = {A fully abstract symbolic semantics for psi-calculi. },
   year = {2009},
   note = {Accepted for SOS'09}
}

  , 2009.


@inproceedings{JMVS,
 author = {Millen, J. and Shmatikov, V.},
 title = {Constraint solving for bounded-process cryptographic protocol analysis},
 booktitle = {CCS '01: Proceedings of the 8th ACM conference on Computer and Communications Security},
 year = {2001},
 isbn = {1-58113-385-5},
 pages = {166--175},
 doi = {http://doi.acm.org/10.1145/501983.502007},
 publisher = {ACM},
 }

@inproceedings{BB,
 author = {Blanchet, B.},
 title = {An Efficient Cryptographic Protocol Verifier Based on Prolog Rules},
 booktitle = {CSFW '01: Proceedings of the 14th IEEE workshop on Computer Security Foundations},
 year = {2001},
 pages = {82},
 }

@inproceedings{HCVS,
 author = {Comon-Lundh, H. and Shmatikov, V.},
 title = {Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or},
 booktitle = {LICS '03: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science},
 year = {2003},
 isbn = {0-7695-1884-2},
 pages = {271},
 }




@inproceedings{DKR07,
  author    = {S. Delaune and
               S. Kremer and
               M.D. Ryan},
  title     = {Symbolic Bisimulation for the Applied Pi Calculus},
  booktitle = {FSTTCS},
  year      = {2007},
  pages     = {133-145},
  ee        = {http://dx.doi.org/10.1007/978-3-540-77050-3_11},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DKR09b,
   author = {Delaune, S. and Kremer, S. and Ryan, M.D.},
   journal = {Journal of Computer Security},
   note = {To appear},
   publisher = {{IOS} Press},
   title = {Symbolic bisimulation for the applied pi~calculus},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ DKR-jcs09.pdf},
   year = {2009}
}



@inproceedings{JSU,
  author    = {J. Borgstr{\"o}m and
               S. Briais and
               U. Nestmann},
  title     = {Symbolic Bisimulation in the Spi Calculus},
  booktitle = {CONCUR},
  year      = {2004},
  pages     = {161-176},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3170{\&}spage=161},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{JB,
 author = {Borgstr\"{o}m, J.},
 title = {A Complete Symbolic Bisimilarity for an Extended Spi Calculus},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {242},
 number = {3},
 year = {2009}
 }



 @inproceedings{MB,
 author = {Baudet, M.},
 title = {Deciding security of protocols against off-line guessing attacks},
 booktitle = {CCS '05: Proceedings of the 12th ACM conference on Computer and communications security},
 year = {2005},
 isbn = {1-59593-226-7},
 pages = {16--25},
 doi = {http://doi.acm.org/10.1145/1102120.1102125},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@inproceedings{BMC,
  author    = {B. Blanchet and
               M. Abadi and
               C. Fournet},
  title     = {Automated Verification of Selected Equivalences for Security
               Protocols},
  booktitle = {LICS},
  year      = {2005},
  pages     = {331-340},
  ee        = {http://dx.doi.org/10.1109/LICS.2005.8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{MBMGB,
  author    = {M. Boreale and
               M. Buscemi},
  title     = {A method for symbolic analysis of security protocols},
  journal   = {Theor. Comput. Sci.},
  volume    = {338},
  number    = {1-3},
  year      = {2005},
  pages     = {393-425},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2005.03.044},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{MJJPBVJB,
 author = {Johansson, M. and Parrow, J. and Victor, B. and Bengtson, J.},
 title = {Extended pi-Calculi},
 booktitle = {ICALP '08: Proceedings of the 35th international colloquium on Automata, Languages and Programming, Part II},
 year = {2008},
 isbn = {978-3-540-70582-6},
 pages = {87--98},
 location = {Reykjavik, Iceland},
 doi = {http://dx.doi.org/10.1007/978-3-540-70583-3_8},
 publisher = {Springer-Verlag},
 }

 @inproceedings{JBMJJPBV,
 author = {Bengtson, J. and Johansson, M. and Parrow, J. and Victor, B.},
 title = {Psi-calculi: Mobile Processes, Nominal Data, and Logic},
 booktitle = {LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science},
 year = {2009},
 isbn = {978-0-7695-3746-7},
 pages = {39--48},
 doi = {http://dx.doi.org/10.1109/LICS.2009.20},
 }

@article{MAVC,
  author    = {M. Abadi and
               V. Cortier},
  title     = {Deciding knowledge in security protocols under equational
               theories},
  journal   = {Theor. Comput. Sci.},
  volume    = {367},
  number    = {1-2},
  year      = {2006},
  pages     = {2-32},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2006.08.032},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{CD-csf09,
   address = {Port Jefferson, NY, USA},
   author = {Cortier, V. and Delaune, S.},
   booktitle = {{P}roceedings of the 22nd {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'09)},
   DOI = {10.1109/CSF.2009.9},
   month = jul,
   pages = {266-276},
   publisher = {{IEEE} Computer Society Press},
   title = {A method for proving observational equivalence},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf},
   year = {2009},
}

@inproceedings{CLHCV08,
 author = {Comon-Lundh, H. and Cortier, V.},
 title = {Computational soundness of observational equivalence},
 booktitle = {CCS '08: Proceedings of the 15th ACM conference on Computer and communications security},
 year = {2008},
 isbn = {978-1-59593-810-7},
 pages = {109--118},
 location = {Alexandria, Virginia, USA},
 doi = {http://doi.acm.org/10.1145/1455770.1455786},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{MACF04PA,
 author = {Abadi, M. and Fournet, C.},
 title = {Private authentication},
 journal = {Theor. Comput. Sci.},
 volume = {322},
 number = {3},
 year = {2004},
 issn = {0304-3975},
 pages = {427--476},
 doi = {http://dx.doi.org/10.1016/j.tcs.2003.12.023},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
 }

 @ARTICLE{BAFJLAP07,
  AUTHOR = {B. Blanchet and M. Abadi and C. Fournet},
  TITLE = {Automated Verification of Selected Equivalences for Security Protocols},
  JOURNAL = {Journal of Logic and Algebraic Programming},
  YEAR = 2008,
  VOLUME = 75,
  NUMBER = 1,
  PAGES = {3--51},
  MONTH = FEB # {--} # MAR
}


@inproceedings{CCD-secco09,
   address = {Bologna, Italy},
   author = {Cheval, V. and Comon-Lundh, H. and Delaune, S.},
   booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oordination {M}odels, {L}anguages and {S}ystems ({SecCo}'09)},
   editor = {Boreale, Michele and Kremer, Steve},
   month = oct,
   title = {A decision procedure for proving observational equivalence},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf},
   year = {2009},
}

@inproceedings{MBDRN,
 author = {Boreale, M and Nicola, R, De},
 title = {A Symbolic Semantics for the pi-calculus (Extended Abstract)},
 booktitle = {CONCUR '94: Proceedings of the Concurrency Theory},
 year = {1994},
 isbn = {3-540-58329-7},
 pages = {299--314},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


 @inproceedings{MH89,
 author = {Hennessy, M},
 title = {A Proof System for Communicating Processes with Value-passing (Extended Abstract)},
 booktitle = {Proceedings of the Ninth Conference on Foundations of Software Technology and Theoretical Computer Science},
 year = {1989},
 isbn = {3-540-52048-1},
 pages = {325--339},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


@ARTICLE{JPDS94,
    author = {J. Parrow and D. Sangiorgi},
    title = {Algebraic Theories for Name-Passing Calculi},
    journal = {Information and Computation},
    year = {1994},
    volume = {120},
    pages = {174--197}
}