apachi_observational_id.spthy

theory apachi_observational_id
begin

/*
 *  Author: Yoav S. & Nicolai S.
 *  Model Name: apachi_observational_id.spthy
 *  Status: DEVELOPMENTAL
 *
 */

builtins: asymmetric-encryption, symmetric-encryption
functions: commit/2, paper/1, randomness/1, id/1, revealSign/2, getMessage/1
equations: getMessage(revealSign(m, privk)) = m

rule Setup:
    [Fr(~id1), Fr(~id2), Fr(~pc_privk)]
  --[]->
    [SubmitterId(~id1), SubmitterId(diff(~id1, ~id2)),
     !PC_privk(~pc_privk),
     Out(<~id1, ~id2>)]

rule Submission:
  let
    paper_commit = commit(paper(~paper), randomness(~r_submit))
    identity_commit = commit(id(submitter_id), randomness(~r_id))
    signed_commits = revealSign(<paper_commit, identity_commit>, ~submitter_privk)

    submission = senc(<paper(~paper), randomness(~r_submit), randomness(~r_review)>, ~submitter_key)
    submission_key = aenc(~submitter_key, pk(~pc_privk))
    signed_submission = revealSign(<submission, submission_key>, ~submitter_privk)
  in
    [Fr(~paper), Fr(~r_submit), Fr(~r_review), Fr(~r_id), Fr(~submitter_key), Fr(~submitter_privk),
     !PC_privk(~pc_privk),
     SubmitterId(submitter_id)]
  --[]->
    [Out(signed_commits),
     Out(signed_submission),
     Out(<~pc_privk, ~submitter_privk>)]

end