第一部分 开场白 3
第1章 简介 3
1.1对安全的需求 3
1.2问题 3
1.3原因 3
1.4传统方法 4
1.5基于模型的UML安全工程 6
1.6概览 7
1.6.1 UMLsec扩展 7
1.6.2应用 7
1.6.3工具支持 8
1.7纲要 9
1.8怎样使用本书 10
第2章 UML构建安全概览 11
2.1使用用例图获取安全需求 11
2.2使用活动图的安全交易过程 12
2.3使用部署图的物理安全 13
2.4使用顺序图的安全交互过程 13
2.5使用状态图的安全状态 15
第3章 背景知识 16
3.1安全工程 16
3.2统一建模语言（Unified Modeling Language） 18
3.2.1用例图（Use Case Diagrams） 19
3.2.2类图（Class Diagrams） 19
3.2.3状态图（Statechart Diagrams） 20
3.2.4顺序图（Sequence Diagrams） 21
3.2.5活动图（Activity Diagrams） 22
3.2.6部署图（Deployment Diagrams） 23
3.2.7子系统（Subsystems） 24
3.2.8 UML扩展机制 25
3.3 UML模型分析 25
3.3.1 UML表示 26
3.3.2形式语义概要 26
3.3.3密码学建模 27
3.3.4 UML图的安全分析 29
3.3.5重要的安全属性 31
第二部分 开发安全系统 37
第4章 基于模型的UML安全工程 37
4.1 UMLsec模板 37
4.1.1开发安全关键系统的UML扩展的需求 37
4.1.2扩展 38
4.1.3表达需求 51
4.2安全系统设计原则 51
4.3应用安全模式 52
4.4参考文献注解 54
4.5结论 55
第5章 应用实例 56
5.1安全信道 56
5.2网络协议TLS的一个变种协议 60
5.3通用电子钱包规范 66
5.3.1支付业务 67
5.3.2充值业务 74
5.4开发安全的Java程序 90
5.4.1 Java的访问控制 90
5.4.2设计过程 91
5.4.3例子：商务应用系统 93
5.5更多应用 95
5.5.1银行应用系统的建模与验证 95
5.5.2生物特征认证系统 96
5.5.3机动车应急应用系统 97
5.5.4德国电子健康卡 97
5.5.5啤酒节电子钱包 97
5.5.6保险公司的电子签名体系 97
5.6参考文献注解 97
5.7结论 98
第三部分 工具支持 101
第6章 UMLsec的工具支持 101
6.1用分析工具扩展UML用例工具 101
6.1.1元对象工具MOF（Meta-Object Facility） 101
6.1.2用元数据仓库MDR实现基于XML的数据绑定 103
6.2 UMLsec自动化工具 104
6.2.1工具的功能 104
6.2.2实现细节 106
6.2.3模型检测UMLsec规范 107
6.2.4自动化定理证明 107
6.2.5产生基于Prolog的攻击 107
6.3运行时数据的连接模型：SAP R／3权限 108
6.3.1安全规则的自动化分析 109
6.3.2实例数据 111
6.3.3评估规则 113
6.4将模型与代码连接起来 116
6.4.1测试序列的生成 116
6.4.2代码生成与代码分析 118
6.5参考文献注解 119
6.6结论 120
第7章 形式化基础 121
7.1 UML状态机 121
7.2 UML状态机系统 127
7.3求精 130
7.4信任-保证规范 133
7.5推理安全性质 133
7.5.1求精 136
7.5.2机密性 137
7.5.3完整性 139
7.5.4真实性 139
7.5.5新鲜性 140
7.5.6安全信息流 141
7.6参考文献注解 142
7.7结论 142
第8章 使用UML的形式化系统开发 144
8.1 UML片段形式语义 144
8.1.1一般概念 146
8.1.2类图 151
8.1.3状态图 152
8.1.4序列图 161
8.1.5活动图 164
8.1.6部署图 166
8.1.7子系统 166
8.2使用UML开发 171
8.2.1求精 172
8.2.2信任-保证规范 174
8.2.3在UML中推理安全性质 174
8.3参考文献注解 175
8.4结论 176
第四部分 尾声 179
第9章 其他相关研究 179
9.1更多关于UMLsec方法的资料 179
9.2其他的安全工程方法 179
9.2.1软件工程与安全性 179
9.2.2 UML的其他使用方法 180
9.2.3应用于安全领域的形式化方法 181
9.2.4其他非功能性需求 183
第10章 展望 184
第五部分 附录 187
附录A 面向UML 2.0 187
附录B UML状态机规则的语义 189
附录C 证明 191
C.1 UML状态机 191
C.2求精 192
C.3信任-保证规范 193
C.4安全性质的推理 194
C.5用UML进行形式化系统开发 197
C.6可靠信道 199
C.7 Internet TLS协议的一个变种 200
C.8通用电子钱包规范 204
C.8.1支付业务 204
C.8.2充值业务 207
参考文献 210