<p>Authenticated Group Key Agreement Protocols are protocols allowing a group of principals to contributively generate a key by the exchange of messages on a network possibly controlled by an attacker. Furthermore, their execution also guarantees all group members that the key they obtained can only be known by the other intended protocol participants. These protocols can be exploited in many applications such as audio or videoconferencing, replicated servers (such as database, web, time servers), chat or network games for instance.</p> <p>AGKAP's present several particularities that make them interesting case studies for research in the theory of security. At first, the consideration of the number of protocol participants as a parameter raises several complexity problems that are not present in the classical two or three-party frameworks. Furthermore, up to now, the security properties of group protocols have roughly been considered as direct extensions of two-party properties, what does not capture several plausible attack scenarios. A second interesting aspect of the analysis of AGKAP's is the consideration of Diffie-Hellman-type primitives, that present properties out of the scope of most classical models.</p> <p>We started our study with the construction of a simple model for the analysis of a classical family of protocols: the Cliques AGKAP's. This allowed us to discover several attacks and define different flavors of group security properties. We then tried to fix these protocols, what led us to extend our model in order to prove that it is in fact impossible to build a secure AGKAP based on the same design assumptions as the Cliques protocols. Finally, we designed a new AGKAP based on different cryptographic primitives (signature and hash functions) for which we proved authentication, freshness and secrecy properties. A comparison with a similar AGKAP developed in parallel to ours is also proposed.</p>

No description available.

Dans ce mémoire, la conception de systèmes numériques complexes, et notamment de systèmes embarqués critiques, est abordée au travers d'une méthodologie allant de la modélisation formelle à l'implantation sur FPGA : la méthodologie HILECOP. Celle-ci offre au concepteur la possibilité de représenter dans un modèle formel d'une part l'architecture du système selon un assemblage de composants, et d'autre part le comportement de ces composants et leur composition par réseaux de Petri temporels. Le modèle décrit est ensuite transformé automatiquement en un modèle implémentable (en langage VHDL) pour son exécution sur la cible matérielle, mais également en un modèle analysable pour permettre l'analyse formelle des propriétés du système. Les deux objectifs principaux des travaux présentés sont l'étude de la conformité d'un point de vue comportemental entre les différents modèles utilisés dans la méthodologie (modèle conçu, modèle implémentable et modèle analysable), ainsi que l'intégration d'un mécanisme de gestion efficace des exceptions. Ces travaux ont permis de fiabiliser l'implémentation du modèle et d'obtenir un modèle analysable plus pertinent par rapport au modèle conçu, dans le sens où il garantit l'inclusion du comportement du modèle conçu dans celui du modèle analysé et réduit, dans une certaine mesure, le risque d'explosion combinatoire. Les limites de la pertinence des résultats obtenus par analyse formelle sont de plus désormais connues. En ce qui concerne la gestion des exceptions, principalement étudiée au niveau comportemental, le mécanisme de la macro-place a été retenu et adapté aux contraintes fonctionnelles et non-fonctionnelles des systèmes embarqués critiques. L'apport de la macro-place et la conservation de la conformité ont pu être validés sur des modèles industriels relatifs à l'architecture numérique de neuroprothèses. / In this thesis, the conception of digital complex systems, and notably of critical embedded systems, is discussed through a methodology which goes from formal modeling to the implementation on a FPGA: the HILECOP methodology. This methodology offers, to a designer, the possibility of representing in a formal model from one hand the digital architecture thanks to some components' assembly, and on the other hand the behavior of these components and their composition, thanks to time Petri nets. The described model is then automatically transformed in an implementable model (in the VHDL language) for its execution on a hardware target, but also in an analyzable model to allow some formal analysis on system properties to be performed. The two main goals of the presented work are the study of the behavioral conformity between the different models used in the methodology (designed model, implementable model and analyzable model) and the integration of an efficient mechanism for handling exception. These works allow to have a more reliable implementation of the model and to obtain a more relevant analyzable model. It is now possible to guarantee that the behavior of the designed model is included in the analyzed one. The risk of combinatorial explosion has also been reduced to some extent. The limits of the relevance of the obtained results thanks to the formal analysis are henceforth known. As for exception handling, it has been mostly studied on the behavioral level. The mechanism of the macroplace has been chosen and adapted to meet the functional and non-functional constraints of critical embedded systems. The benefits given by the use of the macroplace and the preservation of the conformity between the models have been validated on industrial models relative to the digital architecture of neuroprosthetics.

