An executable model for security protocol JFKr
David L. Rager · 2009
JFKr is a security protocol that establishes a shared encryption key between two participants. This paper briefly describes the different components of JFKr and the security property each component is intended to provide. It then describes an executable model, interleaving pieces of code to help the reader understand how the model represents the protocol specification. Finally, it presents some theorems about the model.