Operational Semantics and Verification of Security Protocols

摘要: Security protocols are widely used to ensure secure communications over insecure networks, such as the internet or airwaves. These use strong cryptography prevent intruders from reading modifying messages. However, using is not enough their correctness. Combined with typical small size, which suggests that one could easily assess correctness, this often results in incorrectly designed protocols. The authors present a methodology for formally describing security and environment. This includes model protocols, execution model, intruder model. models extended number of well-defined properties, capture notions correct secrecy data. can be prove satisfy these properties. Based on they have developed tool set called Scyther automatically find attacks In case studies show application well effectiveness analysis tool. methodologys mathematical basis, separation concerns accompanying make it ideally suited both researchers graduate students information formal methods advanced professionals designing critical