dolev-yao-star-extrinsic/examples/nsl_pk/DY.Example.NSL.SecurityProperties.fst at main · REPROSEC/dolev-yao-star-extrinsic · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
module DY.Example.NSL.SecurityProperties

open Comparse
open DY.Core
open DY.Lib
open DY.Example.NSL.Protocol.Total.Proof
open DY.Example.NSL.Protocol.Stateful
open DY.Example.NSL.Protocol.Stateful.Proof

#set-options "--fuel 0 --ifuel 1 --z3rlimit 25  --z3cliopt 'smt.qi.eager_threshold=100'"

/// This module defines the security properties of the NSL protocol.
/// They are all implied by the protocol invariants,
/// defined in DY.Example.NSL.Protocol.Total.Proof
/// and DY.Example.NSL.Protocol.Stateful.Proof.
/// Because all functions of the NSL protocol preserve the protocol invariants,
/// the attacker function also preserves the invariants.
/// Hence these security theorems hold on every trace obtainable by the attacker.

/// If Bob thinks he talks with Alice,
/// then Alice thinks she talk to Bob (with the same nonces),
/// unless the attacker corrupted Alice or Bob.

val initiator_authentication:
  tr:trace -> i:timestamp ->
  alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes ->
  Lemma
  (requires
    event_triggered_at tr i bob (Respond2 alice bob n_a n_b) /\
    trace_invariant tr
  )
  (ensures
    is_corrupt (prefix tr i) (principal_label alice) \/
    is_corrupt (prefix tr i) (principal_label bob) \/
    event_triggered (prefix tr i) alice (Initiate2 alice bob n_a n_b)
  )
let initiator_authentication tr i alice bob n_a n_b = ()

/// If Alice thinks she talks with Bob,
/// then Bob thinks he talk to Alice (with the same nonces),
/// unless the attacker corrupted Alice or Bob.

val responder_authentication:
  tr:trace -> i:timestamp ->
  alice:principal -> bob:principal -> n_a:bytes -> n_b:bytes ->
  Lemma
  (requires
    event_triggered_at tr i alice (Initiate2 alice bob n_a n_b) /\
    trace_invariant tr
  )
  (ensures
    is_corrupt (prefix tr i) (principal_label alice) \/
    is_corrupt (prefix tr i) (principal_label bob) \/
    event_triggered (prefix tr i) bob (Respond1 alice bob n_a n_b)
  )
let responder_authentication tr i alice bob n_a n_b = ()

/// The nonce n_a is unknown to the attacker,
/// unless the attacker corrupted Alice or Bob.

val n_a_secrecy:
  tr:trace -> alice:principal -> bob:principal -> n_a:bytes ->
  Lemma
  (requires
    attacker_knows tr n_a /\
    trace_invariant tr /\ (
      (exists sess_id. state_was_set tr alice sess_id (InitiatorSentMsg1 bob n_a)) \/
      (exists sess_id n_b. state_was_set tr alice sess_id (InitiatorSentMsg3 bob n_a n_b)) \/
      (exists sess_id n_b. state_was_set tr bob sess_id (ResponderReceivedMsg3 alice n_a n_b))
    )
  )
  (ensures is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob))
let n_a_secrecy tr alice bob n_a =
  attacker_only_knows_publishable_values tr n_a

/// The nonce n_b is unknown to the attacker,
/// unless the attacker corrupted Alice or Bob.

#push-options "--z3rlimit 50"
val n_b_secrecy:
  tr:trace -> alice:principal -> bob:principal -> n_b:bytes ->
  Lemma
  (requires
    attacker_knows tr n_b /\
    trace_invariant tr /\ (
      (exists sess_id n_a. state_was_set tr bob sess_id (ResponderSentMsg2 alice n_a n_b)) \/
      (exists sess_id n_a. state_was_set tr bob sess_id (ResponderReceivedMsg3 alice n_a n_b)) \/
      (exists sess_id n_a. state_was_set tr alice sess_id (InitiatorSentMsg3 bob n_a n_b))
    )
  )
  (ensures is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob))
let n_b_secrecy tr alice bob n_b =
  attacker_only_knows_publishable_values tr n_b
#pop-options