Proving Authentication Property of Modified Needham-Schroeder Protocol with Logic of Events

DOI

10.2991/cisia-15.2015.103How to use a DOI?

Keywords

formal method; logic of events; authentication of cryptographic protocols

Abstract

Security protocols are the foundation of modern secure networked systems. Proving security properties of cryptographic protocols is a challenge problem. Model checking has proven useful for finding certain classes of errors in network security protocols, but it is based on bounded model or constraint solving, and provides little insight into why a protocol is correct. While theorem proving puts no bound on the size of the principal and requires no state space enumeration. We present novel proof rules and mechanisms for protocol actions and temporal reasoning to check security properties of cryptographic protocols using logic of events theory. The logic is an event-ordering which extended by seven special event classes New, Send, Receive, Sign, Verify, Encrypt, and Decrypt, and axioms AxiomK, AxiomR, AxiomV, AxiomD, AxiomS, AxiomF, Disjointness axioms and Flow relation. As a case study, our method is illustrated by showing the proof of the modified Needham-Schroeder protocol. Result shows the logic of events is feasible and general for analyzing cryptographic protocols.

Copyright

© 2015, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - M.H Xiao
AU  - C.Y Deng
AU  - C.L Ma
AU  - K. Zhu
AU  - D.L Cheng
PY  - 2015/06
DA  - 2015/06
TI  - Proving Authentication Property of Modified Needham-Schroeder Protocol with Logic of Events
BT  - Proceedings of the International Conference on Computer Information Systems and Industrial Applications
PB  - Atlantis Press
SP  - 379
EP  - 383
SN  - 2352-538X
UR  - https://doi.org/10.2991/cisia-15.2015.103
DO  - 10.2991/cisia-15.2015.103
ID  - Xiao2015/06
ER  -