Laura Voinea
email: a.voinea.1@research.gla.ac.uk

Ornela Dardha
email: ornela.dardha@glasgow.ac.uk

Simon J Gay
email: simon.gay@glasgow.ac.uk

A Laura Voinea

Typechecking Java Protocols with [St]Mungo

Keywords: multiparty session types, typestate, Mungo, StMungo, HTTP protocol

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The concept of an application programming interface (API) is central to software architecture and implementation. An API is a specification of a collection of related programming language operations that enable the use of a particular kind of functionality. For example, in a typical programming language, the functionality for implementing graphical user interfaces is organised and described as an API. In an object-oriented language, an API is presented as a collection of classes, each with methods for a range of related operations. A specific example is the JavaFX API, which provides graphics and media functionality -in fact JavaFX is so large that it is better described as a collection of APIs for more specific purposes, such as media streaming and web rendering.

Nowadays, APIs are not only used to present the library functions of programming language implementations. They can also package up the functionality of distributed services, and be called remotely in networked applications. A significant trend is the development and publication of APIs to allow access to functions that were previously internal to a software application. For example, the developer of a student records database might publish an API to allow programmatic access to the data, and this could be used by third-party developers to produce applications that make use of student records to provide additional services. This evolution of the API concept has become a key aspect of open software development and service-oriented system architectures. In a commercial setting it has enabled the birth of an API economy in which the provision of APIs can be monetised. APIs have thus become a key focus of the software industry.

Typical methods in an API require parameters, and these can be specified using standard type-theoretic techniques. In a statically typed language, each method in an API has its type signature, specifying the types of its parameters and the type of any result that it returns. The standard techniques of typechecking, especially when implemented in an integrated development environment (IDE), are effective in supporting programmers to use APIs correctly, identifying errors during development rather than waiting until the testing phase when they are much more expensive to correct.

The description of an API as a collection of typed method signatures however, does not capture any constraints on the sequence in which methods can be called. For example, an API for working with files requires that a file must be successfully opened before it can be read or written. After the file has been closed, it cannot be read or written any more, and the only available method is open. Another standard example is the Iterator class in Java, in which the hasNext method must be called (and return true) before the next method can be called.

Another category of examples arises in APIs for communication, in concurrent or distributed systems. Typically the communication within a system is structured around various communication protocols, each of which specifies a permitted sequence of messages and the format (type) of each message. An API whose operations allow sending and receiving of messages in a given protocol has constraints so that the operation calls follow the protocol specification. These constraints cannot be expressed purely within the framework of typed method signatures, more expressive types and type systems are needed. In general, we can speak of behavioural APIs, a term based on the term behavioural types for type systems that specify sequence-related properties involving multiple method calls.

