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

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