A Formalization of Credit and Responsibility Within the GNDC Schema

We formally define a notion of credit and responsibility within the Generalized Non Deducibility on Compositions framework. We investigate the validity of our definitions through some examples discussed in the literature. Key words: Formal methods, authentication, Generalized Non Deducibility on Composition 1 Overview Formal methods and tools have been successfully applied for the analysis of network security. The protocol under investigation is described in a given language, then a formal specification of the security property to be analyzed is defined. Whether or not the security property is fulfilled is investigated by formally analyzing the protocol in a hostile environment, i.e., considering the presence of an adversary running in parallel with the honest participants. Both the property's formal specification and its informal definition are crucial steps for the analysis. Indeed, even a common notion as authentication is usually considered a slippery security property (see [...

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Roberto Gorrieri, Fabio Martinelli, Marinella Petrocchi
• Keywords: ENTCS 2006, Generalized Non Deducibility, Non Deducibility, Security Property