Entry Bhargavan:2012:VCI 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{Bhargavan:2012:VCI,
  author =       "Karthikeyan Bhargavan and C{\'e}dric Fournet and
                 Ricardo Corin and Eugen Zalinescu",
  title =        "Verified Cryptographic Implementations for {TLS}",
  journal =      j-TISSEC,
  volume =       "15",
  number =       "1",
  pages =        "3:1--3:??",
  month =        mar,
  year =         "2012",
  CODEN =        "ATISBQ",
  DOI =          "https://doi.org/10.1145/2133375.2133378",
  ISSN =         "1094-9224 (print), 1557-7406 (electronic)",
  ISSN-L =       "1094-9224",
  bibdate =      "Sat Mar 24 09:45:43 MDT 2012",
  bibsource =    "http://portal.acm.org/;
                 http://www.math.utah.edu/pub/tex/bib/tissec.bib",
  abstract =     "We narrow the gap between concrete implementations of
                 cryptographic protocols and their verified models. We
                 develop and verify a small functional implementation of
                 the Transport Layer Security protocol (TLS 1.0). We
                 make use of the same executable code for
                 interoperability testing against mainstream
                 implementations for automated symbolic cryptographic
                 verification and automated computational cryptographic
                 verification. We rely on a combination of recent tools
                 and also develop a new tool for extracting
                 computational models from executable code. We obtain
                 strong security guarantees for TLS as used in typical
                 deployments.",
  acknowledgement = ack-nhfb,
  articleno =    "3",
  fjournal =     "ACM Transactions on Information and System Security",
  journal-URL =  "http://portal.acm.org/browse_dl.cfm?idx=J789",
}

Related entries