ep2

AIST and Swansea University
last updated 2023.08.03
[ Isobe > CSP-Prover > ep2 ]
The ep2 system is a new industrial standard of electronic payment systems. It consists of seven autonomous entities centred around the ep2 Terminal: Cardholder (i.e., customer), Point of Service (i.e., cash register), Attendant, POS Management System, Acquirer, Service Center, and Card, (see Fig.1). These entities communicate with the Terminal and, to a certain extent, with one another via XML-messages in a fixed format.  These messages contain information about authorisation, financial transactions, as well as initialisation and status data. The state of each component heavily depends on the content of the exchanged data.


ep2 interface

Fig.1. ep2 interface.


In [gimblett2004], major parts of the ep2 system have been formalized in CSP-CASL [csp-casl]. Following the structure of the original ep2 documents [ep2-docs], the specifications presented in [gimblett2004] can be classified to be e.g. on the Architectural Level, on the Abstract Component Description Level, or on the Concrete Component Description Level. In this context, tool support is needed to prove (1) deadlock freedom for the interaction between the various ep2 components and (2) refinement relations between the different level of abstraction.

Translating the data part of the specifications given in [gimblett2004] into adequate Isabelle code, we obtain specifications in the input format of CSP-Prover. Fig.2 shows a part of [ep2_nucleus.thy] (which is the nucleus of [ep2_acl.thy]) of the initialisation procedure of the ep2 Terminal at the Abstract Component Description Level.

  1. (* data part *)
  2. typedecl init_d       typedecl request_d
  3. typedecl response_d   typedecl exit_d
  4. datatype Data = Init init_d | Exit exit_d | Request request_d | Response response_d
  5. datatype Event = c Data
  6.  
  7. (* process part *)
  8. datatype ACName = Acquirer | AcConfigManagement | Terminal | TerminalConfigManagement
  9. consts  ACfun :: "ACName => (ACName, Event) proc"
  10. primrec
  11.   "ACfun Acquirer = c ? x:(range Init) -> $AcConfigManagement"
  12.   "ACfun AcConfigManagement
  13.          = c !? exit:(range Exit) -> SKIP |~|
  14.            c !? request:(range Request) -> c ? response:(range Response) -> $AcConfigManagement"
  15.   "ACfun Terminal = c !? init:(range Init) -> $TerminalConfigManagement"
  16.   "ACfun TerminalConfigManagement
  17.          = c ? x -> IF (x:range Request)
  18.                     THEN c !? response:(range Response) -> $TerminalConfigManagement
  19.                     ELSE IF (x:range Exit) THEN SKIP ELSE STOP"

  21. defs (overloaded)
  22.   Set_ACfun_def [simp]: "PNfun == ACfun"

  24. consts AC :: "(ACName, Event) proc"
  25. defs   AC_def: "AC == ($Acquirer |[range c]| $Terminal)"

  27. defs FPmode_def [simp]: "FPmode == CMSmode"

Fig.2. ep2 Specification at the Abstract Component Description Level.
The Terminal starts the initialization (line 15) and waits then for data sent by the Acquirer. If this data is of type Request, the Terminal answers with a value of type Response (line 18). Another possibility is that the Acquirer wants to exit (SKIP) the initialization (line 19).  Any other type of communication sent by the Acquirer will lead to a deadlock represented by the process STOP (line 19). On the other end of the communication, after receiving an initialization request (line 11) the Acquirer internally decides if it wants to exit the process (line 13) or interact with the Terminal by sending a request followed by a response of the Terminal (line 14). The system AC to be analyzed here consists of the parallel composition of the Terminal and the Acquirer synchronized on the channel c (line 25).

It is the defining characterization of the Abstract Component Description Level that the data involved is loosely specified.  No specific values are defined (lines 2--5). Semantically this means that -- depending on the interpretation of e.g. the type init_d -- the described systems might involve infinite non-determinism, e.g. if the type init_d has infinitely many values, the Terminal process of Fig.2. chooses internally between sending any of these values (line 15). Thus, CSP-Prover has simulateneously to deal with a class of specifications: it has to prove that a certain property holds for any possible interpretation of the types involved.

