投稿论文范文

基于XYZ/E的CA认证系统描述与求精作者11，2，作者22，4，作者33（1.xx学院 xx系，江苏无锡 214063；2.xx大学 xx学院，江苏苏州 215006；3. xx大学xx中心，深圳518053；4.xx大学 xx学院，重庆 400047）摘要：时序逻辑语言XYZ/E在统一的逻辑框架下既能表示静态语义又能表示动态语义，可以实现从抽象描述到可执行程序的平滑过渡。

本文建立了CA认证系统组件模型，对CA和RA组件用XYZ/E进行了抽象描述。

关键词：XYZ/E；CA；RA；组件The Description of CA Attestation System Based on XYZ/ELIU Jian-yun1，2，ZHANG Guang-quan2，4，RONG Mei3(1.Wuxi V ocational Institute of Commercial Technology, Information Engineering Department, Wuxi 214063,China, 2.School ofComputer Science and Technology, Soochow University, Suzhou 215006, China, 3.ShenZhen Tourism College，Jinan University, Shenzhen 518053, 4.School of mathematics and Computer Science, Chongqing NormalUniversity, Chongqing 400047,China )Abstract: The temporal logic language (TLL) XYZ/E can represent both dynamic semantics and static semantics under a unified logical framework, carry out the smooth transition from the abstract specification to executable program. This paper builds up the Certification Authority attestation system component model, and abstract describes the CA and the RA component using XYZ/E.Keywords: XYZ/E; Certification Authority; Registry Authority; component.1 引言XYZ系统是由时序逻辑语言XYZ/E及一组基于该语言的CASE工具集组成，其目标是提高软件可靠性和软件生产率。

时序逻辑语言XYZ/E是面向软件工程设计的，以适应软件工程如下领域：图形程序设计、分布式和基于共享存储器的并发程序设计、并发进程与数据模块相结合意义下的面向对象程序设计，在编译的编译、源代码到源代码的转换中起中间语言的作用[1]。

它能在统一的逻辑框架下即可以表示静态语义又可以表示动态语义，克服了CSP、Z等形式化工具只适合描述其一的不足，因此，非常适合描述软件体系结构。

在文献[2]中介绍了采用逐步求精方法对CA认证系统体系结构整体抽象描述，本文将在它的基础上对该认证系统中的CA和RA两个组件做进一步详细的描述。

2时序逻辑语言XYZ/EXYZ/E是基于Manna-Pnueli线性时间的时序逻辑语言，它将时序逻辑算子融进程序设计语言之中，使其既是一个逻辑系统又是一个程序设计语言[3]。

2.1 基本语言成分XYZ/E的基本语言成分是条件元，有两种形式：LB=y∧R=>$O(v1，…，v k)=(e1，…，e k)∧$OLB=z (1)LB=y∧R=>@(Q∧$OLB=z) (2)式中“=>”表示蕴含；R和Q表示一阶逻辑公式，分别称为条件元的条件部分和动作部分；y和z分别表示条件元的定义标号和转出标号；符号＠为一阶逻辑算子，可以是下一时刻算子$O或最终时刻算子◇。

形式(1)条件元定义了程序相邻状态之间的转换关系，用于* 作者简介：作者1（1972-），硕士，主要研究方向：软件体系结构；作者2（1965-），男，博士、教授，主要研究方向：形式化方法、软件工程；作者3（1966-），博士、副教授，主要研究方向：软件工程。

基金项目：中国科学院计算机科学国家重点实验室开放课题（SYSKF0303）；重庆市教委科学技术研究项目（040803）；江苏省计算机信息处理技术重点实验室开放课题。

描述动态语义；形式(2)条件元表示程序抽象规范，用于描述静态语义。

2.2 通信命令XYZ/E提供两种通信命令：输入命令：LB i=y∧R=>ChNm?x∧$O LB i=w输出命令：LB i=y∧R=>ChNm!z∧$O LB i=w其中，“ChNm”是通道名，x是变量，z是表达式。

“ChNm?x”表示由通道ChNm接收信息送入变量x中，数据与x的类型必须一致；“ChNm!z”表示由通道ChNm送出表达式z 的值，数据与z的类型必须一致。

3 CA认证系统组件模型[4]由于电子邮件、电子商务、资源发布等Internet和Intranet应用的发展，经常需要在大型异种开放网络中不明身份的实体之间进行通信。

为了在这种环境中提供机密性、完整性、不可抵赖性和安全性等服务，通常将公开密钥与其拥有者之间的信息绑定到一条电子记录上，称为数字证书，简称证书。

此证书由一个可信任的权威机构签发，此权威机构称为CA （Certification Authority）[4]。

CA认证系统从逻辑上可以分成三层，分别是用户层CL（Client Layer），应用层AL（Application Layer）和系统层ML（System Layer）,其结构如图1所示。

其中应用层处理有关证书申请、验证、撤销、查询等事务；系统层则处理证书签发、密钥管理等事务。

图1 CA认证系统组件模型3.1基本组件在认证系统中主要包括根CA自身管理、证书管理、密钥管理和交叉认证等组件。

