Logics for Cryptographic Information Games

Preamble:

There is currently a zoo of various logics for evaluating (proving) security in cryptographic protocols. The idea is that, by expressing these protocols using some logic, you can create a formula describing some property (such as shared secrecy, message authentication, and perfect forward secrecy).

Example (Shared Secrecy Property): $(\forall t_i\forall C \ne A,B) \text{ } (A\text{ k } m) \land (B \text{ k } m) \land \lnot (C \text{ k } m)$

This translates to: "For all times, $t_i$, and all adversaries, $C$, (not Alice or Bob), it is true that $A$ and $B$ know message $m$, but $C$ does not".

By using some techniques from formal verification, we can sometimes generate a computer proof that such a statement holds for some protocols (or construct an attack). This gets harder as we add more power to our logics, such as incorporating multi-agent epistemic modalities (knowledge of certain messages, truths, and knowledge of others) and the ability to describe time.

The most modern logics I have observed are PCL (Protocol Composition Logic) and CPL (Cryptographic Protocol Logic). These two are extensions or variations of Linear Temporal Logic (LTL). There are also other logics that use the syntax of linear logic (not LTL) instead. All of them include the typical cryptographic primitives ($\text{enc}$, $\text{dec}$, $\text{hash}$, $\text{sign}$, and possibly $\text{blind}$). These primitives are assumed to be perfect within the context of the logic (no probability based assumptions or usage of string representations for data). Reverse engineering them is considered impossible (or deemed out of the scope of our purposes). Our goal is to simply look at the logic and actions involved with the protocol; not the implementation.

Question:

Current logics for cryptographic protocols are primarily used to assess communication based protocols, such as Needham-Schroeder, Wide Mouthed Frog, or Kerberos. This includes both secret sharing and authentication schemes. I am looking for results or research that takes this idea and apply it to information games and decision problems. Interactive proofs, multiparty communication, and algorithmic game theory are fine approaches, but they are mostly based on complexity and number theoretic concepts. I am seeking a solely logical or rational approach that differs from the above for these reasons:

• Resource bounds (time and space) for computation play no role.
• Cryptographic primitives are considered to be perfect. Their use is strongly encouraged.
• No notions or or reliance on collisions, brute force, probability, etc. Our constructions should not rely on number theory, period.
• Must involve epistemic and temporal reasoning.
• Random Elements (nonces, keys, etc) are allowed.

I am specifically aiming for protocols where the goal is not to willingly communicate secrets, but rather to exchange controlled amounts of information, assess situations, reason about an opponent, and distinguish among choices (such as identifying clones/spies or constructing a Turing-like test).

I know this is asking for a lot, so I am open to any pointers or directions as to where to look.

Sample Motivational Problem: Detecting Time Travellers (This is NOT the question asked here):

Suppose you have a friend named Joe who can time travel once into the past. He also has perfect memory. You are faced with two Joes, one from the present and one from the future. We want to distinguish future Joe from present Joe.

This seems impossible at first since future Joe has all the information that present Joe has. Future Joe can keep track of what information he is supposed to know at various times. Therefore, he should be able to perfectly play dumb just as normal Joe would.

A possible approach I am looking into is to mimic the scenario found in the Sleeping Beauty Problem. To summarize, the sleeping beauty is allowed to be woken up, questioned and put back to sleep (this can skew or distort). Furthermore, we can choose if we want her to recall that session or forget it ever happened.

We might want to subject both Joes to variants of this situation many times in succession in order to trick future Joe into revealing information they are not supposed to know. We could even attempt to have the Joe's compete with each other. Future Joe will remember parts of what present Joe was subjected to, but could be faced with vastly different queries.

Can we identify the time traveller? What if we added the ability to distort the ordering of sessions or delete past sessions from memory?

NOTE: This is a sample problem which might be appropriate for the type of analysis requested for in the "Question" section. I am requesting research for logics for cryptographic protocols that extend to game theoretic scenarios in this question. Other related problems might be distinguishment games and strategy making use of metaknowledge and time. I believe that cryptographic primitives can help a great deal here to protect pieces of information and introduce authenticity.

-
If this is outside the scope of crypto.se, please migrate it to cs.se. – mdxn Oct 22 '13 at 1:23
Besides the fact that "Detecting and identifying Time Travellers who have a Perfect Memory" sounds a bit like science fiction, I think this question would have a better home at Security.SE as it's clearly more related to security than cryptography. – e-sushi Oct 22 '13 at 17:12
I don't know about that @e-sushi, it's pretty theoretical for Security.SE. – pg1989 Oct 22 '13 at 21:31
I have the feeling that a question about time travelling is not well received on Security.SE. – Hendrik Brummermann Oct 23 '13 at 11:36
@e-sushi The time traveller problem was just an example/sample problem that involved temporal/epistemic reasoning regarding knowledge and secrets. I could swap out the time traveller aspect with an adversary that has at least all the information that another agent/player knows (or remove it completely). The real question is in the middle (the question section), which asks for resources and research describing cryptographic information games. The approach I am looking for is via mathematical logic, which is why it is considered theoretical. I'll update the question to be more clear. – mdxn Oct 23 '13 at 16:28