Two established lines of research are relevant in this context. One is typestates [START_REF] Strom | Typestate: A programming language concept for enhancing software reliability[END_REF], which is the idea of using static type systems to specify permitted sequences of method calls. The other is session types [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Takeuchi | An interaction-based language and its typing system[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], which are type-theoretic descriptions of communication protocols. The StMungo and Mungo tools are the result of convergence between these two lines of research [START_REF] Kouzapas | Typechecking protocols with mungo and stmungo[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo: A session type toolchain for java[END_REF][START_REF] Dardha | Mungo and StMungo: Tools for typechecking protocols in Java[END_REF][START_REF]Mungo webpage[END_REF]. On the one hand, APIs for communication protocols are clearly a special case of behavioural APIs in general. On the other hand, transferring the concepts of session types from process calculi or functional languages to object-oriented languages requires embedding them in a more general setting that supports typestates. This is because it is natural to define methods that each perform several communication steps, and then the original communication protocol (session type) gives rise to different, although related, sequencing constraints on the methods.

StMungo is a bridge between session types and typestates, by translating multiparty session types (MPST) [START_REF] Honda | Multiparty asynchronous session types[END_REF] written in the Scribble language [START_REF]Scribble project homepage[END_REF] into typestate specifications for Java classes. The key steps are given in the following:

-Scribble is used as a specification language for global protocols (or global types) describing communication among all involved participants in a communication protocol in a distributed system. -The Scribble tools are used to validate and project a global type into local protocols (or local types) for each participant involved. -StMungo translates Scribble local types into typestate specifications for Java classes, describing the Java object protocols, namely the permitted sequences of method calls of an object. -StMungo also generates an API implementation for each participant, which follows its typestate specification, described in the previous step.

At this stage we can run the Mungo tool. The key ideas and steps behind Mungo are given in the following:

-Typestate specifications are expressed as annotations of Java classes, so there is no change to the language itself. -Linear typing is used to control aliasing, so that there is no possibility of inconsistent views of an object's state. -The Mungo typechecker checks that method calls are performed following the object's protocol, as specified by its associated typestate. -If Mungo typechecking is successful and no errors are reported, then the code is compiled with javac and run as standard Java code. -The Mungo typechecker is formalised inspired by session types theory and the resulting type system is proved correct via the standard theorems of progress and subject reduction [START_REF] Kouzapas | Typechecking protocols with mungo and stmungo[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo: A session type toolchain for java[END_REF].

In the remainder of this tutorial paper we will describe the StMungo § 2 and Mungo § 3 tools via a real-world case study, the HTTP protocol. In § 4 we give step-by-step instructions on how to run the tools. In § 5 we discuss related work and in § 6 we conclude the paper and discuss future work.

StMungo

The StMungo tool is a Java-based transpiler implemented using the ANTLR v4.5 framework [START_REF]Antlr project homepage[END_REF]. StMungo acts as a bridge between multiparty session types and typestate specifications. In particular it is the link between the Scribble specification language [START_REF]Scribble project homepage[END_REF][START_REF] Honda | Scribbling interactions with a formal foundation[END_REF] and the Mungo tool § 3. StMungo is the first tool to provide a practical embedding of Scribble multiparty session types into an object-oriented language with typestates.

In order to better understand the StMungo tool, we need to describe both the Scribble language and the typestate specifications. Let's start with Scribble.

The Scribble specification language is an implementation of multiparty session types (MPST) [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF]Scribble project homepage[END_REF]. Participants in a distributed system communicate among each other by sending and receiving messages and following a predefined communication protocol. Such protocol is given as a global protocol (or global type) in Scribble. The Scribble tools can perform validation and projection of a global protocol. First, we must check if the specified global protocol is valid, meaning if it is correct with respect to transmitted data; there are no deadlocks within the global protocol; there are no un-notified participants for example, regarding session termination, and so on. These checks follow the MPST theory [START_REF] Honda | Multiparty asynchronous session types[END_REF]. Once a global protocol is validated, with Scribble tools we can project it into local protocols (or local types) for each participant in the system.

The HTTP Protocol Case Study Let us illustrate the notions of global and local protocols using our HTTP case study. HTTP (HyperText Transfer Protocol) [START_REF] Fielding | Hypertext transfer protocol (HTTP/1.1): message syntax and routing[END_REF] is the underlying data protocol used by the World Wide Web defining how messages are formatted and transmitted, and what actions servers and clients may take in response to various methods, such as GET, PUT or POST. An HTTP session is a sequence of network request-response transactions, initiated by the client sending a request over a TCP connection to a particular port of a server. Upon receiving the request, the server listening on that port sends back a status line, such as "HTTP/1.1 200 OK", and a message of its own. The structure of the request and response messages exchanged is rich and complex, lending itself to be further specified through session types. Hence, we represent the HTTP global protocol in the style of Hu [START_REF] Hu | Distributed Programming Using Java APIs Generated from Session Types[END_REF] where an HTTP request and response are broken down respectively into sending and receiving a request linerequest, followed by zero or more header-fieldshost or usera terminated by a new-line. This fine grained representation of the protocol is made possible by the message being broken down via TCP bit streams, in a manner that is transparent to the parties involved.

The global protocol for HTTP specified in Scribble is given in Listing 1.1. Line 1 contains the module declaration, made up of an optional package prefix i.e., http, and the name of the file containing the module, Http. Line 2 contains a payload type declaration type <java>..., which gives an alias (str) to a data type (String) from an external language java which can be used in the payload of a message signature. A module can contain zero or more global protocol declarations, consisting of a protocol signature (line 4), choices (lines 5 and 27), message passing (line 6), and recursion (line 7). Lines 11-46 model a correctly formatted client request and lines 49-91 a server response. Using the Scribble tools, we can project the HTTP global protocol onto local protocols for the server S and the client C. In this tutorial we will focus only on the client side as we will interact with real-world HTTP servers. The local protocol for the HTTP client C, given in Listing 1.2, describes the behaviour of this role. The _C in the protocol name indicates that C is the local endpoint. For simplicity, we limit this protocol to the GET command only, with the rest being represented in a similar manner. The client can send a request line request (line 4), followed by zero or more header-fieldshost, or userA and so on. The server responds with a line containing the HTTP versionhttpv (line 18) followed by the status of the request, either -200 for a found resource, or -404 for a bad request. The server can choose zero or more header-fields to follow this message with. The StMungo tool takes in input a Scribble local protocol for a role and translates it into a typestate specification for a Java API skeleton. This translation is based on the principle that each role in the multiparty session communication following its local protocol, can be abstracted as a Java class following its typestate specification. A typestate is a state machine defining the permitted sequence of method calls of a Java object, thus defining the object's protocol. subset of the methods defined by the class; each method specifies a transition to a successor state, such that when called at runtime allows the object to change state as specified by its typestate. The send and receive operations given in the client's local protocol are translated as typestate methods in CProtocol.protocol. For example, the message request(str) to S (line 4, Listing 1.2) where the client sends a request message of type str to the server, is translated as two method calls due to formatting and parsing (lines 2-3 in Listing 1.3). Calling the first method void send_REQUESTToS() specifying the method and calling the second method void send_requestStrToS(String) requests the rest of the message of type String (further details in § 3).

We will comment on the other two files CRole.java and CMain.java in § 3.

Mungo

The Mungo tool is a Java front-end tool used to statically typecheck typestate specifications for Java classes. The tool is implemented in Java using the ExtendJ framework [START_REF] Hedin | An introductory tutorial on jastadd attribute grammars[END_REF][START_REF] Öqvist | Extendj: extensible java compiler[END_REF], a meta-compiler based on reference attribute grammars. Mungo extends a Java class with a typestate specification, which is saved in a separate file (such as CProtocol.protocol in § 2) and is attached to a Java class using the annotation @Typestate("ProtocolName"), where "ProtocolName" names the file where the typestate is defined. The typestate inference algorithm given by the formalisation of the Mungo tool in [START_REF] Kouzapas | Typechecking protocols with mungo and stmungo[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo: A session type toolchain for java[END_REF] constructs the sequences of methods called on all objects associated with a typestate, and then checks if the inferred typestate is a subtype of the object's declared typestate. The formalisation of the typestate inference system and its soundness properties are beyond the scope of this paper and the reader is referred to [START_REF] Kouzapas | Typechecking protocols with mungo and stmungo[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo: A session type toolchain for java[END_REF].

Source files are typechecked in two phases: first, according to the standard Java type system, and then to the typestate type system via Mungo. The source files can then be compiled using standard javac and executed in the standard Java runtime environment.

The typestate specification generated from StMungo together with the Mungo typechecker can guide the user in the design and development of distributed multiparty communication-based systems with guarantees of communication safety and soundness.

We will now describe the use of Mungo via our running example, the HTTP protocol, and in particular we will do so by commenting on the last two files CRole.java and CMain.java generated by StMungo for the HTTP client C.

The HTTP Protocol Case Study (Continued)

The HTTP client API is given by Listing 1.4 annotated by the typestate CProtocol, defined in Listing 1.3.

Lines 3-9 define the client's constructor where the connection phase over Java sockets takes place. The rest of CRole contains a minimal implementation of the methods specified in the typestate CProtocol. The methods for sending and receiving messages contain basic formatting and parsing, which can be further improved by the programmer. Lines 8-9 define the two methods for sending the initial, mandatory, request line -send_REQUESTToS (for the method, i.e."GET") and send_requestStrToS (for the rest of the message). Lines 11-34 define methods for receiving the first line in a response, composed of the HTTP version -receive_httpvStrFrom and the status. The method in line 16 Choice1 receive_Choice1LabelFromS captures the status. This method returns a Choice1 type, which is an enumerated type defined as: enum Choice1 { _200 , _404 ;} For each choice there is an enumerated type, named by StMungo according to the position of the choice in the sequence of choices within the local protocol. The values of the enumerated type are the names of the first message in each branch of the choice, for example for Choice1 they are _200 or _400. Thus, the method receive_Choice1LabelFromS receives a message which represents one of the two status codes, and it returns the corresponding enum value.

Let's move now onto the CMain.java given in Listing 1.5. CMain.java contains a minimal implementation of the client endpoint using the CRole class to communicate with the server endpoint. Below we give the main method, omitting any auxiliary methods generated by StMungo. The code is modified from the generated version by adding the request and host messages needed to request the home page from www.google.co.uk. ... // other cases corresponding to the header fields case BODY : currentC . receive_bodyStrFromS () ; [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Takeuchi | An interaction-based language and its typing system[END_REF] and multiparty session types [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]. The BETTY project1 produced three survey articles: one on foundations of behavioural types [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF], one on behavioural types and security [START_REF] Capecchi | Information flow safety in multiparty sessions[END_REF] and one on behavioural types in programming languages [START_REF] Ancona | Behavioral types in programming languages[END_REF]. The project also produced a book [START_REF]Behavioural Types: from Theory to Tools[END_REF] describing implementations of programming languages and tools based on behavioural types. The ABCD project2 has produced a list of implementations of session types in programming languages.

Since the introduction of typestate [START_REF] Strom | Typestate: A programming language concept for enhancing software reliability[END_REF], there have been several projects to add the concept to practical programming languages. Vault [START_REF] Deline | Enforcing high-level protocols in low-level software[END_REF][START_REF] Fähndrich | Adoption and focus: Practical linear types for imperative programming[END_REF] is an extension of C, and Fugue [START_REF] Deline | Typestates for objects[END_REF] applies similar ideas to C#. Plural [START_REF] Bierhoff | Practical API protocol checking with access permissions[END_REF] is based on Java and has been used to study access control systems [START_REF] Bierhoff | Modular typestate checking of aliased objects[END_REF] and transactional memory [8], and to evaluate the effectiveness of typestate in Java APIs [START_REF] Bierhoff | Practical API protocol checking with access permissions[END_REF]. Sing# [START_REF] Fähndrich | Language support for fast and reliable message-based com-munication in singularity OS[END_REF] is an extension of C# which was used to implement Singularity, an operating system based on message-passing. It incorporates typestate-like contracts, which are a form of session type, to specify protocols. Bono et al. [START_REF] Bono | Typing copyless message passing[END_REF] have formalised a core calculus based on Sing# and proved type safety.

The Plaid programming language [START_REF] Aldrich | Typestate-oriented programming[END_REF][START_REF] Sunshine | First-class state change in Plaid[END_REF] proposes a new paradigm of typestateoriented programming. Instead of class definitions, a program consists of state definitions containing methods that cause transitions to other states. Transitions are specified in a similar way to Plural's pre-and post-conditions. Like classes, states are organised into an inheritance hierarchy. Recent work [START_REF] Garcia | Foundations of typestate-oriented programming[END_REF][START_REF] Wolff | Gradual typestate[END_REF] uses gradual typing to integrate static and dynamic typestate checking.

Bodden and Hendren [START_REF] Bodden | The clara framework for hybrid typestate analysis[END_REF] developed the Clara framework, which combines static typestate analysis with runtime monitoring. The monitoring is based on the trace matches approach [START_REF] Allan | Adding trace matching with free variables to aspectj[END_REF], using regular expressions to define allowed sequences of method calls. The static analysis attempts to remove the need for runtime monitoring, but if this is not possible, the runtime monitor is optimised.

A challenge in typestate systems is aliasing. State changes to a given object must be reflected in all references that point to that object, otherwise inconsistency can result in violations of type safety. The literature includes several approaches to alias control. Some work, including ours, uses linear typing to forbid aliasing completely. The adoption and focus approach of Vault and Fugue, and the permission-based approaches of Plural and Plaid, are more flexible. Militão et al. [START_REF] Militão | Aliasing control with viewbased typestate[END_REF] present an expressive fine-grained system. Crafa and Padovani [START_REF] Crafa | The chemical approach to typestate-oriented programming[END_REF][START_REF] Padovani | Deadlock-free typestate-oriented programming[END_REF] present an approach to concurrent typestate-oriented programming, allowing objects to be accessed and modified concurrently by several processes, each potentially changing only part of their state. Some work [START_REF] Hu | Hybrid session verification through endpoint API generation[END_REF][START_REF] Padovani | A simple library implementation of binary sessions[END_REF] combines static checking of typestate (or session type) properties with dynamic monitoring of (non-)aliasing properties. Balzer et al. [START_REF] Balzer | Manifest deadlock-freedom for shared session types[END_REF] augment session types with points at which locks need to be acquired in order to perform state-changing operations; this approach has not yet been applied to a typestate system.

There is relatively little work combining behavioural types and typestate in the way that Mungo and StMungo do. The only other research we are aware of is the API generation approach of Hu [START_REF] Hu | Distributed Programming Using Java APIs Generated from Session Types[END_REF]. The idea is to translate a Scribble protocol into a collection of classes for a standard language such as Java [START_REF] Hu | Hybrid session verification through endpoint API generation[END_REF], F# [START_REF] Neykova | A session type provider: compiletime API generation of distributed protocols with refinements in F#[END_REF] or Go [START_REF] Castro-Perez | Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures[END_REF]. Each class represents a particular state in a protocol, with the methods available in that state. Each method returns the object on which it was called, but with a different class corresponding to the new state of the object. Because each state has its own class, standard IDEs can show the programmer which methods are available; however, for a complex protocol there can be a large number of classes. Runtime monitoring is used to check absence of aliasing.

For this tutorial we have used an example based on a standard internet protocol, HTTP. In previous work with Mungo and StMungo we have analysed SMTP [START_REF] Kouzapas | Typechecking protocols with mungo and stmungo[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo: A session type toolchain for java[END_REF] and POP3 [START_REF] Dardha | Mungo and StMungo: Tools for typechecking protocols in Java[END_REF]. Hu et al. also use SMTP [START_REF] Hu | Hybrid session verification through endpoint API generation[END_REF][START_REF] Neykova | A session type provider: compiletime API generation of distributed protocols with refinements in F#[END_REF] and HTTP [START_REF] Hu | Distributed Programming Using Java APIs Generated from Session Types[END_REF] as case studies.

Conclusion and Future Work

We have presented a tutorial on using the [St]Mungo toolchain for static typechecking of a communication protocols. StMungo connects the Scribble specification language, used to define communication protocols, to Mungo by translating multiparty session types into typestate specifications. Mungo extends Java with typestate specifications, which annotate classes and define the permitted sequence of method calls of Java objects. We illustrate the workflow of both tools through implementing a substantial case study, an HTTP client. We use this client to communicate with a real-world server, the www.google.co.uk server.

While the toolchain is effective for statically typechecking the correct implementation of communication protocols, we intend to further improve its features for distributed programming in Java. On the StMungo side, we will keep it up to date with any changes in the Scribble specification language. On the Mungo side, we aim to offer static typechecking of generics and exceptions. To support generics, method calls on an object whose type is a generic parameter must be typechecked against the typestate specification of the parameter's upper bound. To support typechecking of exception handlers, typestate specifications must define the state transitions corresponding to exceptions, and check the transitions are consistent with the states of fields at the point where an exception is thrown. While existing work on exceptions in session types [START_REF] Carbone | Structured interactional exceptions in session types[END_REF] provides inspiration, the complexities of Java's exception mechanism need to be accounted for as well. Another aim is to improve Mungo's error messages to better allow debugging.

  module http . Http ; type < java > " java . lang . String " from " rt . jar " as str ; global protocol Http ( role C , role S ) { choice at C { // Request request ( str ) from C to S ; // GET / HTTP /1.1 rec X { choice at C { host ( str ) from C to S ; // Host : www . google . co . uk continue X ; } or { userA ( str ) from C to S ; // User -Agent :... continue X ; } or { acceptT ( str ) from C to S ; // Accept : text / html ... continue X ; } or { ... // other header fields body ( str ) from C to S ; }}} // Response httpv ( str ) from S to C ; // HTTP /1.1 choice at S { 200( str ) from S to C ; // 200 OK } or { 404( str ) from S to C ; // 404 Bad Request } rec Y { choice at S { date ( str ) from S to C ; // Date : ... continue Y ; } or { server ( str ) from S to C ; // Server :... continue Y ; } or { strictTS ( str ) from S to C ; // Strict -Transport -Security continue Y ; } or { ... // other header fields body ( str ) from S to C ; }}} Listing 1.1. HTTP Global Protocol

  ... local protocol Http_C ( role C , role S ) { choice at C { request ( str ) to S ; rec X { choice at C { host ( str ) to S ; continue X ; } or { userA ( str ) to S ; continue X ; } or { acceptT ( str ) to S ; continue X ; } or { ... // other header fields body ( str ) to S ; }}} httpv ( str ) from S ; choice at S { 200( str ) from S ;

  The HTTP Protocol Case Study (Continued) Running StMungo on the HTTP client protocol Listing 1.2 produces the following files, where C at the beginning of each file name stands for client. 1. CProtocol.protocol: the typestate specification representing the HTTP client's local protocol. The send and receive operations are translated as Java methods (Listing 1.3 below in this section). 2. CRole.java: the Java API implementing the HTTP client. This class implements the typestate CProtocol over Java sockets (Listing 1.4, § 3). 3. CMain.java: this can be an optional file. It gives a minimum logic of the client CRole and provides a main() method (Listing 1.5, § 3). The typestate specification CProtocol.protocol for the HTTP client is given in Listing 1.3.typestate CProtocol { State0 = { void send_REQUESTToS () : State1 } State1 = { void send_requestStrToS ( String ) : State2 } State2 = { void send_HOSTToS () : State3 , void send_USERAToS () : State4 , void send_ACCEPTTToS () : State5 , ... // send other labels void send_BODYToS () : State12 } State3 = { void send_hostStrToS ( String ) : State2 } State4 = { void send_userAStrToS ( String ) : State2 } ... // send other main messages State12 = { void send_bodyStrToS ( String ) : State13 } State13 = { String r eceiv e_ht tpvSt rFro mS () : State14 } State14 = { Choice1 r e c e i v e _ C h o i c e1 L a b e l F r o m S () : < _200 : State15 , _404 : State16 >} State15 = { String receive_200StrFromS () : State17 } State16 = { String receive_404StrFromS () : State17 } State17 = { Choice2 r e c e i v e _ C h o i c e2 L a b e l F r o m S () : < DATE : State18 , SERVER : State19 , STRICTTS : State20 , ... , BODY : State28 >} State18 = { String receive_dateStrFromS () : State17 } State19 = { String rec ei ve _se rv er Str Fr om S () : State17 } State20 = { String r ec e i v e_ s t r ic t T S St r F r om S () : State17 } ... State28 = { String receive_BODYStrFromS () : end }} Listing 1.3. Typestate Specification A typestate is a state machine (Fig. 1) with states labelled State0 (initial state), State1, State2 . . . Each state offers a set of methods that must be a s e n d _ H O S T T o S ( ) v o i d s e n d _ U S E R A T o S i n g r e c e i v e _ 2 0 0 S t r F r o m S ( ) S t r i n g r e c e i v e _ 4 0 4 S t r F r o m S ( )

Fig. 1 .

 1 Fig. 1. State machine for CProtocol

@

  Typestate ( " CProtocol " ) public class CRole { public CRole () { ... // Bind the sockets and accept a client connection try { // Create the read and write streams socketSIn = new BufferedReader (...) ; socketSOut = new PrintWriter (...) ;} catch ( IOException e ) {...}} public void send_REQUESTToS () { this . socketSOut . print ( " GET " ) ;} public void send_requestStrToS ( String payload ) { this . socketSOut . println ( payload ) ;} ... // Define all other send methods in CProtocol public String re ceiv e_htt pvSt rFrom S () () { String line = " " ; try { line = this . socketSIn . readLine () ;} catch ( IOException e ) {...} return line ;} public Choice1 r e c e i v e _ C h oi c e 1 L a b e l F r o m S () { try { stringLabelChoice1 = this . socketSIn . readLine () ;} catch ( IOException e ) {..= this . socketSIn . readLine () ;} catch ( IOException e ) {...} return line ;} public String receive_404StrFromS () { String line = " " ; try { line = this . socketSIn . readLine () ;} catch ( IOException e ) {...} return line ;} ... /* Define all other receive methods in CProtocol */ }}} Listing 1.4. Client API

  public static void main ( String [] args ) { CRole currentC = new CRole () ; String sread = // input REQUEST if ( " REQUEST " . equals ( sread ) ) { currentC . send_REQUESTToS () ; currentC . send_requestStrToS ( " / HTTP /1.1 " ) ; _X : do { sread = // input header choice switch ( sread ) { case ( " HOST " ) : currentC . send_HOSTToS () ; currentC . send_hostStrToS ( " www . google . co . uk " ) ; continue _X ; ... // other cases corresponding to header fields case ( " BODY " ) : currentC . send_BODYToS () ; currentC . send_bodyStrToS ( " / r / n " ) ; break _X ; }} while ( true ) ;} currentC . rec eive_ http vStrF romS () ; switch ( currentC . r e c e i v e _ C ho i c e 1 L a b e l F r o m S () . r e c e i v e _ C ho i c e 2 L a b e l F r o m S () ) { case DATE : currentC . receive_dateStrFromS () ; continue _Y ;

COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY), www.behavioural-types.eu

EPSRC EP/K034413/1 From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD), groups.inf.ed.ac.uk/abcd/

Supported by the UK EPSRC grant EP/K034413/1, "From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD)", by the EU HORIZON 2020 MSCA RISE project 778233 "BehAPI: Behavioural Application Program Interfaces", and by an EPSRC PhD studentship.

In line 2 we create a new HTTP client, currentC, and proceed by showing the code for a small correctly formatted request, with the initial, mandatory request line messages being sent first (lines 5-6); then among the recursive choice cases we show the code for sending the the host field (lines 10-11), before concluding the request by an empty body (lines [START_REF] Castro-Perez | Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures[END_REF][START_REF] Crafa | The chemical approach to typestate-oriented programming[END_REF]. Then currentC will receive the response status line (lines 19-26) followed by recursive choice cases for the fields to be received from the server (lines [START_REF] Honda | Scribbling interactions with a formal foundation[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Hu | Distributed Programming Using Java APIs Generated from Session Types[END_REF][START_REF] Hu | Hybrid session verification through endpoint API generation[END_REF][START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo[END_REF][START_REF] Kouzapas | Typechecking protocols with mungo and stmungo: A session type toolchain for java[END_REF][START_REF] Militão | Aliasing control with viewbased typestate[END_REF].

To ensure that methods of the protocol are called in a valid sequence and that all possible responses are handled, the CMain implementation is checked by computing the sequences of method calls that are made on the currentC object, inferring the minimal typestate specification that allows them, and then comparing it with the specification declared in CProtocol. The tools together with the HTTP example and further examples can be obtained from the [St]Mungo repository [START_REF]Mungo repository[END_REF].

The tools come prebuilt and ready to use as runnable jar files: stmungo.jar and mungo.jar. In the same repository we also provide the latest release -0.4.3, of the command line tool for Scribble.

We show how to use these tools via the HTTP example, assuming the root folder of the repository linked above.

To run the Scribble tool on the global protocol for validation only: ./scribble -0.4.3/scribblec.sh demos/http/Http.scr

To run the Scribble tool on the global protocol and project the client role: ./scribble-0.4.3/scribblec.sh demos/http/Http.scr -project http C

To run StMungo and obtain the Java prototype implementation: java -jar stmungo.jar demos/http/Http_C.scr

To run Mungo: java -jar mungo.jar demos/http/CMain.java Finally, if no errors are reported, the code can be compiled with javac and run as standard Java code.

Related Work

There is a huge and growing literature on session types and other forms of behavioural types, going back to the original papers on binary session types


Gerhard Goos

Elisa Bertino

Wen Gao

Bernhard Steffen

Gerhard Woeginger

ISBN 978-3-030-50086-3 (eBook) https://doi.org/10.1007/978-3-030-50086-3 LNCS Sublibrary: SL2 -Programming and Software Engineering © IFIP International Federation for Information Processing 2020 The chapter "Conformance-Based Doping Detection for Cyber-Physical Systems" is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/). For further details see license information in the chapter. This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. This Springer imprint is published by the registered company Springer Nature Switzerland AG The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland Together, these conferences cover a broad spectrum of distributed computing subjects, ranging from theoretical foundations and formal description techniques to systems research issues. As is customary, the event also included several plenary sessions in addition to the individual sessions of each conference, that gathered attendants from the three conferences. These included joint invited speaker sessions and a joint session for the best papers from the respective three conferences.

Associated with the federated event, two satellite events took place:

-The 13th International Workshop on Interaction and Concurrency Experience (ICE 2020) -The First International Workshop on Foundations of Consensus and Distributed Ledgers (FOCODILE 2020) I would like to thank the Program Committee chairs of the different events for their help and cooperation during the preparation of the conference, and the Steering Committee and Advisory Boards of DisCoTec and their conferences for their guidance and support. The organization of DisCoTec 2020 was only possible thanks to the dedicated work of the Organizing Committee, including Davide Basile and Francisco "Kiko" Fernández Reyes (publicity chairs), Antonis Achilleos, Duncan Paul Attard, and Ornela Dardha (workshop chairs), Lucienne Bugeja (logistics and finances), as well as all the students and colleagues who volunteered their time to help. Finally, I would like to thank IFIP WG 6.1 for sponsoring this event, Springer's Lecture Notes in Computer Science team for their support and sponsorship, EasyChair for providing the reviewing framework, and the University of Malta for providing the support and infrastructure to host the event.

June 2020

Adrian Francalanza

Preface

This volume contains the papers presented at the 40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2020), held as one of three main conferences of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020), during June 15-19, 2020, online due to the coronavirus pandemic. FORTE is a well-established forum for fundamental research on theory, models, tools, and applications for distributed systems, with special interest in:

• Software quality, reliability, availability, and safety • Security, privacy, and trust in distributed and/or communicating systems • Service-oriented, ubiquitous, and cloud computing systems • Component-and model-based design • Object technology, modularity, and software adaptation • Self-stabilization and self-healing/organizing • Verification, validation, formal analysis, and testing of the above The Program Committee received a total of 25 submissions, written by authors from 18 different countries. Of these, 11 papers were selected for inclusion in the scientific program. Each submission was reviewed by at least three Program Committee members with the help of 10 external reviewers in selected cases. The selection of accepted submissions was based on electronic discussions via the EasyChair conference management system.

As program chairs, we actively contributed to the selection of the keynote speakers of DisCoTec 2020 (which due to the conference being held online are not all confirmed at the time of writing).

This year DisCoTec also includes a Tutorial Day of six invited tutorials. This volume includes the following tutorial papers:

• Parameterised Verification with Byzantine Model Checker • Typechecking Java Protocols with [St] Mungo

We wish to thank all the authors of submitted papers, all the members of the Program Committee for their thorough evaluations of the submissions, and the external reviewers who assisted the evaluation process. We are also indebted to the Steering Committee of FORTE for their advice and suggestions. Last but not least, we thank the DisCoTec general chair, Adrian Francalanza, and his organization team for their hard, effective work in providing an excellent environment for FORTE 2020 and all other conferences and workshops, despite of the pandemic troubles.

June 2020

Alexey Gotsman Ana Sokolova

Foreword

  The 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020) took place during June 15-19, 2020. It was organized by the Department of Computer Science at the University of Malta, but was held online due to the abnormal circumstances worldwide affecting physical travel.The DisCoTec series is one of the major events sponsored by the International Federation for Information Processing (IFIP). It comprises three conferences:-The IFIP WG 6.1 22nd International Conference on Coordination Models and Languages (COORDINATION 2020) -The IFIP WG 6.1 20th International Conference on Distributed Applications and Interoperable Systems (DAIS 2020) -The IFIP WG 6.1 40th International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE 2020)


Wassila Belferdi
email: wassila.belferdi@univ-batna.dz

Lemnouar Noui

Ali Behloul
email: ali.behloul@univ-batna.dz

A Novel Cholesky Decomposition-based Scheme for Strict Image Authentication

Keywords: Strict authentication, Cholesky decomposition, Cryptographic hash function, Public key cryptosystem

With the increasing image falsification due to the easy access and use of image manipulation tools, image authentication techniques have seen considerable interest in protecting multimedia documents integrity and authenticity, it has been demonstrated to be a very powerful solution for ensuring the security of multimedia documents. The aim of this paper is to present a Cholesky decomposition based scheme for strict image authentication. To ensure the requirement of strict authentication where no changes are tolerated to the host image, the Cholesky decomposition properties are used beside the use of cryptographic hash function and public key cryptosystem. For the purpose of reducing the authentication data size, the diagonal of the Cholesky decomposition matrix is used instead of using the entire matrix.

The experimental results demonstrate that our technique is able to identify image tampering despite the minor modifications. In addition, the proposed scheme demonstrates its effectiveness in sensitive information systems. We review an application example in medical information security to ensure both integrity and authenticity. Our scheme can find a niche role in healthcare systems as an instrument for secure sharing and control of medical images.

I. INTRODUCTION

In recent years, the security of multimedia documents becomes a serious problem, especially with the increasing image falsifications provided by the easy access and use of image manipulation tools. Thus, new information security requirements become ever more urgent [START_REF] Haouzia | Methods for image authentication: a survey[END_REF].

Military, medical and quality control images must be protected against illegal use and unauthorized manipulations; which could affect the judgments based on these images. Thus, image authentication techniques has the ability to attain this requirement due to its effectiveness in several multimedia applications.

Generally, the image authentication schemes can be divided into tow main stages, stamping and verification stages. In the stamping stage the desired image to be protected is used to derive the authentication data that serves to verify the integrity of the image. At the verification stage, to decide whether the image is changed or not the consistence is evaluated between the authentication data calculated from the query image and the one calculated in the stamping stage [START_REF] Tiwari | Comparative evaluation of semi fragile watermarking algorithms for image authentication[END_REF]. Authentication schemes can be classified according to the service they provide into two main categories strict and selective authentication. In strict authentication schemes no modifications to the host image are accepted, even if only one bit is changed. It is used for several applications such as in law enforcement and medical image systems where no alterations in the image are allowed, while selective or content based authentication is used specifically when some image processing operations are allowed such as compression and filtering, it considers images as authentic when the content does not change [START_REF] Haouzia | Methods for image authentication: a survey[END_REF]- [START_REF] Rey | Un panorama des mthodes de tatouage permettant dassurer un service dintgrit pour les images[END_REF].

Strict image authentication methods can be further separated into two main categories according to the techniques that are used: methods based on conventional cryptography and fragile watermarking-based methods [START_REF] Haouzia | Methods for image authentication: a survey[END_REF], [START_REF] Doke | Digital Signature Scheme for Image[END_REF], [START_REF] Rey | A survey of watermarking algorithms for image authentication[END_REF]. The main difference between these two categories of techniques is that the former create a separate file to the authentication data, while the later embed it into the data to be authenticated [START_REF] Lou | Digital signature-based image authentication[END_REF].

In classical image authentication methods based on cryptography, an authentication data is computed from images using a hash function. The resulting hash is further encrypted with a secret private key of the sender and then appended to the image or stored in a confidential authority. During the verification process, the receiver computes the hash from the received image and compare it with the appended one [START_REF] Haouzia | Methods for image authentication: a survey[END_REF], [START_REF] Rey | A survey of watermarking algorithms for image authentication[END_REF], [START_REF] Lo | A novel reversible image authentication scheme for digital images[END_REF]. To address both the authentication and integrity problems, a diversity of schemes has been proposed for different applications.

In this paper, a Cholesky decomposition-based scheme for strict image authentication is proposed, the novelty of our proposed scheme is the profit from the Cholesky decomposition properties to detect any modification made on the original image despite there imperceptibility by the human eyes.

Unfortunately the Cholesky decomposition is not possible and unique if the decomposed matrix is not positive definite, to solve this problem the given image is firstly multiplied by its transpose then decomposed by the Cholesky decomposition to generate an authentication data. Using the hash function the principal diagonal is hashed. This latter will be encrypted with the public key cryptosystem Rivest, Shamir, and Adleman (RSA).

To detect any modifications, the authentication data is calculated from the given probe image and it is compared with the appended authentication data, depending on the consistence between the two sequences the image is considered as authentic or not. Experimental results show the efficiency of our proposed method under several attacks and show the ability to use the proposed scheme in sensitive information applications such as low enforcement, military and medical images share and control.

The rest of this paper is organized as follows. In section II we describe the cryptographic background. Section III includes the related works and briefly formulates the problem in the existing methods. The Cholesky decomposition which will be used in the proposed scheme is described in section IV. The detailed proposed scheme is described in section V, then experimental results including an example of application are presented in section VI and VII respectively. Finally, section VIII concludes our work.

II. CRYPTOGRAPHIC BACKGROUND AND TOOLS

Over the ages, Cryptography has attracted the attention as a tool to meet some of the information security requirements. Cryptography is the study of mathematical tools and techniques used in information security to provide a security service including confidentiality, data integrity, and entity authentication [START_REF] Menezes | Handbook of applied cryptography[END_REF]. Enabling significant information to be stored or transmitted over non-secure networks, so that only authorized recipients can read it [START_REF] Haouzia | Methods for image authentication: a survey[END_REF].

Message authentication techniques such as hash functions, private or public key systems and digital signatures are also used in image authentication and integrity systems [START_REF] Haouzia | Methods for image authentication: a survey[END_REF]. There are several tools that are used in image authentication algorithms. The most important one is based on the hash function which afford an effective and secure information processing [START_REF] Haouzia | Methods for image authentication: a survey[END_REF], [START_REF] Gauravaram | Cryptographic hash functions[END_REF].

A. Hash Function

In modern cryptography, the cryptographic hash function is considered as one of the most frequently used primitives [START_REF] Menezes | Handbook of applied cryptography[END_REF]. A hash function processes an arbitrary finite length input message to a fixed length output called the hash value or digest; in other words, it is the compact representation of the input message [START_REF] Haouzia | Methods for image authentication: a survey[END_REF], [START_REF] Menezes | Handbook of applied cryptography[END_REF], [START_REF] Gauravaram | Cryptographic hash functions[END_REF].

To achieve the security (cryptographic) requirement, a typically chosen hash function must satisfy at least, the following properties [START_REF] Gauravaram | Cryptographic hash functions[END_REF], [START_REF] Rogaway | Cryptographic hash-function basics: Definitions, implications, and separations for preimage second-preimage resistance, and collision resistance[END_REF]:

• For any given hash value y of H, it is "computationally impossible" to obtain a message m such that H(m) = y. It must be difficult to reverse H from y to get an m corresponding to y. • For any given message m, it is "computationally impossible" to obtain any message m such that m = m and H(m) = H(m ). • It is "computationally impossible" to obtain any two messages m and m such that m = m and H(m) = H(m ).

B. Rivest, Shamir, and Adleman (RSA) Public Key Cryptosystem

One of the most used public key cryptosystem is the RSA cryptosystem. It is used to provide both secrecy and digital signatures, The security of this cryptosystem is ensured by the integer factorization intractability [START_REF] Menezes | Handbook of applied cryptography[END_REF].

The RSA key generation, encryption and decryption algorithms are described as follows [START_REF] Menezes | Handbook of applied cryptography[END_REF]:

1) Key Generation Algorithm: Each entity generates an RSA public key and a corresponding private key and do the following:

1) Generate two large distinct random primes p and q each roughly the same size. 2) Compute n = p × q and φ(n) = (p -1) × (q -1).

3) Randomly choose the integer e such that gcd (e, n) = 1. 4) Using the extended Euclidean algorithm (see [START_REF] Menezes | Handbook of applied cryptography[END_REF]), Calculate the unique integer d,

1 ≺ d ≺ φ(n), such that e × d ≡ 1 [φ]
. The public key is (e, n) and the private key is d.

2) Encryption Algorithm: At the sender end, A encrypts a message m for the receiver B.

1) Obtain the authentic public key (e, n) of the receiver B.

2) Represent the message as an integer m in the interval

[0, n -1]. 3) Compute the encrypted message m c ≡ m e [n]. 4) Send m c to B.

III. RELATED WORK AND PROBLEM FORMULATION

The emerging evolution of image processing tools imposes new challenges for researchers to design effective authentication schemes. The existing schemes should be further improved to meet new requirements including the use largesize authentication data and tolerating more image processing operations without compromising security.

The compromise between these requirements leads to a new generation of image authentication schemes that use new techniques to combine the watermark and digital signature techniques [START_REF] Lou | Digital signature-based image authentication[END_REF].

Friedman and Gary in [START_REF] Friedman | The trustworthy digital camera: Restoring credibility to the photographic image[END_REF] proposed the concept of trustworthy digital camera for image authentication. A hash function is used to hash the content of the original image, then the encrypted result is attached with the original image and sent to the receiver. To obtain the original digest, a public key is needed to decrypt the signature. The authentication of the images is verified by comparing the decrypted digest and the newly created one. In [START_REF] Wong | A public key watermark for image verification and authentication[END_REF] a watermarking based image authentication scheme is proposed, that is suitable for several applications including medical images archiving and commercial image transaction. In this scheme, a private key is used to insert a watermark in the original image. To verify the image authenticity, anyone can use the public key to extract the watermark. If the watermarked image is modified the visual quality of the extracted watermark will be affected. However, compared to the secret key schemes, the public key scheme are more expensive computationally [START_REF] Wong | Secret and public key image watermarking schemes for image authentication and ownership verification[END_REF]. Ping et al. described in [START_REF] Wong | Secret and public key image watermarking schemes for image authentication and ownership verification[END_REF] a secure visible watermarking-based scheme for ownership verification and authentication. According to the user need, the watermark can be visible or invisible. This scheme is able to detect any modifications made on the image. To check the ownership, a valid user key is required. The disadvantage of this scheme is that the secret key will need to be transmitted from the image owner to the user through a secure channel. In [START_REF] Zain | Strict authentication watermarking with jpeg compression (saw-jpeg) for medical images[END_REF] a strict authentication watermarkingbased scheme for medical images is proposed, the watermark is generated by hashing selected area of interest and embedded outside the region of interest in the LSB bits.

For strict image authentication, digital signature-based schemes are more applicable than watermarking-based schemes. The authentication data generated by the hash function is sufficiently short, enabling the fast creation of the digital signature. In addition, the hash function is very sensitive to any modifications made on the images, which means that changing a single bit in an image may result a different hash value. Moreover, the authentication data used to identify the image is associated with it in a separate file, by the sequence, the embedding capacity of those techniques is higher than the embedding capacity of watermarking-based schemes [START_REF] Lou | Digital signature-based image authentication[END_REF].

IV. CHOLESKY DECOMPOSITION

The Cholesky decomposition of a positive definite matrix A is a decomposition of the form:

A = L × L t
In which L is upper triangular with positive diagonal elements and L t denotes the conjugate transpose of L, if A is positive definite; the decomposition is unique and there is only one lower triangular matrix L with strictly positive diagonal entries [START_REF] Higham | Analysis of the Cholesky decomposition of a semidefinite matrix[END_REF], [START_REF] Edlin | Correlated Parameters and the Cholesky Decomposition[END_REF].

A. Cholesky Decomposition Properties

The Cholesky decomposition is considered as an important tool in matrix computation because [START_REF] Edlin | Correlated Parameters and the Cholesky Decomposition[END_REF]:

1) It maintains correlated parameters; this means that the same information used to determine the value of one parameter is also used to partially conclude the value of the other. 2) The Cholesky decomposition destroy the relation between each parameter and their proceeding ones.

