Spelling suggestions: "subject:"formal analysis"" "subject:"anormal analysis""
1 |
Modelling and Security Analysis of Authenticated Group Key Agreement ProtocolsPereira, Olivier 16 May 2003 (has links)
<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>
|
2 |
Formal Analysis of Automated Model Abstractions under Uncertainty: Applications in Systems BiologyGhosh, Krishnendu 19 April 2012 (has links)
No description available.
|
3 |
A property-driven methodology for formal analysis of synthetic biology systemsKonur, Savas, Gheorghe, Marian 03 1900 (has links)
Yes / This paper proposes a formal methodology to analyse bio-systems, in particular synthetic biology systems. An integrative analysis perspective combining different model checking approaches based on different property categories is provided. The methodology is applied to the synthetic pulse generator system and several verification experiments are carried out to demonstrate the use of our approach to formally analyse various aspects of synthetic biology systems. / EPSRC
|
4 |
Méthodologie de conception d'architectures numériques complexes : du formalisme à l’implémentation en passant par l'analyse, préservation de la conformité. Application aux neuroprothèses / Design methodology for complex digital systems : from formalism to implementation through formal analysis, preservation of the compliance. Practical application to neuroprostheticsLeroux, Hélène 28 October 2014 (has links)
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.
|
5 |
Formal Analysis of Component Adaptation TechniquesKanetkar, Kavita Vijay 30 April 2002 (has links)
Increasing demand for commercial software components has led to a development and deployment issue of overcoming differences between the customer requirements and developer specifications for the component. Component Adaptation is one solution to the issue. This thesis focuses on modeling the adaptations to an Enterprise JavaBeanTM component using the Z notations and carrying out the adaptations using Active Interfaces adaptation technique. We also formally model the Active Interfaces adaptation technique.
|
6 |
Where is the bakery? : The ethnomethodological conception of social orderAnderberg, Ellinor January 2011 (has links)
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.
|
7 |
Reading/unfolding Architectural Form: An Inquiry Into The Venice Hospital Project By Le CorbusierCinar, Sinem 01 September 2005 (has links) (PDF)
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.
|
8 |
Stylish Politics: Long Takes in Post-1945 CinemaCheney, Zachary 06 September 2017 (has links)
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.
|
9 |
Integrating formal analysis techniques into the Progress-IDEIvanov, Dinko January 2011 (has links)
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.
|
10 |
Integrating formal analysis techniques into the Progress-IDEIvanov, Dinko January 2011 (has links)
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.
|
Page generated in 0.0688 seconds