Article · Wikipedia archive · Last revised May 28, 2026

Protocol composition logic

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.

Last revised
May 28, 2026
Read time
≈ 1 min
Length
135 w
Citations
2
Source
Wikipedia ↗

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

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