Modeling and Analysis of Security Protocols Using Role Based Specifications and Petri Nets

Abstract. In this paper, we introduce a framework composed of a syntax and its compositional Petri net semantics, for the specification and verification of properties (like authentication) of security protocols. The protocol agents (e.g., an initiator, a responder, a server, a trusted third party, . . . ) are formalized as roles, each of them having a predefined behavior depending on their global and also local knowledge (including for instance public, private and shared keys), and may interact in a potentially hostile environment. The main characteristics of our framework, is that it makes explicit, structured and formal, the usually implicit information necessary to analyse the protocol, for instance the public and private context of execution. The roles and the environment are expressed using SPL processes and compositionally translated into high-level Petri nets, while the context specifying the global and local knowledge of the participants in the protocol is used to generate the ...

• Type: Conference
• Year: 2008
• Where: APN
• Authors: Roland Bouroulet, Raymond R. Devillers, Hanna Klaudel, Elisabeth Pelz, Franck Pommereau
• Keywords: APN 2008, Artificial Intelligence, Petri Net Semantics, Petri Nets, Security Protocols