3) The Cholesky decomposition can indicate the correlation degree of its variables. 4) Compared with the other entries in a row, the size of the diagonal entries indicates the independence degree in a correlated variable.

This sort of result and properties can be potentially useful when considering the value of future research since this may give an indication of the degree to which variables are related.

V. PROPOSED METHOD Our main issue in the proposed scheme is to address both the authentication and integrity of images. The use of Cholesky decomposition properties, is the major difference that differentiates our proposed scheme from existing state of the art approaches; correlated parameters of the Cholesky decomposition allows the control of any modification arise the factorized matrix; this means that modification that changes the value of one parameter will also partially affect the value of the other. In addition, the parameters correlation degree is indicated using the size of the diagonal entries, providing the use of the principal diagonal instead of using the whole matrix.

To fulfill the several requirements of security, the robustness of the proposed signature scheme is achieved by using the hash function and RSA cryptosystem that encrypts the obtained sequence before attaching it with the host image.

The goal of our proposed scheme is to detect any modification in the digital images. If the image is untempered, the recalculated authentication data and the attached one will be equal. If the image is tampered, the two extracted and attached authentication data will not be equal and the image considered as non-authentic.

Our proposed scheme consists of two processes: authentication data generation process and authentication verification process, which are described in the following subsections.

A. Authentication Data Generation Process

