A formal model of security controls implementing the IPsec and IKE protocols

Starting a process of standardization of security protocols can be considered as one of the solutions to meet the growing needs of corporate network systems to integrate security functions to create more secure systems.The lack of standard interfaces to control and monitor the behaviour of NSFs makes it virtually impossible for security service providers to automate service offerings that utilize different security functions from multiple vendors.The NSF developed by different vendors have different interfaces for their configuration and management because there is no industry standard of interfaces for NSF.This heterogeneity introduces complexity to managing the NSFs of multiple suppliers, resulting in increased management costs.Standardization is essential to successfully implement NSF offered by various vendors.Recently, some standardization activities have started a development process such as the IETF I2NSF working group to meet these needs.This working group develops a series of information models and standard data models that are the key to building the standard interfaces of the I2NSF architecture.Based on the models defined by I2NSF, this thesis has as its starting point the expansion of the IM developed by another student.The main aim is to model the configurable aspects of a security device so that automatic configuration tools or tools that think about policies are able to understand how to use, avoiding human intervention. I worked on modelling the IPsec security protocol.It was created a model of the capabilities of devices implementing level 3 channel security using IPsec and IKE.An abstract representation of the security capabilities has been created in a data model to manage and manipulate every potential security functionality.IPsec is a protocol that can be implemented by manual or automatic key exchange.To make the DM heterogeneous, a peculiar and profound moderation was required within these devices that implement IPsec.To express the security policies, the event-condition-action paradigm is used for a correct subdivision of the security capabilities of protocols.The model is created using the UML graphic representation and some design patterns to optimize the expressive features of the model exported in xmi format.Then the policies of a device are saved in abstract format, it was necessary to implement a tool for the conversion from xmi to XSD.This format was chosen because the XML language is easily compatible.Subsequently, a catalogue was created that contained all the necessary security capabilities and the NSF instanced.Each NSF contains a reference to the security capability that it can exploit.Starting from the instances in the catalogue, there was the generation of the protocol language in abstract format.A previously developed tool was used and then adapted to our situation, in which the name of the NSF for which we want the language is specified and in output we will have a new xsd file containing all the schemes.Since the devices require configurations in their proprietary language, it was necessary to carry out a translation mechanism from the abstract language to the specific one of the device itself.A translator is implemented and it takes in input rules written in abstract language according to the previous scheme and referring to the NSF and its specific language.In the translation phase, *Details classes present in the catalogue are used, useful for passing from the abstract to the final language.