Security Infrastructure Verification of Library Information Grid Based on ePr/T net

INTRODUCTION

By constituting fully shared resource integration through high-speed Internet with the calculating resources distributed at different places, grid provides a sort of resource capability for high-performance calculation, management and service (Chard et al., 2009). In the grid computing environment, all sorts of resources are dynamically linked to the internet and can be used conveniently by users (Foster et al., 2001). Therefore, the grid computing environment must have the capability to resist the illegal attack and encroachment and guarantee the security of information.

Grid as a new resources management form of next-generation internet, it can provide a secure, reliable and efficient operating environment for on-demand digital library (Thomasr et al., 2007). Because of the grid nodes are located in different regions, these will be key problem that how to safely share data between the resources nodes of the digital library (Yang and Hu, 2005), how to ensure the integrity of sharing data. Grid security includes grid system security, data transmission security, information storage security. Therefore, we must adopt advanced security technology and need to identify data and information which to be sent and to be received online between the two sides, in order to ensure the security, integrity, reliability and transaction non-repudiation of all transmission of information.

The use of Grid Security Infrastructure of Library Information (GSI-LI) to build a digital library platform that enables secure sharing of library resources. All nodes of libraries to the library resource agent (Agent) supplied data resources (Candela and Castellil, 2005) so this will form local management domain, which has regional trading security policy and name of data resources. On this basis, a virtual share trading field is built, a virtual library of resources and global security strategy are provided and the transaction is managed by agent.

The project of digital library information provides safety authentication and safety communication by putting forward GSI-LI. Based on the system of public key encryption, GSI (Foster et al., 2002) adopts X.509 authentication and SSL (Secure sockets layer) communication protocol and expand them in certain degree. The main security technology method includes safety authentication and mutual identification of safety identity, communication encryption, private key protection (Zhang and Wang, 2008), commission and single dot logging on, etc. Grid is prevalent in recent years; there are some literatures to study why, in the attempt to better satisfy the user requirements, develop a sexrvice-oriented digital library infrastructure on the grid. The study describes and compares the two systems by focusing, in particular, on that part of the architecture that controls and supplies the necessary features for creating and managing digital libraries, but the security infrastructure of OpenDLib is not be analyzed systemically by model checking. Barbosa et al. (2007) investigated the benefits and drawbacks of a strategy for verification of occurrence graphs that uses computational grids as infrastructure for distribution. This investigation was performed using a tool set for the Petri net formalism and a computational grid for bag-of-tasks applications.

Cholia and Porter (2008) analyzed the various vectors of information being published from sites to grid infrastructures and analyze the risks and potential threat models posed by the publication and collection of such data. We also offer some recommendations and best practices for sites and grid infrastructures to manage and protect sensitive data. But there are few people setting foot in GSI’s assignment submission and implementation procedure in grid environment using ePr/T net. EPr/T net is a kind of advanced Petri net, it can depict the system’s dynamic characteristic concisely from the process angle completely, it has great advantage on describing some important activities and phenomena such as concurrence, conflict and synchronization, etc. The established model not only can achieve the macro-control effect by ePr/T, but also can feed back every detail of the flow with reference to microcosmic aspect. This study applies ePr/T net theory in the description of GSI-LI, it could make this complicated process transparent toward customers, therefore it is very useful for the improvement of grid structure.

BASIC CONCEPTION

Here, we only introduce several conceptions correlating with the study close, other Petri Nets terms in the literature (Murata, 1989).

Definition 1: The condition for ' = (S, T; F, D, V, A_P, A_T, A_F, M_O) to constitute Pr/T net:

Definition 2: Murata (1989): Nonzero m = |S| dimensional row vector V = (V₁,V₂,...,V_m) is called S-invariable of Pr/T net, if:

viz., v_i·R(M) = v·R(M₀), among it, M, M₀ are column vectors.

Definition 3: A ePr/T net is a quintuples called EPR = (Pr/t;M,R), among it:

