INRIA_Internship/Sap_Tam/Toy_t_diff.spthy at master · dchandak99/INRIA_Internship · 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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
theory Toy_diff
begin

builtins: hashing, asymmetric-encryption
//equations: radec(raenc(m,r,pk(sk)),sk) = m

// Registering a public key
rule Register_pk:
  [ Fr(~ltk) ]
  -->
  [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]

rule Get_pk:
  [ !Pk(A, pubkey) ]
  --[Get_(A)]->
  [ Out(pubkey) ]

rule Reveal_ltk:
    [ !Ltk(A, ltk) ]
  --[ LtkReveal(A) ]->
    [ Out(ltk) ]

rule Client_init:
    [ Fr(~k)         // choose fresh key
    , !Pk($S, pkS)
    , Fr(~r2)   // lookup public-key
    ]
  -->
    [ Client_init( $S, ~k )
    , Out( aenc(<~k, ~r2>, pkS ) )
    ]

rule Client_rec:
    [ Client_init(S, k)   // Retrieve server and session key
    , In( h(<k, r2>) )
    ]
  --[ Record_sess( S, k ) ]->
    [ Record_sess1( S, k )]

rule Serv_1:
    [ !Ltk($S, ~ltkS)                          // lookup the private-key
    , In( request )                            // receive a request
    ]
  --[ Ans_req($S, fst(adec(request, ~ltkS)))
    ]->
    [ Out( h(adec(request, ~ltkS))) ]

rule chall:
  [ Record_sess1(S,k)
  , Fr(~r)
  ]
--[ Challe(S, k, ~r)]->
  [ Out(diff(k, ~r))]

restriction Out__:
"   All S k r #i.
    Challe(S, k, r) @ #i
    ==> not(Ex #j. LtkReveal(S) @ j & j<i)
"
/*
restriction Out__1:
"   All S k r #i.
    Challe(S, k, r) @ #i
    ==> not(Ex #j. Client_init(S, k) @ j & i<j )
"*/

lemma Client_session_key_secrecy:
  "
    not(
      Ex S k ran #i #j #m.
        /* client has set up a session key 'k' with a server'S' */
        Record_sess(S, k) @ #i
        /* and the adversary knows 'k' */
      & K(k) @ #j
      & Challe(S, k, ran) @ #m
      & j<m
      & not(Ex #r. LtkReveal(S) @ r)
    )
  "


lemma Client_auth:
  "
    ( All S k #i.  Record_sess(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. Ans_req(S, k) @ a)
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

lemma Client_auth_injective:
  "
    ( All S k #i.  Record_sess(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. Ans_req(S, k) @ a
           /* and there is no other client that had the same request */
           & (All #j. Record_sess(S, k) @ #j ==> #i = #j)
       )
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

lemma Client_session_key_honest_setup:
  exists-trace
  " Ex S k #i.
        Record_sess(S, k) @ #i
      & not(Ex #r. LtkReveal(S) @ r)
  "

end