Team for Research in
Ubiquitous Secure Technology

Citation
John C. Mitchell. "A Symbolic Logic with Exact Bounds for Cryptographic Protocols". 6642, SpringerLink, 2011.

Abstract
This invited talk will describe a formal logic for reasoning about security properties of network protocols with proof rules indicating exact security bounds that could be used to choose key lengths or other concrete security parameters. The soundness proof for this logic, a variant of previous versions of Protocol Composition Logic (PCL), shows that derivable properties are guaranteed in a standard cryptographic model of protocol execution and resource-bounded attack.We will discuss the general system and present example axioms for digital signatures and random nonces, with concrete security properties based on concrete security of signature schemes and pseudorandom number generators (PRG). The quantitative formal logic supports first-order reasoning and reasoning about protocol invariants, taking exact security bounds into account. Proofs constructed in this logic also provide conventional asymptotic security guarantees because of the way that exact bounds accumulate in proofs. As an illustrative example producing exact bounds, we use the formal logic to prove an authentication property with exact bounds of a signature-based challenge-response protocol.

Electronic downloads

• http://www.springerlink.com/content/0255520024659905/

• HTML

  John C. Mitchell. <a
  href="http://www.truststc.org/pubs/895.html"
  ><i>A Symbolic Logic with Exact Bounds for
  Cryptographic Protocols</i></a>, 6642,
  SpringerLink, 2011.

• Plain text

  John C. Mitchell. "A Symbolic Logic with Exact Bounds
  for Cryptographic Protocols". 6642, SpringerLink, 2011.

• BibTeX

  @inbook{Mitchell11_SymbolicLogicWithExactBoundsForCryptographicProtocols,
      author = {John C. Mitchell},
      title = {A Symbolic Logic with Exact Bounds for
                Cryptographic Protocols},
      volume = {6642},
      publisher = {SpringerLink},
      year = {2011},
      abstract = {This invited talk will describe a formal logic for
                reasoning about security properties of network
                protocols with proof rules indicating exact
                security bounds that could be used to choose key
                lengths or other concrete security parameters. The
                soundness proof for this logic, a variant of
                previous versions of Protocol Composition Logic
                (PCL), shows that derivable properties are
                guaranteed in a standard cryptographic model of
                protocol execution and resource-bounded attack.We
                will discuss the general system and present
                example axioms for digital signatures and random
                nonces, with concrete security properties based on
                concrete security of signature schemes and
                pseudorandom number generators (PRG). The
                quantitative formal logic supports first-order
                reasoning and reasoning about protocol invariants,
                taking exact security bounds into account. Proofs
                constructed in this logic also provide
                conventional asymptotic security guarantees
                because of the way that exact bounds accumulate in
                proofs. As an illustrative example producing exact
                bounds, we use the formal logic to prove an
                authentication property with exact bounds of a
                signature-based challenge-response protocol. },
      URL = {http://www.truststc.org/pubs/895.html}
  }
  

Posted by Mary Stewart on 4 Apr 2012.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.