•	R is a flow of Pr/T, elements in R are called inhibit arc. , a section with a small circle in the end is used to describe inhibit arc. If (x,y)R, then x is y’s inhibit place

Definition 4: The firing rule of transition in a ePr/T net called EPR = (S, T, F, M, R) is:

then t is enabled under the marking M.

Definition 5: Murata (1989). The condition that |S|x|T| step matrix C is the incidence matrix of Pr/T net is: C’s matrix element C_ij is demonstrated by the formula below:

Among:

it i = 1, 2,þ,|S|; j = 1, 2,þ,|T|;

and:

if S_i∉^Ct_j,

then:

A_F(S_i, T_j) = <>;

if s_i∉^Ct_j, nA_F(t_j, s_i) = <>

Definition 6: Murata (1989). If V = (v₁,v₂,þv_m) is a S-invariable of Pr/T net, then v·IC = θ_T, among it, • is matrix multiplication, θ_T is n = |T| dimensional zero row vector (IC is an incidence matrix of Pr/T net).

THE DESCRIPTION OF ASSIGNMENT SUBMISSION AND IMPLEMENTATION PROCEDURE ABOUT GSI-LI

The description of assignment submission and implementation procedure about GSI-LI as follows:

MODELING AND ANALYSIS BASED ON EPr/T NET

Modeling based on ePr/T net: In this assignment submission, it involves the flow of many kinds of resources and the flowing process is relatively complicated. If singly seeing general depicting graph, we can only find some main flows, whereas some details can not be mastered, in view of the inhomogeneous flowing resources, here we model based on Pr/T net to solve this problem (Fig. 1).

Fig. 1:	ePr/t net based on GSI’s assignment submission and implementation procedure

Because of too many transitions and places, enumeration is not given here. Connotation and features of the main places and transitions in this process can be concluded as follows:

From Fig. 1, we can find the flowing procedure of every sort of initial resource and grasp every detail in submitting assignment from the microcosmic angle. At first, t1 is fired, viz.,s1 sends C and b to s2, after s2 receives resources, t2 could be fired, viz., CA identification center returns certificate c which has been signed and public key a to the user and saves the private key into s3. The subsequent firing procedure is almost the same, so here it is unnecessary to give the similar narration.

Model analysis based on S-invariable: As ePr/T net is different from elementary Petri net, its resources are in different variety, so the reachability can’t be analyzed by the matrix equation. Here, S-invariable is adopted to analyze reachability.

The original meaning of S-invariable (Murata, 1989) is to seek for the trace of resources and the reachability of certain state marking could be verified according to the definition of S-invariable. First of all, S-invariable should be calculated and incidence matrix of the ePr/T net could be written out (Table 1).

Table 1:	Incidence matrix of the ePr/T net based on GSI-LI’s assignment submission and implementation procedure

According to Table 1, if resource categories of every row and column are ignored and the numbers of resources are only paid close attention to, then the following incidence matrix with 23 rows and 28 columns could be written out. The incidence matrix of ePr/t model as:

According to definition 6, v vector can be calculated, here the numbers of rows and columns of the matrix are with big amount, as majority of element are zero, so the calculation is not very complicated, 23 dimensional row vector v = (1, 1, 1þ, 1) is obtained by calculation, on the basis of v·R(M) = v·R(M₀), it can be verified whether v is a S-invariable. The initial marking is M^T₀ = (<b, c, d, e>,<a>,<>,þ<>), if M₀[t₁>M₁>, M^T₁ = (<e, d>, <a, b, c>, <>, <>). Through the verification: v satisfies the formula above, viz., v is a S-invariable.

According to the quality of S-invariable, the reachablity of any one of state markings could be verified. For the model based on ePr/T net, assignment can be verified whether it is submitted and finished ultimately. If the ultimate state cannot be reached, then the system could be directly inspected, which promotes the work efficiency.

In this model, the ultimate state M'^T = (<>, <>, <b>, þ<m, d, k>), can be verified that it is reachable according to the methods descried above; meanwhile, it also verifies the correctness of the model based on ePr/T net.