-
Notifications
You must be signed in to change notification settings - Fork 0
/
OTS.ec
82 lines (67 loc) · 1.88 KB
/
OTS.ec
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
require import FSet Int Real SmtMap Distr.
abstract theory OTS_Theory.
(* types and functions associated with One-Time Signature Scheme *)
type pkey, skey, message, sig.
op otsSig : skey -> message -> sig.
op otsVer : pkey option -> message -> sig -> bool.
op otsKey : int -> pkey * skey.
require import KeyGen.
clone import KeyGen with type pkey <- pkey,
type skey <- skey,
op keyGen <- otsKey.
(* the OTS oracle module type *)
module type OTSOracleT = {
proc init(pk : pkey, sk : skey) : unit
proc sign(m : message) : sig option
proc fresh(m : message) : bool
}.
(* The OTS adversaries with the access to the OTS oracle *)
module type AdvOTS (O : OTSOracleT) = {
proc forge(pk : pkey) : message * sig {O.sign}
}.
(* OTS game which represents the existantial unforgeability under the
chosen message attack *)
module GameOTS(O : OTSOracleT, A : AdvOTS, K : KeyGenT) = {
module A = A(O)
var s : sig
var m : message
proc main() : bool = {
var pk, sk, forged, fresh;
(pk, sk) <@ K.keyGen();
O.init(pk, sk);
(m, s) <@ A.forge(pk);
forged <- otsVer (Some pk) m s;
fresh <@ O.fresh(m);
return forged /\ fresh;
}
}.
(* The standard implementation of OTS oracle. Note that the oracle
will generate the signature for only one message. *)
module OTSOracle : OTSOracleT = {
var qs : message option
var used : bool
var pk : pkey
var sk : skey
proc init(pk : pkey, sk : skey) : unit = {
OTSOracle.pk <- pk;
OTSOracle.sk <- sk;
qs <- None;
used <- false;
}
proc sign(m : message) : sig option = {
var r, q;
if(!used){
qs <- Some m;
q <- otsSig sk m;
r <- Some q;
}else{
r <- None;
}
used <- true;
return r;
}
proc fresh(m : message) : bool = {
return (Some m) <> qs;
}
}.
end OTS_Theory.