Game-Based Verification ofContract Signing ProtocolsAlternating Transition SystemsTransition FunctionExample: Two-Player ATSExample: Computing Next StateAlternating-Time Temporal LogicStrategies in ATLTemporal ATL Formulas (I)Temporal ATL Formulas (II)Protocol Description LanguageFairness in ATLTimeliness + Fairness in ATLAbuse-Freeness in ATLModeling TTP and CommunicationMOCHA Model CheckerCS 395TGame-Based Verification ofContract Signing ProtocolsAlternating Transition SystemsGame variant of Kripke structures•R. Alur, T. Henzinger, O. Kupferman. “Alternating-time temporal logic”. FOCS 1997.Start by defining state space of the protocol• Π is a set of propositions• Σ is a set of players• Q is a set of states• Q0⊆ Q is a set of initial states• π: Q →2Πmaps each state to the set of propositions that are true in the stateSo far, this is very similar to MurϕTransition Functionδ: Q×Σ →22Qmaps a state and a player to a nonempty set of choices, where each choice is a set of possible next states• When the system is in state q, each player chooses a set Qa∈δ(q,a)• The next state is the intersection of choices made by all players ∩a∈Σδ(q,a)• The transition function must be defined in such a way that the intersection contains a unique stateInformally, a player chooses a set of possible next states, then his opponents choose one of themExample: Two-Player ATSΣ = {Alice, Bob}¬p ∧¬q¬p ∧ qp ∧¬qp ∧ qp ∧ qA’s choicesB’s choicesExample: Computing Next StateΣ = {Alice, Bob}¬p ∧¬q¬p ∧ qp ∧¬qp ∧ qp ∧ qIf A chooses this set…… B can choose either stateNext stateNext stateAlternating-Time Temporal LogicPropositions p ∈Π¬ϕ or ϕ1∨ϕ2where ϕ,ϕ1,ϕ2are ATL formulas〈〈A〉〉{ϕ, 〈〈A〉〉ϕ, 〈〈A〉〉ϕ1Uϕ2where A⊆Σ is a set of players, ϕ,ϕ1,ϕ2are ATL formulas• These formulas express the ability of coalition A to achieve a certain outcome• {, , U are standard temporal operators (similar to what we saw in PCTL)Define 〈〈A〉〉ϕ as 〈〈A〉〉 true U ϕStrategies in ATLA strategy for a player a∈Σ is a mapping fa:Q+→2Qsuch that for all prefixes λ∈Q* andall states q∈Q, fa(λ⋅q)∈δ(q,a)• For each player, strategy maps any sequence of states to a set of possible next statesInformally, the strategy tells the player in each state what to do next• Note that the player cannot choose the next state. He can only choose a setof possible next states, and opponents will choose one of them as the next state.Temporal ATL Formulas (I)〈〈A〉〉{ϕ iff there exists a set Faof strategies, one for each player in A, such that for all future executions λ∈out(q,Fa) ϕ holds in first state λ[1] • Here out(q,Fa) is the set of all future executions assuming the players follow the strategies prescribed by Fa, i.e., λ=q0q1q2…∈ out(q,Fa) if q0=q and ∀i qi+1∈ ∩a∈Afa(λ[0,i])Informally, 〈〈A〉〉{ϕ holds if coalition A has a strategy such that ϕ always holds in the next stateTemporal ATL Formulas (II)〈〈A〉〉ϕ iff there exists a set Faof strategies, one for each player in A, such that for all future executions λ∈out(q,Fa) ϕ holds in all states• Informally, 〈〈A〉〉ϕ holds if coalition A has a strategy such that ϕ holds in every execution state〈〈A〉〉ϕ iff there exists a set Faof strategies, one for each player in A, such that for all future executions λ∈out(q,Fa) ϕ eventually holds in some state• Informally, 〈〈A〉〉ϕ holds if coalition A has a strategy such that ϕ is true at some point in every executionProtocol Description LanguageGuarded command language• Very similar to PRISM input language (proposed by the same people)Each action described as [] guard → command•guardis a boolean predicate over state variables• command is an update predicate, same as in PRISM• Simple example:[]SigM1B ∧¬SendM2 ∧¬StopB -> SendMrB1’:=true;Fairness in ATL¬〈〈B,Com〉〉(contractA∧¬〈〈Ah〉〉contractB)Bob in collaboration with communication channelsdoes not have a strategyto reach a state in which Bob has Alice’s signaturebut honest Alice does not have a strategyto reach a state in which Alice has Bob’s signatureTimeliness + Fairness in ATL〈〈Ah〉〉(stopA∧(¬contractB→¬〈〈B,Com〉〉contractA))in which she can stop the protocol andHonest Alice always has a strategy to reach a stateif she does not have Bob’s signature then Bob does not have a strategy to obtain Alice’s signature even if he controls communication channelsAbuse-Freeness in ATL¬〈〈A〉〉(proveToC ∧〈〈A〉〉contractB∧〈〈A〉〉(aborted ∧¬〈〈Bh〉〉contractA))she has a strategy to obtain Bob’s signature ANDAlice doesn’t have a strategy to reach state in whichshe can prove to Charlie thata strategy to abort the protocol, i.e., reach a state where Alice has received abort token and Bob doesn’t havea strategy to obtain Alice’s signatureModeling TTP and CommunicationTrusted third party is impartial• This is modeled by defining a unique TTP strategy• TTP has no choice: in every state, the next action is uniquely determined by its sole strategyCan model protocol under different assumptions about communication channels• Unreliable: infinite delay possible, order not guaranteed– Add “idle” action to the channel state machine• Resilient: finite delays, order not guaranteed– Add “idle” action + special constraints to ensure that every message is eventually delivered (rule out infinite delay)• Operational: immediate transmissionMOCHA Model CheckerModel checker specifically designed for verifying alternating transition systems• System behavior specified as guarded commands– Essentially the same as PRISM input, except that transitions are nondeterministic (as in in Murϕ), not probabilistic• Property specified as ATL formulaSlang scripting language• Makes writing protocol specifications easierTry online implementation!•
View Full Document
Unlocking...