Logic of Events for Proving Security Properties of Protocols

摘要

Formal methods are vital for ensuring the security and reliability of the network systems. We propose a promising method to check security properties of cryptographic protocols using logic of events theory. The logic is designed around a message automaton with actions for possible protocol steps including generating new nonces, sending and receiving messages, and performing encryption, decryption and digital signature verification actions. We figure out types for the keys, nonces, and messages of the protocol and present novel proof rules and mechanism for protocol actions, temporal reasoning, and a specialized form of invariance rule. It puts no bound on the size of the principal and requires no state space enumeration. Our main theorem guarantees that any well-typed protocol is robustly safe under attack while reasoning only about the actions of honest principals in the protocol.