计算机数理逻辑-程序验证-协议安全分析

1. The Neuman-Stubblebine key exchange protocol

1.1. breaking

  • The intruder now sends a message to B, and the message will make B believe it’s actually from A. Thus B will start to use the wrong key, i.e. an insecure key.
    • 入侵者现在向B发送一个信息，这个信息将使B相信它实际上来自A，因此B将开始使用错误的密钥，即一个不安全的密钥。

2. Verification of security protocols using resolution

  • The idea is that the security property says an unsafe state is possible
  • Since first-order logic is not decidable, there is however no guarantee that the saturation will terminate when the security property does not hold. Non-termination can therefore indicate the existence of a potential attack on the protocol.

3. Assumptions in security protocol analysis

What can an intruder do?

  • The intruder can capture all messages sent by one participant to another
  • It can send a message it has constructed to any other participant
  • It can generate new keys, new nonces, timestamps . . .
  • It can construct new messages from the ones it has, using legal constructors
  • The intruder can decompose分解 tuples from which messages are formed
  • It can decrypt encrypted parts, but only if it knows the key I.e. we assume perfect cryptography: an intruder cannot break any keys nor does it know any of the initial keys $K_{at}$ at or $K_{bt}$

4. Encoding

4.1. The capabilities of the intruder入侵者

5. SPASS

SPASS is an automated theorem prover for first-order logic with equality. So the input for the prover is a first-order formula in our syntax.

  • Running SPASS on such a formula results in the final output SPASS beiseite: Proof found. if the formula is valid,
  • SPASS beiseite: Completion found. if the formula is not valid
  • and because validity in first-order logic is undecidable, SPASS may run forever without producing any final result.

An SPASS input file consists of three parts, a description part started with list_of_descriptions., a part where the signature is declared starting with list_of_symbols., a part where all axioms are given, starting with list_of_formulae(axioms). and a final part where all conjectures are presented, starting with list_of_formulae(conjectures)

Then SPASS tries to prove that the conjunction of all axiom formulae implies the disjunction of all conjectures

6. Saturation

Aclause C is a condensation of a clause D,if C is a proper (unordered) factor of D that subsumes D

A set of clauses N is called saturated if it is closed under condensation, the deletion of subsumed clauses and any clause generated by an ordered resolution inference from clauses from N is subsumed by some clause in N