Analysing the BKE-security Protocol with μCRL

The μCRL language and its corresponding tool set form a powerful methodology for the verification of distributed systems. We demonstrate its use by applying it to the well-known Bilateral Key Exchange security protocol.