In this talk we present PCL - a logic for proving security properties of network protocols. Two central results for this logic are a "composition theorem" and a "computational soundness theorem". The composition theorem allows proofs of complex protocols to be built up from proofs of their constituent sub-protocols. It is formulated and proved by adapting ideas from the assume-guarantee paradigm for reasoning about distributed systems. The computational soundness theorem guarantees that, for a class of security properties and protocols, axiomatic proofs in PCL carry the same meaning as hand-proofs done by cryptographers. The soundness proof uses standard proof techniques from cryptography, in particular, complexity-theoretic reductions. PCL has been successfully applied to a number of internet, wireless and mobile network security protocols developed by the IEEE and IETF Working Groups, in several cases identifying serious security vulnerabilities.