的象征性的协议分析.ppt

Symbolic Protocol Analysis Vitaly Shmatikov Overview Strand space model Protocol analysis with unbounded attacker Parametric strands Symbolic attack traces Protocol analysis via constraint solving SRI constraint solver Protocol Analysis Techniques Obtaining a Finite Model Two sources of infinite behavior Multiple protocol sessions, multiple participants Message space or data space may be infinite Finite approximation Assume finite sessions Example: 2 clients, 2 servers Assume finite message space Represent random numbers by r1, r2, r3, … Do not allow encrypt(encrypt(encrypt(…))) Decidable Protocol Analysis Eliminate sources of undecidability Bound the number of protocol sessions Artificial bound, no guarantee of completeness Bound structural size of messages by lazy instantiation of variables Loops are simulated by multiple sessions Secrecy and authentication are NP-complete if the number of protocol instances is bounded [Rusinowitch, Turuani ’01] Search for solutions can be fully automated Several tools; we’ll talk about SRI constraint solver Strand Space Model A strand is a representation of a protocol “role” Sequence of “nodes” Describes what a participant playing one side of the protocol must do according to protocol specification A node is an observable action “+” node: sending a message “-” node: receiving a message Messages are ground terms Standard formalization of cryptographic operations: pairing, encryption, one-way functions, … Participant Roles in NSPK NSPK in Strand Space Model Each primitive capability of the attacker is a “penetrator” strand Same set of attacker strands for every protocol Bundles A bundle combines strands into a partial ordering Nodes are ordered by internal strand order “Send message” nodes of one strand are matched up with “receive message” nodes of another strand Infinitely many possible bundles for any given set of strands No bound on the number of times any given attacker strand may be used Each bundle corresponds to