Let the original image I be an image with the size of M ×N . Detailed steps are described as follows, as depicted in Fig ( 1): 1) Cholesky decomposition is unique only if the matrix to be factorized is a positive definite matrix. Thus, to overcome this problem and obtain a positive definite matrix from the host image I, it is firstly multiplied by its transpose. I m = I × I t 2) Using the Cholesky decomposition, the obtained positive definite matrix I m is decomposed into two Matrices L and L t .

I m = L × L t 3) Principal diagonal D of the L matrix is obtained. 4)
The hash function is applied on the obtained principal diagonal D. H = hash(D) 5) Using a private key, the hashed sequence is encrypted and attached with the original image. So, an authentication data sequence (digital signature) can be transmitted electronically with the original image.

B. The Verification Process

As shown in Fig [START_REF] Tiwari | Comparative evaluation of semi fragile watermarking algorithms for image authentication[END_REF], to verify if the received image has tampered or not, the receiver computes the authentication data from the received image. The authentication data that was appended with the received image is extracted and decrypted using the public key K p . The decrypted attached data and the calculated one are then compared. If the two extracted and attached authentication data are equal the image is considered as authentic, else the received image is not authentic.

VI. EXPERIMENTAL RESULTS

In our experiments, the testing programs are implemented using C + +. Besides the use of Cryptoc++ library to call SHA256 hash function and RSA cryptosystem.

