Probabilistic Model CheckingOverviewCrowds SystemSlide 4Discrete-Time Markov ChainsMarkov Chain: Simple ExamplePRISMPRISM SyntaxModeling Crowds with PRISMPRISM: Path Construction in CrowdsPRISM: Intruder ModelPowerPoint PresentationSlide 13PCTL: State FormulasPCTL: Path FormulasPCTL: Probabilistic State FormulasIntruder Model ReduxNegation of Probable InnocenceAnalyzing Multiple Paths with PRISMSender Detection (Multiple Paths)Attacker’s ConfidenceProbabilistic Model CheckingCS 395TOverviewCrowds reduxProbabilistic model checking•PRISM model checker•PCTL logic•Analyzing Crowds with PRISMProbabilistic contract signing •Rabin’s beacon protocol•Ben-Or, Goldreich, Rivest, Micali protocol•Analyzing probabilistic contract signing protocols with PRISMCrowds SystemCC4C1C2CCCC3C0senderrecipientCCCCpf1-pfRouters form a random path when establishing connection•In onion routing, random path is chosen in advance by senderAfter receiving a message, honest router flips a biased coin•With probability Pf randomly selects next router and forwards msg•With probability 1-Pf sends directly to the recipient[Reiter,Rubin ‘98]Probabilistic Model Checking......0.30.50.2Participants are finite-state machines•Same as MurState transitions are probabilistic•Transitions in Mur are nondeterministicStandard intruder model•Same as Mur: model cryptography with abstract data typesMur question:•Is bad state reachable?Probabilistic model checking question:•What’s the probability of reaching bad state?“bad state”Discrete-Time Markov ChainsS is a finite set of statess0 S is an initial stateT :SS[0,1] is the transition relations,s’S s’ T(s,s’)=1L is a labeling function (S, s0, T, L)Markov Chain: Simple ExampleBACD0.2E0.80.91.01.00.50.50.1s0Probabilities of outgoingtransitions sum up to 1.0for every state•Probability of reaching E from s0 is 0.2- 0.5+0.8-0.1-0.5=0.14•The chain has infinite paths if state graph has loops–Need to solve a system of linear equations to compute probabilitiesPRISM[Kwiatkowska et al., U. of Birmingham]Probabilistic model checkerSystem specified as a Markov chain•Parties are finite-state machines w/ local variables•State transitions are associated with probabilities– Can also have nondeterminism (Markov decision processes)•All parameters must be finiteCorrectness condition specified as PCTL formulaComputes probabilities for each reachable state–Enumerates reachable states–Solves system of linear equations to find probabilitiesPRISM SyntaxBACD0.2E0.80.91.01.00.50.50.1s0module Simple state: [1..5] init 1; [] state=1 -> 0.8: state’=2 + 0.2: state’=3; [] state=2 -> 0.1: state’=3 + 0.9: state’=4; [] state=3 -> 0.5: state’=4 + 0.5: state’=5;endmoduleIF state=3 THEN with prob. 50% assign 4 to state, with prob. 50% assign 5 to stateModeling Crowds with PRISMModel probabilistic path constructionEach state of the model corresponds to a particular stage of path construction•1 router chosen, 2 routers chosen, …Three probabilistic transitions•Honest router chooses next router with probability pf, terminates the path with probability 1-pf•Next router is probabilistically chosen from N candidates•Chosen router is hostile with certain probabilityRun path construction protocol several times and look at accumulated observations of the intruderPRISM: Path Construction in Crowdsmodule crowds . . . // N = total # of routers, C = # of corrupt routers // badC = C/N, goodC = 1-badC [] (!good & !bad & run) -> goodC: (good’=true) & (revealAppSender’=true) & (run’=false) + badC: (badObserve’=true) & (run’=false); // Forward with probability PF, else deliver [] (good & !deliver) -> PF: (pIndex’=pIndex+1) & (forward’=true) & (good’=false) + notPF: (deliver’=true);. . .endmoduleNext router is corrupt with certain probabilityRoute with probability PF, else deliverPRISM: Intruder Modelmodule crowds . . . // Record the apparent sender and deliver [] (badObserve & appSender=0) -> (observe0’=observe0+1) & (deliver’=true); . . . // Record the apparent sender and deliver [] (badObserve & appSender=15) -> (observe15’=observe15+1) & (deliver’=true); . . .endmodule• For each observed path, bad routers record apparent sender• Bad routers collaborate, so treat them as a single attacker• No cryptography, only probabilistic inferenceProbabilistic Computation Tree LogicUsed for reasoning about probabilistic temporal properties of probabilistic finite state spacesCan express properties of the form “under any scheduling of processes, the probability that event E occurs is at least p’’•By contrast, Mur can express only properties of the form “does event E ever occur?’’PCTL Logic[Hansson, Jonsson ‘94]State formulas•First-order propositions over a single state ::= True | a | | | | P>p[]Path formulas•Properties of chains of states ::= X | Uk | U PCTL SyntaxPredicate over state variables(just like a Mur invariant)Path formula holdswith probability > pState formula holds fornext state in the chainFirst state formula holds for every state in the chain until second becomes truePCTL: State FormulasA state formula is a first-order state predicate•Just like non-probabilistic logicX=3y=0X=1y=1X=1y=20.2X=2y=00.80.51.01.0s00.5 = (y>1) | (x=1)TrueTrueFalseFalsePCTL: Path FormulasA path formula is a temporal property of a chain of states1U2 = “1 is true until 2 becomes and stays true”X=3y=0X=1y=1X=1y=20.2X=2y=00.80.51.01.0s00.5 = (y>0) U (x>y) holds for this chainPCTL: Probabilistic State FormulasSpecify that a certain predicate or path formula holds with probability no less than some boundX=3y=0X=1y=1X=1y=20.2X=2y=00.80.51.01.0s00.5 = P>0.5[(y>0) U (x=2)]FalseTrueTrueFalseIntruder Model Reduxmodule crowds . . . // Record the apparent sender and deliver [] (badObserve & appSender=0) -> (observe0’=observe0+1) & (deliver’=true); . . . // Record the apparent sender and deliver [] (badObserve & appSender=15) -> (observe15’=observe15+1) & (deliver’=true); . . .endmodule Every time a hostile crowd member receives a message from some honest member, he records his observation (increases the count for that honest
View Full Document
Unlocking...