Cryptographic Protocol Verification
Communication systems and protocols are often standardized to enable interoperability. Cryptographic protocols for key establishment, channel encryption and other tasks are part of these standards. Large and complex standards, such as those for mobile networks and internet protocols, include implicit requirements and frequently have vague security assumptions and goals. In this project we extract and formalize cryptographic protocols from 5G and IoT standards, define appropriate adversary models and security properties, and analyze the protocols in the symbolic model (using the Tamarin prover) as well as in the computational model (using traditional pen-and-paper proofs).
