网络安全认证协议形式化分析.ppt

网络安全认证协议形式化分析
7/28/2018
1
第二十次全国计算机安全学术交流会
Organization
Introduction
Related Work
Formal System Notation
Intruders Algorithmic Knowledge Logic
Verification Using SPIN/Promela
Conclusion
7/28/2018
2
第二十次全国计算机安全学术交流会
Introduction
Cryptographic protocols are protocols that use cryptography to distribute keys and authenticate principals and data over work.
Formal methods, bination of a mathematical or logical model of a system and its requirements, together with an effective procedure for determining whether a proof that a system satisfies its requirements is correct.
Model;
Requirement (Specification);
Verification.
7/28/2018
3
第二十次全国计算机安全学术交流会
Introduction (cont.)
In cryptographic protocols, it is very crucial to ensure:
Messages meant for a principal cannot be read/accessed by others (secrecy);
Guarantee genuineness of the sender of the message (authenticity);
Integrity;
Non-Repudiation (NRO, NRR);
Fairness, etc.
7/28/2018
4
第二十次全国计算机安全学术交流会
Related Work
Techniques of verifying security properties of the cryptographic protocols can be broadly categorized:
methods based on belief logics (BAN Logic)
π-calculus based models
state machine models (Model Checking)
Model checking advantages (compare with theory proving):
automatic; counterexample if violation
Use LTL (Linear temporal logic ) to specify properties
FDR (Lowe); Mur(Mitchell);
Interrogator (Millen); Brutus (Marrero)
SPIN (Hollzmann)
theorem prover based methods (NRL, Meadows)
methods based on state machine model and theorem prover (Athena, Dawn)
Type checking
ISCAS, LOIS, …(in China)
7/28/2018
5
第二十次全国计算机安全学术交流会
Notation
(1) Messages
a ∈Atom ::= C | N | k | 
m ∈ Msg ::= a | m• m | {m}k
(2) Contain Relationship (⊑)
m ⊑ a ≜ m = a
m ⊑ m1• m2 ≜ m = m1• m2 ∨ m ⊑ m1∨ m ⊑ m2
m ⊑{m1}k ≜ m = {m1}k ∨ m ⊑ m1
Submessage: sub-msgs(m) ≜{m’∈ Msg | m’⊑ m }
7/28/2018
6
第二十次全国计算机安全学术交流会
Notation
(3) Derivation (⊦, Dolev-Yao model)
m ∈ B ⇒ B ⊦ m
B ⊦ m ∧ B ⊦ m’⇒ B ⊦ m•