The performance of the proposed Cholesky decomposition based scheme is tested using a wide variety of images in the CVG-URG database such as "Baboon", "Airplane", "Girl", "House", "Lena" and "Peppers" with the size of 256 × 256 pixels as shown in Fig [START_REF] Doke | Digital Signature Scheme for Image[END_REF].

In order to evaluate if the two authentication data sequences (the attached and recalculated) are equal or not, we use correlation metric as:

Corr(S c , S a ) = [(S c (i) -S c ) × (S a (i) -S a )] [(S c (i) -S c ) × (S a (i) -S a )] 2 (1)
Where S c and S a are the calculated authentication data and the attached one respectively. S c and S a are the mean of the calculated authentication data and the attached one respectively. Generally, the correlation can take a value between 0 and 1. If it is closer to 1, the two sequences are getting more similar. In our tests, if the correlation is equal to 1 the image is considered as authentic, in the other case the image is considered as tampered.

The peak signal to noise ratio (PSNR) is defined in Eq.( 2), in units of (dB), which may be used to evaluate perceptual distortion between the original and modified images.

P SN R = 10 log N × M × max(I(x, y)) 2 N -1 x=0 M -1 y=0 [I(x, y) -I (x, y)] 2 (2)
Where I is the original image, I is the modified image, and N , M denote the height and width of the image respectively. Generally, the larger the PSNR value is, the more invisible the distortions are.

