Changeset 16158


Ignore:
Timestamp:
12/05/08 10:27:49 (4 years ago)
Author:
hritcu
Message:

Fixed the remaining old examples.

Files:
5 edited

Legend:

Unmodified
Added
Removed

  • processes/old/daa-join.spi

    r13094 r16158  
    11(** Direct Anonymous Attestation (DAA) - Join Protocol *) 
    22 
    3 statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) (*: Stm(Pair(yid : Un, Pair(yu : Blind(Private), Pair(yn : Un, Pair(yxi : Un, Ok [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]))))) *). 
     3statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) 
     4        (*: Stm(yid : Un, yu : Blind(Private), yn : Un, yxi : Un; [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]) *). 
    45 
    56predicate ValidTPM(*1*). 
    … …  
    1819        new r (*: Blinder(Private) *); 
    1920        (assume(*#Join(tid, blind(f,r))*) | 
    20         out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1(*=d6*), bsni(*: Untainted *)))(*=y*),f(*: Private*))),hash(pair(n1(*=d7*), bsni(*: Untainted *))))); 
    21         out(c2,pair(tid(*=xid*),pair(blind(f,r)(*=xu*),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) )); 
     21        out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1, bsni(*: Un *))),f(*: Private*))),hash(pair(n1, bsni(*: Un *))))); 
     22        out(c2,pair((*=xid*)tid,pair((*=xu*)blind(f,r),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) )); 
    2223        in(c3, x); 
    2324        let cert = unblind(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(x, r, bvk(ki)) in 
    2425        let tt = bcheck(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(cert, bvk(ki)) in 
    25         let xu = fst(tt) in 
     26        let (xu, o) = tt in 
    2627        let d1 = eq(xu, f) in 
    27         let o = snd(tt) in 
    28         let d2 = exercise(o) in 
    2928        assert(*#Joined(tid,f,blind(f,r))*) 
    3029        ). 
    … …  
    3433        !in(c1,xzk); 
    3534        in(c2,ttt); 
    36         let yid = fst(ttt) in 
    37         let tt = snd(ttt) in 
    38         let yu = fst(tt) in 
    39         let o1 = snd(tt) in 
    40         let d1 = exercise(o1) in 
    41         let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1(*=d2*), bsni(*: Untainted *)))(*=d*),f(*:Private*))), pair(n1(*=d8*), bsni(*: Untainted *))) in 
    42         let d2 = exercise(o2) in 
     35        let (yid, tt) = ttt in 
     36        let (yu, o1) = tt in 
     37        let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1, bsni(*: Un *))),f(*:Private*))), pair(n1, bsni(*: Un *))) in 
    4338        (assert(*#Certified(yid,yu)*) | 
    44         out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair(yu(*=x*),ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki)) 
     39        out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair((*=x*)yu,ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki)) 
    4540        ). 
    4641 
    4742process 
    48         new c2 (*: Ch Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*] ))*); 
    49         new bsni (*: Untainted *); 
     43        new c2 (*: Ch(Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*] )))*); 
     44        new bsni (*: Un *); 
    5045        new daaseed (*: Private *); 
    5146        new f (*: Private *); (** cutting corners for now *) 

  • processes/old/daa.spi

    r13094 r16158  
    11(** Direct Anonymous Attestation (DAA) *) 
    22 
    3 statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) (*: Stm(Pair(yid : Un, Pair(yu : Blind(Private), Pair(yn : Un, Pair(yxi : Un, Ok [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]))))) *). 
     3statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) 
     4        (*: Stm(yid : Un, yu : Blind(Private), yn : Un, yxi : Un; [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]) *). 
    45 
    56statement ssign(*2,4*) = 
    67        landh(eqh(bcheckh(alpha(*2*), beta(*1*)), alpha(*1*)), 
    78                eqh(hash(pair(beta(*3*),alpha(*1*))), beta(*2*))) 
    8         (*: Stm(Pair( 
    9                 yvk : BlindVerKey(Pair(yu : Blind(Private), Ok [*#exists([xid],Certified(xid,yu))*])), Pair( 
    10                 yn : Un, Pair( 
    11                 yxi : Un, Pair( 
    12                 ym : Un, 
    13                 Ok [*#exists([xf,xcert,xv,xbs,xid], and(and(equal(yn,hash(pair(yxi,xf))), Certified(xid,blind(xf,xv))),DSigned(xf,ym)))*]))))) 
     9        (*: Stm( 
     10                yvk : BlindVerKey(Pair(yu : Blind(Private), Ok [*#exists([xid],Certified(xid,yu))*])), 
     11                yn : Un, 
     12                yxi : Un, 
     13                ym : Un; 
     14                [*#exists([xf,xcert,xv,xbs,xid], and(and(equal(yn,hash(pair(yxi,xf))), Certified(xid,blind(xf,xv))),DSigned(xf,ym)))*]) 
    1415        *). 
    1516 
    … …  
    3536        new r (*: Blinder(Private) *); 
    3637        (assume(*#Join(tid, blind(f,r))*) | 
    37         out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1(*=d6*), bsni(*: Untainted *)))(*=y*),f(*: Private*))),hash(pair(n1(*=d7*), bsni(*: Untainted *))))); 
    38         out(c2,pair(tid(*=xid*),pair(blind(f,r)(*=xu*),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) )); 
     38        out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1, bsni(*: Un *))),f(*: Private*))),hash(pair(n1, bsni(*: Un *))))); 
     39        out(c2,pair((*=xid*)tid,pair((*=xu*)blind(f,r),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) )); 
    3940        in(c3, xbs); 
    4041        let cert = unblind(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(xbs, r, bvk(ki)) in 
    4142        let tt = bcheck(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(cert, bvk(ki)) in 
    42         let xu = fst(tt) in 
     43        let (xu, o) = tt in 
    4344        let d1 = eq(xu, f) in 
    44         let o = snd(tt) in 
    45         let d2 = exercise(o) in 
    4645        (assert(*#Joined(tid,f,blind(f,r))*) | 
    4746         
    4847        (** Sign *) 
    49         new m (*: Untainted *); 
     48        new m (*: Un *); 
    5049        new xi (*: Un *); 
    5150        (assume(*#DSigned(f,m)*) | 
    52         out(c4, zk(*2,4,ssign*)(f, cert, bvk(ki), hash(pair(xi(*=d2*),f(*: Private *))), xi, m)) 
     51        out(c4, zk(*2,4,ssign*)(f, cert, bvk(ki), hash(pair(xi,f(*: Private *))), xi, m)) 
    5352        ))). 
    5453 
    … …  
    5756        !in(c1,xzk); 
    5857        in(c2,ttt); 
    59         let yid = fst(ttt) in 
    60         let tt = snd(ttt) in 
    61         let yu = fst(tt) in 
    62         let o1 = snd(tt) in 
    63         let d1 = exercise(o1) in 
    64         let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1(*=d2*), bsni(*: Untainted *)))(*=d*),f(*:Private*))), pair(n1(*=d8*), bsni(*: Untainted *))) in 
    65         let d2 = exercise(o2) in 
     58        let (yid, tt) = ttt in 
     59        let (yu, o1) = tt in 
     60        let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1, bsni(*: Un *))),f(*:Private*))), pair(n1, bsni(*: Un *))) in 
    6661        (assert(*#Certified(yid,yu)*) | 
    67         out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair(yu(*=yu*),ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki)) 
     62        out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair((*=yu*)yu,ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki)) 
    6863        ). 
    6964 
    … …  
    7166        !in(c4, xzks); 
    7267        let tttt = ver(*2,4,1,ssign*)(xzks,bvk(ki)) in 
    73         let xn = fst(tttt) in 
    74         let ttt = snd(tttt) in 
    75         let xxi = fst(ttt) in 
    76         let tt = snd(ttt) in 
    77         let xm = fst(tt) in 
    78         let o = snd(tt) in 
    79         let d = exercise(o) in 
     68        let (xn, ttt) = tttt in 
     69        let (xxi, tt) = ttt in 
     70        let (xm, o) = tt in 
    8071        assert(*#Authenticated(xm)*). 
    8172 
    8273process 
    83         new c2 (*: Ch Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*] ))*); 
    84         new bsni (*: Untainted *); 
     74        new c2 (*: Ch(Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*])))*); 
     75        new bsni (*: Un *); 
    8576        new daaseed (*: Private *); 
    8677        new f (*: Private *); (** cutting corners for now *) 

  • processes/old/proxy.spi

    r13095 r16158  
    1111        new song(*:Un*); 
    1212        (assume(*#Order(u,song)*) | 
    13         out(c, sign(pair(song(*=s*),ok(*:Ok[*#Order(u,s)*]*)),ku))). 
     13        out(c, sign(pair((*=s*)song,ok(*:Ok[*#Order(u,s)*]*)),ku))). 
    1414 
    1515let proxy = 
    … …  
    1717        !in(c,m); 
    1818        let p = check(m,vk(ku)) in 
    19         let s = fst(p) in 
    20         let o = snd(p) in 
    21         let d = exercise(o) in 
    22         out(c, sign(pair(u(*=u1*),pair(s(*=s1*),ok(*:Ok[*#and(Order(u1,s1),Registered(u1))*]*))(*:Pair(s1:Un,Ok[*#and(Order(u1,s1),Registered(u1))*])*)), kp)). 
     19        let (s, o) = p in 
     20        out(c, sign(pair((*=u1*)u,pair((*=s1*)s,ok(*:Ok[*#and(Order(u1,s1),Registered(u1))*]*))(*:Pair(s1:Un,Ok[*#and(Order(u1,s1),Registered(u1))*])*)), kp)). 
    2321 
    2422let store = 
    2523        !in(c,x); 
    2624        let ttt = check(x,vk(kp)) in 
    27         let u = fst(ttt) in 
    28         let tt = snd(ttt) in 
    29         let s = fst(tt) in 
    30         let o = snd(tt) in 
    31         let d = exercise(o) in 
     25        let (u, tt) = ttt in 
     26        let (s, o) = tt in 
    3227        assert(*#CanDownload(u,s)*). 
    3328 

  • processes/old/sign.spi

    r13094 r16158  
    88        in(c, m); 
    99        (assume (*#Good(m)*) | 
    10         out(c, sign(pair(m(*=x*),ok(*:Ok [*#Good(x)*]*)), ks)) 
     10        out(c, sign(pair((*=x*)m,ok(*:Ok [*#Good(x)*]*)), ks)) 
    1111        ). 
    1212 
    … …  
    1414        !in(c, y); 
    1515        let m = check(y, vk(ks)) in  
    16         let z = fst(m) in 
    17         let p = snd(m) in 
    18         let dummy = exercise(p) in 
     16        let (z, p) = m in 
    1917        assert (*#Good(z)*). 
    2018 
    … …  
    2220        !in(c, y); 
    2321        let m = check(y, vk(ks)) in  
    24         let z = fst(m) in 
    25         let p = snd(m) in 
    26         let dummy = exercise(p) in 
     22        let (z, p) = m in 
    2723        assert (*#Good(z)*). 
    2824 

  • src/typechecker/parser.mly

    r16157 r16158  
    244244        | IDENT LPAREN STAR COLON typedef STAR RPAREN   { Ident($1, Some $5) } 
    245245        | PAIR LPAREN LPAREN STAR EQUAL IDENT STAR RPAREN term COMMA term LPAREN STAR COLON typedef STAR RPAREN RPAREN 
    246                                                                                                                 { Pair($9, Some $6, $11, Some($15)) } 
    247         | PAIR LPAREN LPAREN STAR EQUAL IDENT STAR RPAREN term COMMA term RPAREN { Pair($9, Some $6, $11, None) } 
     246                                                                                                                { Pair($9, Some $6, $11, Some $15) } 
     247        | PAIR LPAREN term COMMA term LPAREN STAR COLON typedef STAR RPAREN RPAREN 
     248                                                                                                                { Pair($3, None, $5, Some $9) } 
     249        | PAIR LPAREN LPAREN STAR EQUAL IDENT STAR RPAREN term COMMA term RPAREN 
     250                                                                                                                { Pair($9, Some $6, $11, None) } 
     251        | PAIR LPAREN term COMMA term RPAREN 
     252                                                                                                                { Pair($3, None, $5, None) } 
    248253        | constr LPAREN STAR COLON typedef STAR RPAREN  { Constr($1, Some $5) } 
    249254        | constr                                                                                { Constr($1, None) } 
Note: See TracChangeset for help on using the changeset viewer.