随着信息技术的高速发展和应用,当今社会已经高度信息化。在人们的工作和生活等方方面面,每时每刻都有信息产生,且并快速和广泛地传播。信息的安全问题成为了个体,机构以及国家所面临的重要问题。从保护的对象考虑,信息安全主要分为信息内容的安全性和信息传播机制的安全性。本文研究的对象是信息传播机制。本文从事件驱动的角度出发,把信息传播机制抽象为离散事件系统,再用自动机和Petri网来建立图形化的数学模型。在此模型基础上进行分析,控制和优化。本文的具体工作有两个部分,分别是事件不透明性研究和状态不透明性研究。本文的第一部分主要研究了事件不透明性。现实生活和工作普遍存在一种隐私保护现象,比如个人的私人行为,企业的重要决策或者国家的战略部署等都不希望被各自的竞争对手或者外围世界所知晓。在第四章,这些私人行为,重要决策和战略部署以及其他的需要隐藏的事件被抽象成为隐匿事件集合。而这些行为属于的离散事件系统则被描述成了自动机。在此基础上,我们提出了事件不透明性概念。考虑到私密信息的时效性,相应地提出了事件k步不透明性。并且通过构造包含隐匿信息的特征自动机后与系统原型自动机做集合关系运算的算法来验证此需要隐匿的事件集合是否满足不透明性。第四章的主要贡献是,在自动机模型下提出了事件不透明性和k步事件不透明性两个概念,并给出了相应的验证算法。同时从概念的完备性角度出发,在自动机模型中已经存在语言层次的不透明性和构造元素层次的状态不透明性概念的背景下,作为自动机另外一个构造元素的事件,其不透明性概念的提出有一定的意义。本文的第二部分研究的内容是,基于一种特殊Petri网的状态不透明性验证算法。在已有的Petri网模型中的不透明性验证算法中,研究人员都是考虑的通用Petri网模型,并且用遍历的方法来验证网模型是否满足不透明性。在Petri网中存在着一类非循环网,它们的可达状态和网的状态方程解之间满足充分必要性。在此类网中,人们可以用求解状态方程的方法来降低遍历法所带来的巨大工作量。本文所研究的Petri网被称之为加标Petri网,即变迁的发生如果可以被观测,则会在标记集合中的可观元素标记。如果不可以观测,则用不可观测符号标记。出于实际系统中,不希望出现不可观的事件无限循环发生的可能性,本文认为这一类系统可以不可观部分为非循环网的部分可观Petri网所建模。在分析此类网的状态不透明性时,本文通过基本标识的方法来构造部分可观的Petri网的“观测器”,再通过网络的状态方程来标识出可达状态。根据不同类型的所需隐匿的标识集合,设计相应的验证算法。第五章的主要贡献是,在不可观子网为非循环网的Petri网模型下,分别针对枚举型和线性约束型所需隐匿的状态集合,设计相应的验证算法。与之前的验证算法比较,此类算法不需要进行状态枚举,大大地提高了验证效率。总体来说,论文的主要贡献是提出了基于自动机模型的有关事件的不透明性概念和针对不可观子网为非循环网的Petri网模型中状态不透明验证算法,首次利用基本标识来进行算法验证。