protocol composition logic

{{Short description|Proof method for the security of cryptographic protocols}}

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).{{Cite journal |last1=Datta |first1=Anupam |last2=Derek |first2=Ante |last3=Mitchell |first3=John C. |last4=Roy |first4=Arnab |date=April 2007 |title=Protocol Composition Logic (PCL) |url=https://doi.org/10.1016/j.entcs.2007.02.012 |journal=Electronic Notes in Theoretical Computer Science |volume=172 |pages=311–358 |doi=10.1016/j.entcs.2007.02.012 |issn=1571-0661|doi-access=free }}

Some problems with the logic have been found, implying that some currently claimed results cannot be proven within the logic.{{Citation|first=Cas|last=Cremers|title=Proceedings of the 2008 ACM symposium on Information, computer and communications security - ASIACCS '08|year=2008|chapter=On the Protocol Composition Logic PCL|page=66|doi=10.1145/1368310.1368324|arxiv=0709.1080|isbn=9781595939791|s2cid=7618247}}