References of "Kramer, Simon 40021221"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailLogic of Non-Monotonic Interactive Proofs
Kramer, Simon UL

in Lecture Notes in Computer Science (2013), 7750

We propose a monotonic logic of internalised non-monotonic or instant interactive proofs (LiiP) and reconstruct an existing monotonic logic of internalised monotonic or persistent interactive proofs (LiP ... [more ▼]

We propose a monotonic logic of internalised non-monotonic or instant interactive proofs (LiiP) and reconstruct an existing monotonic logic of internalised monotonic or persistent interactive proofs (LiP) as a minimal conservative extension of LiiP. Instant interactive proofs effect a fragile epistemic impact in their intended communities of peer reviewers that consists in the impermanent induction of the knowledge of their proof goal by means of the knowledge of the proof with the interpreting reviewer: If my peer reviewer knew my proof then she would at least then know that its proof goal is true. Their impact is fragile and their induction of knowledge impermanent in the sense of being the case possibly only at the instant of learning the proof. This accounts for the important possibility of internalising proofs of statements whose truth value can vary, which, as opposed to invariant statements, cannot have persistent proofs. So instant interactive proofs effect a temporary transfer of certain propositional knowledge (knowable ephemeral facts) via the transmission of certain individual knowledge (knowable non-monotonic proofs) in distributed systems of multiple interacting agents. [less ▲]

Detailed reference viewed: 49 (3 UL)
Full Text
Peer Reviewed
See detailLogic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)
Kramer, Simon UL

in Proc.\ 6th Workshop on Intuitionistic Modal Logic and Applications (2013)

Detailed reference viewed: 33 (0 UL)
Full Text
See detailA Logic of Interactive Proofs
Kramer, Simon UL

Report (2012)

Detailed reference viewed: 11 (1 UL)
Full Text
Peer Reviewed
See detailComputer-Aided Decision-Making with Trust Relations and Trust Domains (Cryptographic Applications)
Kramer, Simon UL; Goré, Rajeev; Okamoto, Eiji

in Journal of Logic & Computation (2012)

We propose generic declarative definitions of individual and collective trust relations between interacting agents and agent collections, and trust domains of trust-related agents in distributed systems ... [more ▼]

We propose generic declarative definitions of individual and collective trust relations between interacting agents and agent collections, and trust domains of trust-related agents in distributed systems. Our definitions yield (1) (in)compatibility, implicational and transitivity results for trust relationships, including a Datalog-implementability result for their logical structure; (2) computational complexity results for deciding potential and actual trust relationships and membership in trust domains; (3) a positive (negative) compositionality result for strong (weak) trust domains; (4) a computational design pattern for building up strong trust domains; and (5) a negative scalability result for trust domains in general. We instantiate our generic trust concepts in five major cryptographic applications of trust, namely: Access Control, Trusted Third Parties, the Web of Trust, Public-Key Infrastructures and Identity-Based Cryptography. We also show that accountability induces trust. Our defining principle for weak and strong trust (domains) is (common) belief in and (common) knowledge of agent correctness, respectively. [less ▲]

Detailed reference viewed: 33 (0 UL)
Full Text
Peer Reviewed
See detailA Modular Multi-Modal Specification of Real-Timed, End-To-End Voter-Verifiable Voting Systems
Kramer, Simon UL; Ryan, Peter UL

in 2011 International Workshop on Requirements Engineering for Electronic Voting Systems (REVOTE) (2011)

We propose a modular multi-modal specification of real-timed, end-to-end voter-verifiable voting systems, i.e., a formal but intuitive specification of real-timed voting systems that are accountable (and ... [more ▼]

We propose a modular multi-modal specification of real-timed, end-to-end voter-verifiable voting systems, i.e., a formal but intuitive specification of real-timed voting systems that are accountable (and thus trustworthy) to their users. Our specification is expressed as a single but well-compounded formula in a logical language of temporal, epistemic, and provability modalities. The intuitiveness of the specification is the fruit of its modular and multi-modal form. This means that the specification can be appreciated compound-wise, as a logical conjunction of separate sub-requirements, each of which achieving the ideal of a formal transcription of a suitable natural-language formulation, thanks to powerful descriptive idioms in the form of our multiple modalities. The modular form reduces our proof of the satisfiability (consistency) and thus implementability of the specification to a proof by inspection, and induces the parallelisability of implementation-correctness verifications. The specification also pinpoints the implementation-specific part of particular voting systems, reuses a generic definition of accountability inducing trust in a formal sense, and, last but not least, counter-balances by its implementability some previous results about the contradictory conjunction of certain desirable property pairs of voting systems. So in some sense, ideal voting systems do exist. Our specific formalisation principles are agent correctness, i.e., the behavioural correctness of the voting-system-constituting agents, and data adequacy, i.e., the soundness and (relative) completeness of the voting data processed by the system. [less ▲]

Detailed reference viewed: 82 (2 UL)