Lecture 5 A. Pnueli and L. ZuckIntroduction to CSPCSP is a programming/modeling language based on synchronous message passing.It is intended to model complex reactive systems. UnlikeSPL the main observablesare communication events. Data is viewed as parameters of processes, and ascomponents of messages.The most basic process isStop which stops and does nothing.Basic actions (messages) are sequenced by the prefixing operator→. Thus, theprocessin → out → Stopperforms the actions in followed by out and then stops.Formal Analysis of Security Protocols, NYU, Spring, 2003 18Lecture 5 A. Pnueli and L. ZuckRecursionProcess names can be introduced and used on the left-hand side as well as onthe right-hand side of defining equations. This enables usingrecursion (in factiteration) for modeling infinite behaviors. Thus, the following definitions are allequivalent and represent a process that alternately performs the actionsto and froad infinitum.Alt = to → fro → AltDalt = to → fro → to → fro → DaltMalt1 = to → Malt2 , Malt2 = fro → Malt1Nalt = to → fro → DaltµP.to → fro → PThe operator represents a selection between two possible behaviors. For example,letB and C be two sets of actions. The following process produces the actionout .0 on each “input” of a B-action and produces out.1 on each C-action.P = ?x : B → out.0 → P ?x : C → out.1 → PThe “wild card” ?x : B represents an arbitrary choice of any value out of theaction setB. Once such an action is selected it is bounded to the variable x. Forexample, the following process performs pairs of consecutive actions selected outof a setA.P = ?x : A → x → PFormal Analysis of Security Protocols, NYU, Spring, 2003 19Lecture 5 A. Pnueli and L. ZuckOther Types of SelectionProcesses can be parameterized. This enables associating variable values withprocesses. For example, the following process generates a sequence ofup anddown actions, such that at every prefix of the sequence, the number of up’s isgreater than or equal to the number ofdown’s.Count(0) = up → Count(1)Count(n + 1) = up → Count(n + 2) down → Count(n)Consider again the selection statementP = ?x : B → out.0 → P ?x : C → out.1 → PFor the case that B ∩C = ∅ the selection is always associated with a visible action.On the other hand, ifB ∩ C 6= ∅, then the selection is not immediately visible,because it may be associated with an actiona ∈ B ∩ C. CSP has an explicitinternal selection operator, denoted u.Formal Analysis of Security Protocols, NYU, Spring, 2003 20Lecture 5 A. Pnueli and L. ZuckConditional ProcessesThe language allows also conditional selection depending on data values. Forexample, the following filter process inputs arbitrary integers and outputs only thenon-negative among them:F = in?x → if x ≥ 0 then (out!x → F ) else FThe action out!x is equivalent to out .x. For a boolean expression b, the notationb&P is an abbreviation for the process if b then P else Stop.This combination is useful in order to guard communication actions by booleanguards. For example, the following process described a token moving around anN × M board:Counter(i, j) = (i > 0)&left → Counter(i−1, j) (i < N−1)&right → Counter(i+1, j) (j > 0)&down → Counter(i, j−1) (j < M−1)&up → Counter(i, j+1)Formal Analysis of Security Protocols, NYU, Spring, 2003 21Lecture 5 A. Pnueli and L. ZuckParallel Composition OperatorsCSP has several parallel composition operators. They differ by the amount ofsynchronization on actions which each of them require.On one extreme, we have the operatork which requires synchronization on allvisible actions. The following equivalence captures part of this full synchronizationrequirement:(?x : A → P (x)) k(?x : B → Q(x)) ∼ ?x : A ∩ B → (P (x) kQ(x))As an additional example, consider the process Mult(N, 0) which is always readyto communicatea and communicate b only following a number of a’s which isevenly divisible byN.Mult(N, m) =a → Mult(N, m + 1 mod(N)) m = 0&b → Mult(N, m)The following equivalence shows the effect of forming the parallel composition ofMult(N, 0) and Mult(M, 0):Mult(N, 0) kMult(M, 0) ∼ Mult(lcm(N, M), 0)where lcm(N, M) is the least common multiple of N and M.The most prevalent use of this parallel operator is for modelinghand shaking(synchronous) communication between two processes, as follows:(c!x → P ) k(c?y → Q(y)) ∼ c!x → (P kQ(x))Formal Analysis of Security Protocols, NYU, Spring, 2003 22Lecture 5 A. Pnueli and L. ZuckParallelism with Selective SynchronizationThe interfaced parallel operator P kXQ forms parallel composition while requiringsynchronization on all actions of X. Actions not belonging to X are interleavedwith the rest of the actions. LetP =?x : A → P0(x) and Q =?x : B → Q0(x),thenP kXQ ∼?x : X ∩A ∩ B → P0(x) kXQ0(x) ?x : A − X → P0(x) kXQ ?x : B − X → P kXQ0(x)As another example, consider the parallel composition L k{mid}R, whereL = left?x → mid!x → L and R = mid?x → right!x → RThis parallel composition represents a 1-place buffer which reads a value from leftand eventually outputs it to right. It is almost equivalent to the sequential processB = left?x → right!x → Bexcept, that the parallel composition displays an additional communication eventalong channelmid.At the other extreme of synchronization, we have thestrict interleaving paralleloperatork| which can be defined asP k| Q = P k∅QHere we form a parallel composition based on strict interleaving with nosynchronization.Formal Analysis of Security Protocols, NYU, Spring, 2003 23Lecture 5 A. Pnueli and L. ZuckTwo Representations of a SetLet A be a non-empty set, and let i : A. We present two representations of a classSet which supports the methods add.i, delete.i, and member.i for each i ∈ A,and global methodsempty and nonempty.Set1 (X) =add?i → Set1 (X ∪{i}) delete?i → Set1 (X −{i}) member?i : X → Set1 (X) X = ∅&empty → Set1 (X) X 6= ∅&nonempty → Set1 (X)Here answers to queries are expressed as readiness to synchronize, rather thanreturning a boolean value.The other representation is given bySet2 = kempty{S(i, 0) | i ∈ A}, whereS(i, b) =add.i → S(i, 1) delete.i → S(i,