-
Notifications
You must be signed in to change notification settings - Fork 0
/
trustedLaunch.pv
82 lines (64 loc) · 2.35 KB
/
trustedLaunch.pv
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
free c:channel.
free d:channel [private].
free sp:bitstring.
free IDttp:bitstring.
free m:bitstring [private].
query attacker(m).
(* = Define Primitives = *)
(* == Public-private keys == *)
type pkey.
type skey.
fun pk(skey): pkey.
fun aencrypt(bitstring, pkey):bitstring.
reduc forall x: bitstring, y:skey; adecrypt(aencrypt(x, pk(y)), y) = x.
(* == Signatures == *)
type spkey.
type sskey.
fun spk(sskey):spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall x: bitstring, y: sskey; getmess(sign(x, y)) = x.
reduc forall x: bitstring, y: sskey; checksign(sign(x, y), spk(y)) = x.
(* == Shared key encryption == *)
type nonce.
fun sencrypt(bitstring, nonce):bitstring.
reduc forall x:bitstring, y:nonce; sdecrypt(sencrypt(x, y), y) = x.
let DM(pkeyDM:pkey, skeyDM:skey, pkeyTTP:pkey) =
out (c, aencrypt(m, pkeyTTP));
in (c, tauTPM:bitstring);
let (=adecrypt(tauTPM, skeyDM), t:bitstring) = m in
0.
let SC(request:bitstring) =
in (c, (tau:bitstring, pkeyDM:pkey));
out(d, request);
in(d, (pkeyTPM:pkey, signTPM:bitstring, iml:bitstring));
out(c, (pkeyTPM, signTPM, iml, tau));
in(d, tauTPM:bitstring);
out(d, tauTPM);
in(d, tauSC:bitstring);
out(c, aencrypt(tauSC, pkeyDM)).
let TPM(pkeyTPM:pkey, skeyTPM:skey, sskeyTPM:sskey, iml:bitstring) =
in (d, request:bitstring);
out(d, (pkeyTPM, sign(iml, sskeyTPM), iml));
in (d, tauTPM:bitstring);
out(d, adecrypt(tauTPM, skeyTPM)).
let TTP(pkeyTTP:pkey, skeyTTP:skey, spkeyTPM:spkey, imlGold:bitstring) =
in (c, (pkeyTPM:pkey, sigmaTTP:bitstring, iml:bitstring, tauTTP:bitstring));
let(=iml, i:bitstring) = checksign(sigmaTTP, spkeyTPM) in
let(=iml, z:bitstring) = imlGold in
out(c, aencrypt(adecrypt(tauTTP, skeyTTP), pkeyTPM)).
(* ==Launch VM ==*)
(* = Main = *)
process
new skeyDM: skey;
new skeyTTP: skey;
new skeyTPM: skey;
new sskeyTPM: sskey;
new request:bitstring;
new iml:bitstring;
let pkeyDM = pk(skeyDM) in out (c, pkeyDM);
let pkeyTTP = pk(skeyTTP) in out (c, pkeyTTP);
let pkeyTPM = pk(skeyTPM) in out (c, pkeyTPM);
let spkeyTPM =spk(sskeyTPM) in out (c, spkeyTPM);
let tau = aencrypt(m, pkeyTTP) in out (c, tau);
let imlGold = iml in out (c, imlGold);
( (!DM(pkeyDM, skeyDM, pkeyTTP)) | (!TPM(pkeyTPM, skeyTPM, sskeyTPM, iml)) | (!SC(request)) | (!TTP(pkeyTTP, skeyTTP, spkeyTPM, imlGold)) )