随着互联网的广泛使用，保护敏感和机密信息的系统的正确性验证日渐成为一个重要的问题。许多保护机密信息的协议使用到了随机机制，用于混淆秘密信息和公开信息之间的联系。典型的例子有密码学家就餐协议，匿名通信协议Crowds、洋葱路由Onion Routing、 Tor协议和Freenet等等。这些协议的另外一个共同点是在其网络活动中往往存在多个实体，它们之间的交互呈现并发行为。概率行为和非确定性行为的同时存在使得并发系统安全问题的验证变得十分复杂。　　本文致力于研究验证概率并发系统差分隐私性质的新技术。差分隐私是来源于统计数据库安全领域的隐私保护概念，如今也被广泛运用于其他多种计算模型中。本文使用差分隐私概念作为并发系统隐私保护程度的衡量标准。　　论文的第一部分运用基于Milner的CCS的概率进程代数对并发系统的差分隐私性质进行模块化分析。我们证明了非确定性选择算子、概率选择算子、限制算子和一个受限的并发组合算子是安全的，即，使用这些算子进行组合不会损害整个系统的隐私等级。我们运用模块化分析方法证明了扩展的Crowds匿名通信协议的一个隐私保持性质。　　论文的第二部分考虑应用互模拟技术-并发理论领域最核心的技术之一-刻画差分隐私行为。我们借用起先运用于基于动作花费的互模拟的分摊思想，提出了分摊概率互模拟。在此之上构造的状态度量可验证差分隐私性质，且改进了Tschantz等人提出的基于状态上的层级关系族的方法。我们运用状态度量方法给出了带硬币偏差的密码学家就餐协议的差分隐私值的上界。　　论文的第三部分进一步探讨用状态度量衡量概率系统相似程度的问题。我们试图找到一个状态度量，其上距离为0的状态对完整地刻画了互模拟。我们研究Kantorovich距离并提出了一个重要的概念:一个基于Kantorovich距离的比率变形的状态度量。它满足了前述要求，且存在可通过迭代方式计算的不动点表示，同时，它给出了差分隐私标准要求的路径概率分布间距离的一个上界。　　论文最后一部分的重心转移到证明系统的构造-并发系统性质证明方法中重要的公理化方法-上来。我们给出了分摊概率互模拟以及分摊观察同余的可靠且完备的证明系统。这两个证明系统使得我们能够仅通过语法层面的操作推导（可观察的）差分隐私行为。