# HG changeset patch
# User paulson
# Date 986911130 -7200
# Node ID 64d0bcccb03a31123bc376e2e1744d0ccdbe8e2c
# Parent  3d9d25a3375bc7d7c261b239cf863d46c10054bd
security protocol refs

diff -r 3d9d25a3375b -r 64d0bcccb03a doc-src/manual.bib
--- a/doc-src/manual.bib	Mon Apr 09 14:49:51 2001 +0200
+++ b/doc-src/manual.bib	Tue Apr 10 15:58:50 2001 +0200
@@ -27,7 +27,9 @@
 @string{JLP="Journal of Logic Programming"}
 @string{JSC="Journal of Symbolic Computation"}
 @string{JSL="Journal of Symbolic Logic"}
+@string{PROYAL="Proceedings of the Royal Society of London"}
 @string{SIGPLAN="{SIGPLAN} Notices"}
+@string{TISSEC="ACM Transactions on Information and System Security"}
 
 %conferences
 @string{CADE="International Conference on Automated Deduction"}
@@ -181,6 +183,14 @@
   pages		= {381-392},
   year		= 1972}
 
+@Article{ban89,
+  author	= {M. Burrows and M. Abadi and R. M. Needham},
+  title		= {A Logic of Authentication},
+  journal	= PROYAL,
+  year		= 1989,
+  volume	= 426,
+  pages		= {233-271}}
+
 %C
 
 @TechReport{camilleri92,
@@ -485,6 +495,21 @@
   publisher	= NH,
   year		= 1980}
 
+%L
+
+@InProceedings{lowe-fdr,
+  author	= {Gavin Lowe},
+  title		= {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
+		  Protocol using {CSP} and {FDR}},
+  booktitle = 	 {Tools and Algorithms for the Construction and Analysis 
+                  of Systems:  second international workshop, TACAS '96},
+  editor =	 {T. Margaria and B. Steffen},
+  series =	 {LNCS 1055},
+  year =	 1996,
+  publisher =	 {Springer},
+  pages		= {147-166}}
+
+
 %M
 
 @Article{mw81,
@@ -592,6 +617,17 @@
   pages		= {331-345},
   year		= 1996}
 
+@Article{needham-schroeder,
+  author =       "Roger M. Needham and Michael D. Schroeder",
+  title =        "Using Encryption for Authentication in Large Networks
+                 of Computers",
+  journal =      cacm,
+  volume =       21,
+  number =       12,
+  pages =        "993-999",
+  month =        dec,
+  year =         1978}
+
 @inproceedings{nipkow-W,
   author	= {Wolfgang Naraschewski and Tobias Nipkow},
   title		= {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
@@ -872,6 +908,17 @@
   volume	= 6,
   pages		= {85-128}}
 
+@Article{paulson-tls,
+  author = 	 {Lawrence C. Paulson},
+  title = 	 {Inductive Analysis of the {Internet} Protocol {TLS}},
+  journal = 	 TISSEC,
+  month =        aug,
+  year = 	 1999,
+  volume	= 2,
+  number        = 3,
+  pages		= {332-351}}
+
+
 @article{pelletier86,
   author	= {F. J. Pelletier},
   title		= {Seventy-five Problems for Testing Automatic Theorem