Using CSP-Prover, we can show the above described process AC to be stable-failure refinement of the process Seq given in Fig.3.  Note that Seq is a sequential, i.e. by syntactic characterization deadlock-free process.  As stable failure refinement preserves deadlocks, establishing this refinement proves that the interaction of Terminal and Acquirer on the Abstract Component Description Level is deadlock free. Fig.4 shows the complete script to prove the stable-failure refinement Seq =F AC (line 14) in CSP-Prover.  First, a mapping is defined from the process names in Seq to process expressions in AC (line 3-5).  It is hard to automatically derive such corrensondences. However, CSP-Prover offers assistence for easy cases. Next, it is shown that the involved recursive processes are guarded and do not use the hiding operator.  This is a fully automated routine work (lines 8--11). After these preparations, Seq =F AC is given as a goal (line 14).  Using the above mapping, now the recursive processes are unfolded to a base case and step cases by fixed point induction (line 16). Since a step case is produced for each of the process names of Seq, the step cases are instantiated by induction on SeqName (line 18).  Finally, the theorem is proven by Isabelle's method auto, CSP-Prover's method cspF_auto, which transforms any expression into a head sequential form, and cspF_decompo, which decomposes CSP-operators, etc (line 20). See the User-Guide for more details of CSP-laws and methods.

  1. datatype SeqName = SeqInit | Loop
  2. consts Seqfun :: "SeqName => (SeqName, Event) proc"
  3. primrec
  4.   "Seqfun SeqInit  = c !? init:(range Init) -> $Loop"
  5.   "Seqfun Loop     = c !? exit:(range Exit) -> SKIP |~|
  6.                      c !? request:(range Request) -> c !? response:(range Response) -> $Loop"

  8. defs (overloaded)
  9.   Set_Seqfun_def [simp]: "PNfun == Seqfun"

  11. consts Seq :: "(SeqName, Event) proc"
  12. defs   Seq_def: "Seq == $SeqInit"

Fig.3. A sequential process equal to the process shown in Fig.2.

  1. (* expected correspondence of process names in Abs to AC *)
  2. consts Seq_to_AC :: "SeqName => (ACName, Event) proc"
  3. primrec
  4.   "Seq_to_AC (SeqInit) = ($Acquirer |[range c]| $Terminal)"
  5.   "Seq_to_AC (Loop)    = ($AcConfigManagement |[range c]| $TerminalConfigManagement)"

  7. (* guarded and no hiding operator *)
  8. lemma guardedfun_AC_Seq[simp]:
  9.       "guardedfun ACfun"
  10.       "guardedfun Seqfun"
  11. by (simp add: guardedfun_def, rule allI, induct_tac p, simp_all)+
  12.  
  13. (* the main thorem *)
  14. theorem ep2: "Seq =F AC"
  15. apply (unfold Seq_def AC_def)
  16. apply (rule cspF_fp_induct_left[of _ "Seq_to_AC"])
  17. apply (simp)+
  18. apply (induct_tac p)

  20. apply (cspF_auto | rule cspF_decompo_ref | auto simp add: image_iff)+
  21. done

Fig.4. The complete proof script for Seq =F AC.



In the more complex version [ep2_acl.thy], Abs <=F AC can be similarly proved by CSP-Prover. Furthermore, it can be proven in [ep2_ccl.thy] that Concrete Component Description Level (CC) refines Abstract Componet Level (AC), thus for all p, AC <=F CC p, where p is the initial value. Hence, we also know for the Concrete Component Description Level that the dialog between Terminal and Acquirer of the formal ep2 specification presented in [gimblett2004] does not give rise to a deadlock of the ep2 system. The theory files used here are summarized as follows:

    ep2_nucleus.thy    The nucleus of ep2 verification
    ep2_nucleusDF.thy  The verification of deadlock-freeness of ep2 by DFP
    ep2_acl.thy        Abstract Componet Level (AC) refines an abstraction (Abs).
    ep2_ccl.thy        Concrete Component Description Level (CC) refines Abstract Componet Level (AC),

References

[gimblett2004] A. Gimblett, M. Roggenbach, and H. Schingloff. Towards a formal specification of an electronic payment system in CSP-CASL. WADT 2004, LNCS, (to be appeared)

[csp-casl] M. Roggenbach. CSP-CASL -- A new integration of process algebra and algebraic specification. AMiLP 2003. pp.229--243. 2003.

[ep2-docs] eft/pos 2000 Specification, version 1.0.1, EP2 Consortium, 2002.

[proofgeneral] David Aspinall. Proof General: A Generic Tool for Proof Development. TACAS 2000, LNCS 1785, pp.38--42, 2000.