The fundamental sociological problem of social order finds a somewhat ”unorthodox” solution in the ethnomethodological program, the main responsibility of which is ascribed to Harold Garfinkel. The current thesis rests on the view that the program offers insights that have not been sufficiently recognized, and that it bears a message to sociology that has been somewhat lost. The study aims to investigate and uncover the ethnomethodological conception of social order in a comprehensible way. Comparisons are made to “formal analytical” perspectives, notably that advocated by Talcott Parsons. The result suggests that the ethnomethodological conception of order is closer related to intersubjectivity than to action theory, and that the ethnomethodological view completes rather than opposes that of formal analysis. The deeper ontological and epistemological implications of ethnomethodology are discussed, partly by invocation of the notion of radical reflexivity.

This study aims to discuss the generative possibilities of reading architectural form by focusing on selected interpretations of the Venice Hospital project by Le Corbusier. By presenting complementary and competing readings of the project, it examines different design strategies in the formal organization of the Venice Hospital. It shows that the Venice Hospital project, displaying the characteristics of both a &ldquo / field&rdquo / organization and a well-articulated object, demands a reconsideration of the occasionally overstated distinction between them. First, it introduces interpretations of the Venice Hospital as a field and/or mat-building phenomenon, which emphasize its relevance as a precedent for contemporary formal explorations. The complexity of the Venice Hospital project requires appealing to other reading strategies as well. Based on the discussion initiated by Colin Rowe and Fred Koetter in &ldquo / The Crisis of the Object: The Predicament of Texture,&rdquo / and owing to Alan Colquhoun&rsquo / s analysis of the project&rsquo / s geometrical system in &ldquo / Formal and Functional Interactions,&rdquo / this study proceeds by exploring the way the Venice Hospital becomes &ldquo / an object performing like a texture.&rdquo / It attempts to decipher Colquhoun&rsquo / s remarks and his diagrams concerning the geometrical system through the technique of the &ldquo / plan analysis&rdquo / introduced by Klaus-Peter Gast. The Venice Hospital project is also studied as an example of transparent spatial organization, in light of the conceptual framework developed by Colin Rowe and Robert Slutzky in their &ldquo / Transparency&rdquo / articles. Starting from these interpretations of the Venice Hospital project, this study aims at bringing into discussion the nature of the devices or techniques of formal organization that can mediate between architecture and urbanism. These devices are examined in light of the framework constituted by the concepts of &ldquo / device&rdquo / and &ldquo / material,&rdquo / elucidated by the Russian Formalists. The &ldquo / device and material relationship&rdquo / that was invoked in the formalist tradition of literary criticism, is reformulated for the field of architecture, and it is discussed with its capacity to initiate generative and inclusive interpretations of works of architecture as precedents.

This dissertation is a politically conscious, comparative-historical formal analysis of long takes at the intersection of art and mass-market cinemas in the post-WWII era. Given the contemporary fascination with long takes in the critical discourse of film along with its fairly rampant employment in contemporary mainstream cinema, the discipline has lacked scholarship carefully examining formal techniques as such while remaining alert to the non-reductive possibilities for their political significance. Enlisting and building on the analytical approach of a cinematic poetics, the project outlines numerous contingencies in the practice of very long takes and their function in producing meaning before attending to the technique at the levels of cinematography, editing, and mise-en-scène in separate chapters. Objects of analysis are roughly divided in each chapter between progenitors of contemporary long-take practice—Italian neorealist films, Rope (1948), the 1960s and 1980s films of Jean-Luc Godard, and Jeanne Dielman (1975)—and more recent examples—Timecode (2000), Children of Men (2006), Birdman (2014), A Girl Walks Home Alone At Night (2014), and Too Late (2015). The dissertation invests in the inseparability of form and content, as well as the political stakes of long take practice at both levels by parsing out the historical, technological, cultural, and diegetic contexts of long takes. In so doing, the approach exemplifies previously unrecognized possibilities for employing a historical poetics in a manner acknowledging a formal technique’s commitments to and participation in social power dynamics. These dynamics are legible within a film, in its production, and in its participation in the historical tradition of authorship as constructed in European art cinema.

