Entry Paulson:1999:IAI from tissec.bib

Last update: Sun Oct 15 02:58:48 MDT 2017                Valid HTML 3.2!

Index sections

Top | Symbols | Numbers | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Paulson:1999:IAI,
  author =       "Lawrence C. Paulson",
  title =        "Inductive analysis of the {Internet} protocol {TLS}",
  journal =      j-TISSEC,
  volume =       "2",
  number =       "3",
  pages =        "332--351",
  month =        aug,
  year =         "1999",
  CODEN =        "ATISBQ",
  ISSN =         "1094-9224 (print), 1557-7406 (electronic)",
  ISSN-L =       "1094-9224",
  bibdate =      "Thu Oct 26 11:39:38 MDT 2000",
  bibsource =    "http://www.acm.org/tissec/contents/v2no3.html;
                 http://www.math.utah.edu/pub/tex/bib/tissec.bib",
  URL =          "http://www.acm.org/pubs/citations/journals/tissec/1999-2-3/p332-paulson/",
  abstract =     "Internet browsers use security protocols to protect
                 sensitive messages. An inductive analysis of TLS (a
                 descendant of SSL 3.0) has been performed using the
                 theorem prover Isabelle. Proofs are based on
                 higher-order logic and make no assumptions concerning
                 beliefs of finiteness. All the obvious security goals
                 can be proved; session resumption appears to be secure
                 even if old session keys are compromised. The proofs
                 suggest minor changes to simplify the analysis.
                 \par

                 TLS, even at an abstract level, is much more
                 complicated than most protocols verified by
                 researchers. Session keys are negotiated rather than
                 distributed, and the protocol has many optional parts.
                 Netherless, the resources needed to verify TLS are
                 modest: six man-weeks of effort and three minutes of
                 processor time.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Information and System Security",
  generalterms = "Security; Verification",
  journal-URL =  "http://portal.acm.org/browse_dl.cfm?idx=J789",
  keywords =     "authentication; inductive method; Isabelle; proof
                 tools; TLS",
  subject =      "Theory of Computation --- Logics and Meanings of
                 Programs --- Specifying and Verifying and Reasoning
                 about Programs (F.3.1): {\bf Mechanical verification};
                 Computer Systems Organization ---
                 Computer-Communication Networks --- Network Protocols
                 (C.2.2): {\bf Protocol verification}",
}

Related entries