Formalizing and Analyzing Security Ceremonies with Heterogeneous Devices in ANP and PDL

Part 4: VerificationInternational audienceSecurity ceremonies extend cryptographic protocols with models of human users to allow us to take human behaviors into account when reasoning about security. Actor-network procedures (ANPs) are a well-known formal model of security ceremonies, and procedure derivation logic (PDL) allows us to reason logically about ANPs. In a security ceremony, different nodes may have different capabilities: computers can encrypt and decrypt messages, whereas humans cannot; a biometric device can capture biometric information, whereas a random number generator used in e-banking cannot; and so on. Furthermore, even if a node has the decryption capability, it must also know the encryption key to decrypt a message. ANPs do not support explicitly specifying node capabilities. In this paper, we extend ANPs to deal with heterogeneous devices by explicitly specifying the nodes’ capabilities. We also modify PDL to take into account the knowledge of participants at different points in time. All this allows us to reason about secrecy and authentication in ceremonies with different kinds of devices and human users