Logic-Based Formal Analysis of Cryptographic Protocols

We develop informal principals and formal rules to verify security properties in cryptographic protocols. These principals are based on the notions of message origination, message freshness, ideal cryptography, message count, etcetera. Our focus is the authentication and the secrecy properties. We offer a different perspective for analysis in which participants try to achieve guarantees from their own run of the protocol by investigating the set of messages they send and receive instead of by looking at several attack strategies of an illegitimate participant. We provide a computational model and present formal semantics of our proposed logical framework according to which our formulas are sound.