Most approaches to formal verification of authentication protocols assume encryption to have the property that parts of a message cannot be extracted without knowledge of the encrypting key. In practice, implementations are not perfect in this sense and the correctness of a protocol may depend on the algebraic properties of encryption.
One example is the use of binary exclusive or to encrypt session keys in key establishment protocols. This talk will cover the use of the Isabelle proof tool to model the properties of exclusive or and a protocol that uses it. We also discuss proofs of session key secrecy properties for the protocol.