根CA自身管理包括根CA的初始化和根密钥更新；证书管理主要包括证书申请、证书签发、证书更新、证书撤销和证书下载；密钥管理包括密钥更新和密钥撤销；交叉认证包括为其他CA认证系统签发交叉证书和向其它CA认证系统申请交叉证书。

3.2形式化描述认证系统通常由CA、RA（Registry Authority）和证书库组成。

证书机构（CA）是用于证明数字证书本身具有真实性的重要实体，是被一个或者多个用户信任的主体，可以创建、分配和管理公钥证书。

注册机构（RA）负责确认主体的身份和验证主体确实有权利拥有在证书申请中所要求的值[5]。

数字证书库主要基于LDAP构建，轻量目录访问协议LDAP （Lightweight Directory Access Protocol）作为一个开放的、独立于任何厂商的标准，为目前在分布式应用系统和服务中所要求的信息集中存储和管理提供了一个可扩展的结构[6]。

●CA和RA之间是采用管道-过滤器风格构建的。

过滤器sender调用SeInput过程输入，调用SeOutput过程输出。

Sender= =[ LB=m => SeInput∧$O LB=m1;LB=m1=> Seprocess∧$OLB=m2;LB=m2=> SeOutput∧$OLB=y]SeInput= = [LB=n=>connector.source∧$OLB=RETURN]SeOutput= = [LB=n=>connector.sink∧$OLB=RETURN]管道connector有输入端口source和输出端口sink.connector= =[source; sink]%ALG[%PROS[PROSSource(%CHN ASYN ch1(*,soprocess1:NM):String;%CHN ASYN ch2(soprocess2:NM,*):String;)= =[%ALG[LB=START=>$O(LB=y0);LB=y0=>Protocol.send;] ]PROSSink(%CHN ASYN ch3(*,siprocess1:NM):String;%CHN ASYN ch4(siprocess2:NM,*):String;)= =[%ALG[LB=START=>$O(LB=m0);LB=m0=>Protocol.receiver;] ]%ALG[LB=START=>y0;LB=y0=>%O(sender1=PROSSource{1}∧receiver1=PROSSink{1}∧LB=y1);LB=y1=>|| [ sender(%CHN ch1(*,receiver1) | ch1(*,soprocess1);%CHN ch2(receiver1,*) | ch2(soprocess2,*);receiver(%CHN ch3(*,sender1) | ch3(*,siprocess1);%CHN ch4(sender1,*) | ch2(siprocess2,*))]●CA组件在CA组件的多个功能中最重要的是证书签发。

该项功能具体实现过程为：CA服务器从证书申请表中逐条读取已经审核过的证书申请信息，对应每一条证书申请信息，CA首先为申请人生成RSA密钥对，并将私钥加密后写入密钥库的密钥表中；而后CA为申请人生成证书申请，接着CA为该申请人生成证书，并将证书保存在证书库的证书表中；同时将证书的一个副本发布到LDAP目录服务器；之后通过RA服务器向用户发送一封电子邮件，通知用户证书已经发行成功，并且把证书序列号告诉用户；最后将该条证书申请信息从证书申请表中删除。

%PROS[%PROSCAcountersign(%CHN ASYN c1(*,process1:NM):String;%CHN ASYN c2(process2:NM,*):String;)= =[%ALG[%LOC[appmessage,pubkey,prikey,tellmessage,delmessage :string;x,y,m,n,o,p:string;certino:integer;]LB=START=>$OLB=k1;LB=k1=>$O appmessage=0∧$OLB=k2;LB=k2∧c2 ?=>$OLB=k3;LB=k2∧¬c2 ?=>$OLB=k1;LB=k3=>$O c2 ? appmessage∧$OLB=k4;LB=k4=>$O x=appmessage∧$OLB=k5;LB=k5=>create_key(%iop pubkey|pu; %iop prikey|pr);LB=k6=>$O y=prikey∧$OLB=k7;LB=k7=>encrpt_key(%iop y|epri);LB=k8=>$O c1 ! y∧$OLB=k9;LB=k9=>create_certi_app(%iop x|cap);LB=k10=>$O(m=x∧LB=k11);LB=k11 =>create_certi(%iop m|cc);LB=k12=>$O n=get_certino(m)∧$OLB=k13;LB=k13=>$O o=copy_certi(m)∧$OLB=k14;LB=k14=>$O c1 ! m∧$OLB=k15;LB=k15=>$O c1 ! o∧$OLB=k16;LB=k16=>$O tellmessage=1∧$OLB=k17;LB=k17=>$O tellmessage=tellmessage+n∧$OLB=k18;LB=k18=>$O c1 ! tellmessage∧$OLB=k19;LB=k19=>$O delmessage=1∧$OLB=k20;LB=k20=>$O delmessage=delmessage+appmesssage∧$OLB=k21;LB=k21=>$O c1 ! delmessage∧$OLB=k22;LB=k22=>$OLB=k1;] ] ]●RA组件在RA组件中本文将对其中的证书撤销功能进行形式化描述，其实现过程如下：用户访问RA服务器主页，填写申请人信息、PIN值及要撤销证书的序列号，选择撤销原因，证书撤销申请表单提交给RA服务器。