To evaluate our algorithm, Table I, shows correlation values calculated between the authentication data attached to original images and the recalculated ones, to further demonstrate the advantages of our proposed method different attacks are performed .

As well seen from Table I, the proposed scheme proves its efficiency, without any modification made on the image the two sequences are similar and the correlation is equal to one.

In the other hand, changing only one bit from a pixel of the whole image changes the recalculated sequences and the correlation is different to one and closer to 0 despite the slight modification made.

For better illustration, results are also demonstrated under Salt and Pepper noise with a low variance equal to 0.0001, obtained results in Table I shows the effectiveness of the proposed method, where the correlation values remain low despite the PSNR high values greater than 46 (dB) which demonstrate that the slight modification made can't be perceptible by the human eyes but it can be detected using our proposed scheme. VII. APPLICATIONS Our proposed method can find a main application in healthcare systems, as an efficient tool for protecting sensitive information such as military and medical images, the secure sharing and control of those images is needed. These images must be protected against any incidental or/and malicious manipulations, which could affect the judgments based images, especially in sensitive information applications. To illustrate the efficiency of our proposed method in the medical images an example is shown in Table II.

From the obtained results of the correlation in Table II, we can conclude that any modification in the original images can be detected using our proposed scheme, even if the modifications can't be noticeable by the human (doctors) eyes.

VIII. CONCLUSION

