Thumbnail
Access Restriction
Open

Author Long, Benjamin W. ♦ Fidge, Colin J. ♦ Carrington, David A.
Source CiteSeerX
Content type Text
Publisher Springer-Verlag
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Presentation Layer ♦ Implementation-dependent Attack ♦ Type Flaw Attack ♦ Application Layer Specification ♦ Little Detail ♦ Message Data Structure ♦ Security Protocol ♦ Minimal Requirement ♦ Formal Verification ♦ Interpretation Protocol ♦ Avispa Model ♦ Application Layer ♦ Group Domain ♦ Corresponding Presentation Layer Specification
Description Security protocols are often specified at the application layer; however, application layer specifications give little detail regarding message data structures at the presentation layer upon which some implementation-dependent attacks rely. In this paper we present an approach to verifying security protocols in which both the application and presentation layers are modelled. Using the Group Domain of Interpretation protocol as an example, our application layer specification of the protocol is used as input to the AVISPA model checking tool for analysis. Two type flaw attacks are found via model checking which are then verified against the corresponding presentation layer specification, thus identifying the minimal requirements to prevent the attacks. 1
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2005-01-01
Publisher Institution in ‘4th International Conference of B and Z Users, ZB 2005