Analysis of Object-Specific Authorization Protocol (OSAP)udusing coloured Petri nets

摘要

The use of Trusted Platform Module (TPM) is be-udcoming increasingly popular in many security sys-udtems. To access objects protected by TPM (suchudas cryptographic keys), several cryptographic proto-udcols, such as the Object Specific Authorization Pro-udtocol (OSAP), can be used. Given the sensitivity andudthe importance of those objects protected by TPM,udthe security of this protocol is vital. Formal meth-udods allow a precise and complete analysis of crypto-udgraphic protocols such that their security propertiesudcan be asserted with high assurance. Unfortunately,udformal verification of these protocols are limited, de-udspite the abundance of formal tools that one can use.udIn this paper, we demonstrate the use of ColouredudPetri Nets (CPN) - a type of formal technique, toudformally model the OSAP. Using this model, we thenudverify the authentication property of this protocol us-uding the state space analysis technique. The results ofudanalysis demonstrates that as reported by Chen andudRyan the authentication property of OSAP can beudviolated.