A novel Cholesky decomposition based scheme for strict image authentication has been proposed. By exploiting the Cholesky decomposition properties beside the use of cryptographic tools our proposed scheme shows an effectiveness in detecting tampered images. The proposed scheme can find its application in several areas, where sensitive information need to be protected such as various medical imaging modalities and services (radiology, surgery, etc.). Experimental results have shown the suitability of the proposed scheme for enhancing robustness and the security of protected images to provide an authentication service. Our future works turns around using the Cholesky decomposition properties to detect and restore tampered areas besides the exploitation of medical images properties to embed the authentication data into the host image.

3 )

 3 Decryption Algorithm: B should use the private key d to recover the plain text m from the encrypted message m c . 1) Compute m ≡ (m c ) d [n].

Fig. 1 .

 1 Fig. 1. Authentication data generation process.

Fig. 3 .

 3 Fig. 3. Test images.

I

  CALCULATED CORRELATION BETWEEN THE APPENDED SEQUENCE S appended AND THE CALCULATED ONE S calculated AND THE PSNR VALUES CALCULATED BETWEEN THE ORIGINAL AND THE MODIFIED IMAGES.

	Attacks	-	Baboon	Plane	House	Lenna	Pepper
	Without	Corr 1	1	1	1	1
	attack
	Changing	Corr 0.2996	-0.0181	-0.0921	0.0332	0.3067
	One
	bit	PSNR	96.2956 96.2956 96.2956 96.2956 96.2956
		(dB)
	Changing	Corr 0.4038	-0.0955	0.2234	0.2353	-0.1673
	One
	pixel	PSNR	62.8536 53.2498 51.8934 62.1441 55.1575
		(dB)
	Salt and	Corr -0.0361	0.1674	-0.1193	0.3033	0.1881
	pepper
	variance	PSNR	50.2796 48.7065 51.9702 48.6796 46.678
	0.0001	(dB)


Wassila Belferdi
email: wassila.belferdi@univ-batna.dz

Ali Behloul
email: ali.behloul@univ-batna.dz

Lemnaouar Naoui
email: lemnaouar.naoui@univ-batna.dz

A blind dual color images watermarking based on IWT and sub-sampling

Keywords: blind detection, IWT, subsampling, Edge mask

With more color images being widely used in the Internet, embedding color watermark image into color host image is one of the most challenging issues in robust image watermarking, it is usually termed as dual color image watermarking. Based on integer wavelet transform (IWT) and sub-sampling, this paper proposes a blind dual color image watermarking scheme, which is different from some existing works using the binary or gray-level image as watermark. Firstly, the color host image is subsampled into four sub-images and each sub-image is transformed via IWT to obtain four LL sub-bands, we can find that there is a strong correlation between the LL sub-bands coefficients, this property can be explored for embedding and extracting watermark in a blind way. Experimental results, show that the proposed color image scheme has stronger robustness against most common attacks such as image compression, cropping, noising and scaling etc.

Introduction

In recent years, the copyright protection of digital contents from illegal use has been receiving more and more attention, digital watermarking is considered as a powerful solution arisen through this need [START_REF] Kekre | Robust Watermarking Scheme using Column DCT Wavelet Transform under Various Attacks[END_REF]- [START_REF] Su | A blind color image watermarking based on DC component in the spatial domain[END_REF]. The feature of digital watermarking is to allow for imperceptibly embedding watermark information in the original host image, once created the watermark can be detected or extracted for the purpose of owner identification or/and integrity verification of tested data [START_REF] Moon | Expert system for low frequency adaptive image watermarking: Using psychological experiments on human image perception[END_REF], [START_REF] Das | A novel blind robust image watermarking in DCT domain using interblock coefficient correlation[END_REF].

According to the processing domain of the host image, existing techniques of image watermarking may be divided into two categories: spatial and frequency domain watermarking [START_REF] Ingemar | Digital watermarking and steganography[END_REF]. The frequency domain technique is more widely used in digital watermarking, due to its stronger robustness, and its main feature is to convert the host image into frequency coefficients by using transformation methods such as DCT, DFT, DWT or IWT [START_REF] Ingemar | Digital watermarking and steganography[END_REF], [START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF].

According to whether the original data is required or not when extracting watermark, digital watermarking can be classified into blind detection and non-blind detection watermarking [START_REF] Su | A novel blind digital watermarking algorithm for embedding color image into color image[END_REF]. The blind detection means to extract watermark without the use of the original host image and the original watermark [START_REF] Ingemar | Digital watermarking and steganography[END_REF], [START_REF] Su | A novel blind digital watermarking algorithm for embedding color image into color image[END_REF]. On the contrary, the non-blind detection requires the original host image or the original watermark [START_REF] Ingemar | Digital watermarking and steganography[END_REF]. Generally, the latter one has stronger robustness than the former one, but it is not realistic that need the original data to extract watermark in many applications. Hence, the blind detection watermarking technology has been recently receiving more attention.

Generally, the existing image watermarking schemes use binary or gray-level image as watermark, and many of them belong to non-blind watermarking methods. It is a challenging problem to design a blind color image watermarking scheme [START_REF] Su | Color image blind watermarking scheme based on QR decomposition[END_REF]. Among these existing dual color image watermarking techniques, Chou in [START_REF] Chou | Embedding color watermarks in color images[END_REF] propose to embed color image watermark in color image, which was performed in the spatial domain and had the feature of simplicity in the computation. In [START_REF] Lu | Robust digital image watermarking based on subsampling[END_REF] a robust digital watermarking scheme using subsampling is proposed, a binary watermark image is embedded into the DCT coefficients. Motivated by the above discussion, a blind watermarking method based on IWT and subsampling is proposed for embedding color image watermark into color host image in frequency domain.

Thus, we are interested in three challenges: The first one is to use the integer wavelet transform (IWT), which can map integer to integer without the rounding error, and can further concentrate the energy of each sub-image to obtain a good imperceptibility. The second one is to embed color image watermarking into color host image. This is motivated by the fact that compared with gray level watermarking; digital color image has more amounts of data. The last but not the least is that the proposed watermarking is blind detection [START_REF] Su | A novel blind digital watermarking algorithm for embedding color image into color image[END_REF], [START_REF] Su | A blind dual color images watermarking based on IWT and state coding[END_REF].

In this paper, the proposed IWT and subsampling algorithm is very different to the method in [START_REF] Tsai | DCT and DWTbased image watermarking by using subsampling[END_REF], where a blind sub-sampling based watermarking scheme has been investigated for digital images. Hence, in this paper, the watermark will be embedded into LL sub-band coefficients according to an edge mask. Firstly, an energy compaction region is obtained by IWT after subsampling the color host image. And then, the watermark is embedded into the LL neighboring sub-bands coefficients.

The rest of the paper proceeds as follows: Sect.2 introduces the technique of IWT and sub-sampling technology. The detailed watermark embedding and extracting procedures are presented in Sects.3 and 4, respectively. Subsequently, Sect.5 provides the experimental results. Finally, we draw our conclusion of this paper.

Preliminary

Integer Wavelet Transform (IWT)

The existing watermarking algorithms based on the traditional wavelet transform are not suitable for color image due to the disadvantages of computational complexity and rounding error [START_REF] Su | A blind dual color images watermarking based on IWT and state coding[END_REF]. It uses non-integer filter, which produces noninteger transform coefficients [START_REF] Salomon | Data compression: the complete reference[END_REF].

Since the color image has great amount of information and its pixel values are integers, the integer wavelet transform can map the pixel value to integer without any rounding error see [START_REF] Salomon | Data compression: the complete reference[END_REF], [START_REF] Su | Embedding color watermarks in color images based on Schur decomposition[END_REF] and the bibliography therein.

Image sub-sampling

Since the pixel values of any image have a good correlation with their pixel values neighboring, the sub-sampling allows as mapping the pixel values of any image into four highly correlated sub-images.

Given the image V of size N×M, N = 0... n-1, M=0,..,m-1, the sub-sampling process is as follows:

V 1 [k 1 ; k 2 ] = V [2n; 2m]; V 2 [k 1 ; k 2 ] = V [2n+1; 2m]; V 3 [k 1 ; k 2 ] = V [2n; 2m+1]; (1) V 4 [k 1 ; k 2 ] = V [2n+1; 2m+1]; For k 1 = 0,…,N/2-1,k 2 = 0,…,M/2-1, V i [k 1 ,k 2 ],
i={1,2,3,4} are four sub-images obtained by subsampling Fig. [START_REF] Kekre | Robust Watermarking Scheme using Column DCT Wavelet Transform under Various Attacks[END_REF]. Since the sub-images V i 's are highly correlated, it is expected that the IWT coefficients of different sub-images are approximately equal, i.e. Y i ≈Y j , for i ≠ j except edge, where Y i and Y j denote that the IWT of the subimage V i and V j [START_REF] Lu | Robust digital image watermarking based on subsampling[END_REF], [START_REF] Tsai | DCT and DWTbased image watermarking by using subsampling[END_REF].