In this thesis we contribute to the Progress IDE, an integrated development enviroment for real-time embedded systems and more precisely to the REMES toolchain, a set of tools to enabling construction and analysis of embedded system behavior models. The contribution aims to facilitate the formal analysis of behavioral models, so that certain extra-functional properties might be verified during early stages of development. Previous work in the field proposes use of the Priced Timed Automata framework for verification of such properties. The thesis outlines the main points where the current toolchain should be extended in order to allow formal analysis of modeled components. Result of the work is a prototype, which minimizes the manual efforts of system designer by model to model transformations and provides seamless integration with existing tools for formal analysis.

In this thesis we contribute to the Progress IDE, an integrated development enviroment for real-time embedded systems and more precisely to the REMES toolchain, a set of tools to enabling construction and analysis of embedded system behavior models. The contribution aims to facilitate the formal analysis of behavioral models, so that certain extra-functional properties might be verified during early stages of development. Previous work in the field proposes use of the Priced Timed Automata framework for verification of such properties. The thesis outlines the main points where the current toolchain should be extended in order to allow formal analysis of modeled components. Result of the work is a prototype, which minimizes the manual efforts of system designer by model to model transformations and provides seamless integration with existing tools for formal analysis.

In this thesis, the question of immersion and learning in tutorials is examined to find whether there are principles of design that can universally form a tutorial of a high quality according to several predetermined traits. A formal analysis of the tutorials for three specified games are conducted to identify the underlying principles of design that govern the structure for each individual tutorial. The resulting analyses are then compared to each other to reveal similarities between the tutorials so that the principles of design can be identified and examined. The findings point to no universal principles of design that will generate a tutorial of high quality, instead, the utilization of these principles is angled towards the specific needs of the game being developed. / I denna uppsats undersöks frågan om fördjupning och inlärning i de inledande, handledande/guidande sekvenserna i spel för att granska om det finns design-principer som universellt kan användas för att göra handledande/guidande sekvenser i spel av en högre kvalitet enligt flera förbestämda drag. En formell analys av introsekvenserna för tre specifika spel görs för att identifiera de underliggande design-principerna som utgör strukturen för varje individuell introsekvens. De resulterande analyserna blir sedan jämförda med varandra för att uppdaga likheter mellan introsekvenserna så att design-principerna kan identifieras och undersökas. Resultaten visar att inga sådana universella design-principer finns, istället bör dessa design-principer nyttjas på ett sätt som bäst passar de specifika krav som spelet som utvecklas har.

Formally-based design and implementation techniques for complex safety-critical embedded systems are required not only to handle the complexity, but also to provide correctness guarantees. Traditional design approaches struggle to cope with complexity, and they generally require extensive testing to guarantee correctness. As the designs get larger and more complex, traditional approaches face many limitations. An alternate design approach is to adopt a "correct-by-construction" paradigm and synthesize the desired hardware and software from the high-level descriptions expressed using one of the many formal modeling languages. Since these languages are equipped with formal semantics, formally-based tools can be employed for various analysis. In this dissertation, we adopt one such formal modeling language - MRICDF (Multi-Rate Instantaneous Channel-connected Data Flow). MRICDF is a graphical, declarative, polychronous modeling language, with a formalism that allows the modeler to easily describe multi-clocked systems without the necessity of global clock. Unnecessary synchronizations among concurrent computation entities can be avoided using a polychronous language such as MRICDF. We have explored a Boolean theory-based techniques for synthesizing multi-threaded/concurrent code and extended the technique to improve the performance of synthesized multi-threaded code. We also explored synthesizing ASIPs (Application Specific Instruction Set Processors) from MRICDF models. Further, we have developed formal techniques to identify constructive causality in polychronous models. We have also developed SMT (Satisfiablity Modulo Theory)-based techniques to identify dimensional inconsistencies and to perform value-range analysis of polychronous models. / Ph. D.