Protocol Analysis Tutorial I

Adventures in CryptographicProtocol AnalysisJonathan K. MillenThe MITRE CorporationACM CCS, October 2010The author’s affiliation with The MITRE Corporation is provided for identification purposes only, and is not intended to convey or imply MITRE’s concurrence with, or support for, the positions, opinions orviewpoints expressed by the author. 1Protocol Security Analysis Protocol security analysis has a long and diverse history Rather than a survey, let's look at why it was enjoyable to study this kind of problem, and some unconventional approaches to it Protocol security analysis is like a logical puzzle...– We can use this to understand the power, the demands, and the limits of protocol security analysis2Example: Wolf, Goat and Cabbage Also called Fox, Goose, and Corn; or Fox, Chicken, Grain There's a river A farmer is on one bank with the three possessions and a boat The boat is only big enough for the farmer and one possession The wolf should not be left alone with the goat, or the goat with the cabbage How can the farmer get all his possessions across the river?3The Answer: a Protocol?LEFT BANK RIGHT BANKfwgc fg f: farmerw: wolfwc f fgg: goatfcfwc gc: cabbagew fg fgcfgw fw cg f fwcfg fg wcfwgc4Protocol Analyzers Can Solve This Protocol analysis includes the ability to solve state reachability problems How can this be illustrated?– Encode the WGC problem as a protocol– Encode the constraints and the goal, but not ...