Protocol composition logic

Last updated

Protocol Composition Logic is a formal method that can be used for proving security properties of cryptographic protocols that use symmetric-key and public-key cryptography. PCL is designed around a process calculus with actions for various possible protocol steps (e.g. generating random numbers, performing encryption, decryption and digital signature operations as well as sending and receiving messages). [1]

Some problems with the logic have been found, implying that some currently claimed results cannot be proven within the logic. [2]

References

  1. Datta, Anupam; Derek, Ante; Mitchell, John C.; Roy, Arnab (April 2007). "Protocol Composition Logic (PCL)". Electronic Notes in Theoretical Computer Science. 172: 311–358. doi: 10.1016/j.entcs.2007.02.012 . ISSN   1571-0661.
  2. Cremers, Cas (2008), "On the Protocol Composition Logic PCL", Proceedings of the 2008 ACM symposium on Information, computer and communications security - ASIACCS '08, p. 66, arXiv: 0709.1080 , doi:10.1145/1368310.1368324, ISBN   9781595939791, S2CID   7618247