def atm,alice,bank,prt.
def withdraw.
fun login : <> -> <some user. 'user,cert>{R atm atm}.
fun request : all agent,user. 
  <'agent,'user,cert,cert>{R bank bank} -> int{R agent agent, T agent}.
fun listen : <> -> (some agent,user. <'agent,'user,cert,cert,
  (int{R agent agent} -> <>)>){R bank bank, T bank}.
fun print : int{R atm prt} -> <>.
fun get : all user. ('user) -> int{R user&bank bank}.
fun set : all user. ('user) -> int{R user&bank bank} -> <>.

< 
  fun u:<>.
  if (acquire 'atm #> '(declassify bank)) 
    => 'atm #> '(declassify bank) then
    bind x = login <> in
    let <y,cdel> = x in
    open userid = y with user in
    let creq = acquire userid #> withdraw in
    let msg = <'atm, userid, cdel, creq> in
    let dmsg = declassify msg as <'atm,'user,cert,cert>{R bank bank} in
    bind balance = request [atm,user] dmsg in
    if (acquire 'atm #> '(declassify prt)) 
      => 'atm #> '(declassify prt) then
      let dbalance = declassify balance as int{R atm prt} in    
      print dbalance
    else <>
  else error "insecure network"
,
  fun u:<>.
  bind x0 = listen <>, x=x0 in
  open y = x with agent, user in
  if (acquire 'bank #> '(declassify user))
    => 'bank #> '(declassify user) then
    let <agentid,userid,cdel,creq,reply> = y in
    if cdel => userid #> '(delegate agent) then
      delegate userid <: agentid in
      if creq => userid #> 'withdraw then
        let old = get [user] userid in
        let balance = bind x = old in x - 100 in
        let y = set [user] userid balance in
        let dbalance = declassify balance as int{R user user} in
        reply dbalance
      else <>
    else error "insecure atm"
  else error "insecure network"
>