Edge masking

As it discussed, the IWT sub-images have approximately same coefficients at the same spatial location except edge areas [START_REF] Moon | Expert system for low frequency adaptive image watermarking: Using psychological experiments on human image perception[END_REF], [START_REF] Lu | Robust digital image watermarking based on subsampling[END_REF], [START_REF] Tsai | DCT and DWTbased image watermarking by using subsampling[END_REF]. To deal with this problem, the proposed method uses an edge mask as in Fig. [START_REF] Kasmani | A prefiltering method to improve watermark detection rate in DCT based watermarking[END_REF]. It is used to consider the edge of local image characteristics [START_REF] Moon | Expert system for low frequency adaptive image watermarking: Using psychological experiments on human image perception[END_REF]. The edge mask is constructed according to the pixel-wise relationship between the selected sub-band and neighboring two sub-bands.

Once we select a sub-image to embed the watermark, we have to select neighboring subimages to compare for later watermark extraction. Using the edge mask we select just a horizontal or vertical neighboring sub-image for comparison purpose.

Watermark embedding

Firstly, the 24-bit P×Q color watermark image W is divided into R, G and B components; every component is encoded to 1D sequence, then in order to further remove the space correlations between the watermark coefficients and enhance the robustness of watermarking the 1D sequence is randomly permuted by a secret key K.

Next, the 24-bit M×N color host image H is divided into R, G and B components, every component is decomposed into four sub-images according to Eq.( 1), each of the four sub-images is transformed via IWT to obtain four LL i 's sub-bands, one of which is selected for embedding a watermark. Then, one pair of coefficients from two different sub-images situated in the same LL sub-band location is used to insert one watermark value. According to the mask the LL j sub-band values are modified according to the following equation:

LL Mask(i) =LL i +αW i (2) Where LL i is the chosen sub-band to compare with, Mask(i)={H,V}, H and V are horizontal or vertical neighboring respectively, the positive constant α is known as watermark strength control variable, the choice of α is a tradeoff between image distortion (watermark invisibility) and detection accuracy (robustness).

Once the watermark is embedded, every subimage is firstly transformed by the inverse IWT, and then, the inverse sub-sampling is applied to obtain the watermarked image H'.

Embedding steps are described in Fig.

Watermark extraction

The procedure of watermark extraction is the inverse operation of the embedding process Fig. [START_REF] Das | A novel blind robust image watermarking in DCT domain using interblock coefficient correlation[END_REF] The watermarked image H' (probably attacked) is firstly sub-sampled into four sub-images and each of them is transformed via IWT. And the same watermark insertion order sequence is required to select the chosen sub-band LL i and two neighboring LL j and LL k sub-bands. To recover the watermark Eq.( 3) is performed:

W i ' =(LL * Mask(i) -LL * i )/α (3) Where W i
' is the extracted watermark value, Mask(i)={H,V} is the edge mask value, LL * Mask(i) is the neighboring value of the watermarked image, chosen according to the edge mask value. LL * i is the chosen sub-band to compare with. Then the next process is to inverse the permutation for extracting a visually recognizable watermark.

Experimental results

Five 24-bit color images in the CVG-URG data base with size of 512×512 are selected as original host image, and two 24-bit color images with size of 64×64 are used as original watermarks Fig( 6). The strength of watermark α=0.05 chosen according to a tradeoff between image distortion and robustness as it shown in Fig. [START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF], in other words when the strength of watermark α increase the invisibility of watermark decrease and conversely. For the imperceptible capability, we make use the peak signal to noise ratio (PSNR) defined in Eq.( 4) in units of dB, where H is the original image, H' is the watermarked image, and N, M denote the height and width of the image respectively.

(4)

In general, if the PSNR value is greater than 35 dB the perceptual quality is acceptable, that's mean that the watermark is invisible to human eyes [START_REF] Moon | Expert system for low frequency adaptive image watermarking: Using psychological experiments on human image perception[END_REF], [START_REF] Su | A blind dual color images watermarking based on IWT and state coding[END_REF].

Besides, in order to measure the robustness of watermark, we use the normalized correlation (NC) between the original watermark W and the extracted watermark W', which is shows as follows.

(5)

Where P and Q denote the row and column size of the watermark image. Generally, the NC can take a value between 0 and 1. If the NC value is closer to 1, the extracted watermark is getting more similar to the embedded one, which means that the watermarking has strong robustness. In general, the watermark may be efficient if the NC is more than or equal to 0.750, conversely may be inefficient [START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF].

In this section, the invisibility and robustness of the proposed method are proved; by comparing it with the performance of the algorithms in [START_REF] Chou | Embedding color watermarks in color images[END_REF] and [START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF].

Invisibility test

As can be seen from Table .(1), the embedded watermarks are visually transparent and the watermarked images have high values of PSNR. Beside, most of the extracted watermarks remain high quality without any attacks performed on the watermarked images.

Moreover, the proposed algorithm is compared with the dual color image watermarking algorithm in [START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF] and [START_REF] Chou | Embedding color watermarks in color images[END_REF], It can be seen from Table .(1) that the two algorithms have higher PSNR values, but the proposed method is the less complicated one. Compared with the exiting method [START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF], the extracted watermarks by the proposed method have better quality, which also prove that the proposed method has well invisibility.

Robustness test

In order to show the robustness of the proposed method, various attacks such as compression, cropping, adding noise, scaling and rotation are performed on the watermarked image. The obtained results can be seen in Table .(2) and (3).

Notice the high quality of the extracted watermark especially under the cropping, salt and peppers noise and compression attacking; this proposed method has well robustness obtained by the use of image sub-sampling, and the failure of extraction after rotation with large angles. The failure in this case is due the large changes of the watermarked image caused by the rotation. Table 2. The performance comparison between proposed algorithm and the proposed one in [START_REF] Chou | Embedding color watermarks in color images[END_REF]. Table 3. The results of extracted watermark (NC) under different attacks

Conclusion

In this paper, a blind watermarking algorithm for embedding color image watermark into color host image is proposed. Its main features is to transform the host image via IWT after sub-sampling it, obtained sub-bands are used to embed the watermark, exploiting the advantage of high correlation between LL sub-band coefficients. Experimental results have shown that the proposed algorithm not only guarantees the invisibility of watermarking but also has strong robustness against the operations of common image processing, and its performance outperforms other methods considered in this work.

Figure 1 .

 1 Figure 1. Sub-sampling image into four sub-images.

Figure 2 .

 2 Figure 2. Selecting neighboring sub-images (two white blocks enclosed in dashed line are neighboring sub-images of gray block sub-image).

  Fig.(3) shows an example of embedding procedure, where (a)-(c) represent the LL sub-bands of Y 1 and two neighboring LL sub-bands of Y 2 and Y 3 respectively.

( 4 )Figure 3 .Figure 4 .

 434 Figure 3. Watermark embedding example:(a) LL 1 sub-band of Y 1 ,(b) LL 2 sub-band of Y 2 , (c) LL 3 sub-band of Y 3 ,(d) the edge mask, (e) the modified coefficients.

FigFigure 5 .

 5 Figure 5. Watermark extraction process.

Figure 6 .

 6 Figure 6. Original host images: (a) Lena, (b) House, (c) Baboon, (d) Splash, (e) Peppers, (f) watermarks.

Figure 7 .

 7 Figure 7. Tradeoff between watermark invisibility and detection accuracy curve, (Red) for NC values, (Blue) for PSNR values.

Table 1 .

 1 The performance comparison between proposed algorithm and the proposed one in[START_REF] Su | Embedding color image watermark in color image based on two-level DCT[END_REF].

		Su[7]	Proposed method
	Watermarked	Extracted	Watermarked	Extracted
	image	watermark	image	watermark
	PSNR (dB)		PSNR (dB)
	48.6235	0.9997	38.9599	0.9995
	40.3840	0.9960	38.4909	0.9999
	46.4410	0.9984	39.1033	1.000
	43.4647	0.9983	38.0118	0.9999
	45.5024	1.000	39.2698	1.000
	46.4709	0.9969	39.1197	1.000