-
Notifications
You must be signed in to change notification settings - Fork 0
/
invitation.vp
60 lines (46 loc) · 1.48 KB
/
invitation.vp
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
attacker[active]
principal Alice[
knows private invitation_unlock_key
generates invitation_secret
knows private alice_server_session_key
knows public invitation_id_input_constant
]
principal Server[
knows private alice_server_session_key
knows private bob_server_session_key
]
principal Bob[
knows private bob_server_session_key
]
principal Alice[
invitation_id = MAC(invitation_unlock_key, invitation_id_input_constant)
invitation_ciphertext = AEAD_ENC(invitation_unlock_key, invitation_secret, invitation_id)
invitation_server = ENC(alice_server_session_key, CONCAT(invitation_id, invitation_ciphertext))
]
Alice -> Server: invitation_server
principal Server[
server_invitation_id, server_invitation_ciphertext = SPLIT(DEC(alice_server_session_key, invitation_server))
]
principal Bob[
knows private invitation_unlock_key
bob_invitation_id = MAC(invitation_unlock_key, invitation_id_input_constant)
]
Bob -> Server: bob_invitation_id
principal Server[
invitation_bob = ENC(bob_server_session_key, server_invitation_ciphertext)
]
Server -> Bob: invitation_bob
principal Bob[
bob_invitation_ciphertext = DEC(bob_server_session_key, invitation_bob)
bob_invitation_secret = AEAD_DEC(invitation_unlock_key, bob_invitation_ciphertext, bob_invitation_id)
]
phase[1]
principal Server[
leaks server_invitation_ciphertext
leaks server_invitation_id
]
queries[
confidentiality? invitation_unlock_key
confidentiality? bob_invitation_secret
equivalence? invitation_id, bob_invitation_id
]