iUML-B model of VLAN system

Dataset support the paper 'Analysing security protocols using refinement in iUML-B', presented at 9th NASA Formal Methods Symposium, 16-18 May 2017.

Formal specification of a VLAN tagging system illustrating the well-known security flaw of these systems, double-tagging. We use iUML-B class diagrams which provide a diagrammatic representation of the Event-B formalism. We specify the security principle that packets should only belong to nodes of a VLAN which they are intended for and prove that the property is maintained. We then refine the model to introduce the usual packet tagging mechanism that is supposed to ensure the security principle. A double tagging attack cannot be proven to satisfy the glueing invariant.
A second version of the model is provided that excludes the Native LAN from being used as a VLAN which is the usual recommendation to prevent double-tagging attacks. This version is fully proven to be secure.