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 (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 edit

^ 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.
^ 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

This cryptography-related article is a stub. You can help Wikipedia by expanding it.