Team for Research in
Ubiquitous Secure Technology

Citation
Anupam Datta, Ante Derek, John C. Mitchell, Arnab Roy. "Protocol Composition Logic (PCL)". Electronic Notes in Theoretical Computer Science, 172:311-358, 2007.

Abstract
Protocol Composition Logic (PCL) is a logic for proving security properties of network protocols that use public and symmetric key cryptography. The logic is designed around a process calculus with actions for possible protocol steps including generating new random numbers, sending and receiving messages, and performing decryption and digital signature verication actions. The proof system consists of axioms about individual protocol actions and inference rules that yield assertions about protocols composed of multiple steps. Although assertions are written only using the steps of the protocol, the logic is sound in a strong sense: each provable assertion involving a sequence of actions holds in any protocol run containing the given actions and arbitrary additional actions by a malicious adversary. This approach lets us prove security properties of protocols under attack while reasoning only about the actions of honest parties in the protocol. PCL supports compositional reasoning about complex security protocols and has been applied to a number of industry standards including SSL/TLS, IEEE 802.11i and Kerberos V5.

Electronic downloads

• http://www.andrew.cmu.edu/user/danupam/ddmr-pcl06.pdf

• HTML

  Anupam Datta, Ante Derek, John C. Mitchell, Arnab Roy. <a
  href="http://www.truststc.org/pubs/417.html"
  >Protocol Composition Logic (PCL)</a>,
  <i>Electronic Notes in Theoretical Computer
  Science</i>, 172:311-358,  2007.

• Plain text

  Anupam Datta, Ante Derek, John C. Mitchell, Arnab Roy.
  "Protocol Composition Logic (PCL)".
  <i>Electronic Notes in Theoretical Computer
  Science</i>, 172:311-358,  2007.

• BibTeX

  @article{DattaDerekMitchellRoy07_ProtocolCompositionLogicPCL,
      author = {Anupam Datta and Ante Derek and John C. Mitchell
                and Arnab Roy},
      title = {Protocol Composition Logic (PCL)},
      journal = {Electronic Notes in Theoretical Computer Science},
      volume = {172},
      pages = {311-358},
      year = {2007},
      abstract = {Protocol Composition Logic (PCL) is a logic for
                proving security properties of network protocols
                that use public and symmetric key cryptography.
                The logic is designed around a process calculus
                with actions for possible protocol steps including
                generating new random numbers, sending and
                receiving messages, and performing decryption and
                digital signature verication actions. The proof
                system consists of axioms about individual
                protocol actions and inference rules that yield
                assertions about protocols composed of multiple
                steps. Although assertions are written only using
                the steps of the protocol, the logic is sound in a
                strong sense: each provable assertion involving a
                sequence of actions holds in any protocol run
                containing the given actions and arbitrary
                additional actions by a malicious adversary. This
                approach lets us prove security properties of
                protocols under attack while reasoning only about
                the actions of honest parties in the protocol. PCL
                supports compositional reasoning about complex
                security protocols and has been applied to a
                number of industry standards including SSL/TLS,
                IEEE 802.11i and Kerberos V5.},
      URL = {http://www.truststc.org/pubs/417.html}
  }
  

Posted by Anupam Datta on 25 Jul 2008.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.