-
Notifications
You must be signed in to change notification settings - Fork 0
/
dh.spthy
42 lines (33 loc) · 779 Bytes
/
dh.spthy
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
theory dh
begin
builtins: diffie-hellman
rule Gen_secret:
[ Fr(~n) ]
--[ Secret(~n) ]->
[ Nonce(~n) ]
rule First1:
[ Nonce(~n), Fr(~tid) ]
-->
[ Out('g'^~n), First_waiting(~tid, ~n) ]
rule Second:
[ Nonce(~m), In(fp) ]
--[ SharedKey(fp^~m), Role('s') ]->
[ Out('g'^~m) ]
rule First2:
[ First_waiting(~tid, ~n), In(sp) ]
--[ SharedKey(sp^~n), Role('f') ]->
[]
lemma nonce_secret:
"All n #i.
Secret(n) @ #i ==>
not(Ex #j. K(n) @ #j)"
lemma key_secret:
"All k #i #j.
SharedKey(k)@i & Role('f')@i & SharedKey(k)@j & Role('s')@j ==>
not(Ex #r. K(k) @ #r)"
lemma can_end_up_with_same_key:
exists-trace
"Ex k #i #j.
Role('s') @i & SharedKey(k) @i &
Role('f') @j & SharedKey(k) @j"
end